./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec3_product35.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec3_product35.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2585:3-2606:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2642:3-2667:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2727:5-2747:5 with factor 2
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:192:1-202:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:281:1-292:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:293:1-304:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:645:1-659:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:923:1-937:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:941:1-966:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:967:1-986:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:991:1-1014:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1015:1-1034:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1082:1-1106:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1116:1-1184:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1185:1-1253:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1983:1-1997:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2019:1-2034:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2111:1-2131:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2132:1-2147:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2150:1-2170:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2171:1-2186:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2483:1-2491:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2514:1-2559:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2560:1-2615:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2616:1-2675:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2678:1-2780:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2781:1-2826:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2827:1-2872:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2875:1-2884:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2910:1-2924:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2931-2931)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1607-1607)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2504-2504)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1831-1831)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1332..1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1332-1334)
  on lines 1336..1337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1336-1337)
  on lines 1342..1345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1342-1345)
  on lines 1347..1349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1347-1349)
  on lines 1351..1353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1351-1353)
  on lines 1355..1356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1355-1356)
  on lines 1361..1364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1361-1364)
  on lines 1366..1368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1366-1368)
  on lines 1370..1372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1370-1372)
  on lines 1374..1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1374-1375)
  on lines 1380..1381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1380-1381)
  on line 1385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1385-1385)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1059-1059)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1468-1468)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1903-1903)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1950-1950)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1735..1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1735-1737)
  on lines 1739..1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1739-1740)
  on lines 1744..1747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1744-1747)
  on lines 1749..1751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1749-1751)
  on lines 1753..1754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1753-1754)
  on lines 1758..1761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1758-1761)
  on lines 1763..1765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1763-1765)
  on lines 1767..1768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1767-1768)
  on lines 1772..1773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1772-1773)
  on line 1777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1777-1777)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1557..1558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1557-1558)
  on line 1562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1562-1562)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1628..1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1628-1630)
  on lines 1632..1633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1632-1633)
  on lines 1637..1640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1637-1640)
  on lines 1642..1644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1642-1644)
  on lines 1646..1647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1646-1647)
  on lines 1651..1654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1651-1654)
  on lines 1656..1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1656-1658)
  on lines 1660..1661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1660-1661)
  on lines 1665..1666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1665-1666)
  on line 1670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1670-1670)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1515-1515)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2235..2236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2235-2236)
  on line 2242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2242-2242)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2046..2047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2046-2047)
  on line 2053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2053-2053)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2009..2010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2009-2010)
  on line 2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2016-2016)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2309..2310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2309-2310)
  on line 2316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2316-2316)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2083..2084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2083-2084)
  on line 2090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2090-2090)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:698-698)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:707-707)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2198..2199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2198-2199)
  on line 2205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2205-2205)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 724..725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:724-725)
  on line 732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:732-732)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2480-2480)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2460-2460)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2272..2273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2272-2273)
  on line 2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2279-2279)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2346..2347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2346-2347)
  on line 2353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2353-2353)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:689-689)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1399..1400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1399-1400)
  on lines 1407..1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1407-1409)
  on lines 1411..1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1411-1412)
  on lines 1414..1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1414-1415)
  on lines 1422..1424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1422-1424)
  on lines 1426..1427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1426-1427)
  on lines 1429..1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1429-1430)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1262..1263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1262-1263)
  on lines 1265..1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1265-1266)
  on lines 1273..1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1273-1275)
  on lines 1277..1278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1277-1278)
  on lines 1280..1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1280-1281)
  on lines 1288..1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1288-1290)
  on lines 1292..1293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1292-1293)
  on lines 1295..1296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1295-1296)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1069..1070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1069-1070)
  on lines 1072..1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1072-1073)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1476-1476)
  on lines 1481..1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1481-1482)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1911-1911)
  on lines 1916..1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1916-1917)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1842..1843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1842-1843)
  on lines 1853..1854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1853-1854)
  on lines 1864..1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1864-1865)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1681..1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1681-1682)
  on lines 1692..1693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1692-1693)
  on lines 1703..1704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1703-1704)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2253-2253)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2064-2064)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2216-2216)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2364-2364)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2290-2290)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2327-2327)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2101-2101)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2905-2905)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 703
  dead: 547 (355 in uncalled functions)
  total lines: 1250
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2271:9-2271:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1575:11-1575:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2289:9-2289:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2045:9-2045:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2308:9-2308:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1623:7-1623:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1624:9-1624:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2063:9-2063:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1392:7-1392:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2326:9-2326:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1396:11-1396:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2082:9-2082:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1839:9-1839:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2345:9-2345:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:723:9-723:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2100:9-2100:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1850:11-1850:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1860:11-1860:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2363:9-2363:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1861:13-1861:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2974:10-2974:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1678:9-1678:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1689:11-1689:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1258:7-1258:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1910:7-1910:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1259:9-1259:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1066:7-1066:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1475:7-1475:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1699:11-1699:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1913:9-1913:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1700:13-1700:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1478:9-1478:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1730:7-1730:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1731:9-1731:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2197:9-2197:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2215:9-2215:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1323:7-1323:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1963:11-1963:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1528:11-1528:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1328:11-1328:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:236:7-236:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2234:9-2234:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:1553:11-1553:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2252:9-2252:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product35.cil.c:2008:9-2008:20)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
