./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_spec6_product29.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_spec6_product29.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_spec6_product29.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_spec6_product29.cil.c:446:3-467:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:503:3-528:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:588:5-608: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_spec6_product29.cil.c:188:1-198:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:277:1-288:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:289:1-300:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:375:1-420:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:421:1-476:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:477:1-536:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:539:1-641:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:642:1-687:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:688:1-733:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:804:1-818:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:822:1-847:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:848:1-867:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:872:1-895:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:896:1-915:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:963:1-987:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:997:1-1065:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1066:1-1134:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1328:1-1351:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1352:1-1371:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1763:1-1786:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1787:1-1806:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2081:1-2095:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2098:1-2107:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2144:1-2171:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2172:1-2190:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2191:1-2209:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2210:1-2223:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2253:1-2261:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2290:1-2304:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2307:1-2325:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2326:1-2341:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2418:1-2438:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2439:1-2454:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2457:1-2477:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2478:1-2493:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2644:1-2662:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2870:1-2884:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2898:1-2907:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2917:1-2925:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2926:1-2934:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1860-1860)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 180..182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:180-182)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1488-1488)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2274-2274)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1685..1686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1685-1686)
  on lines 1699..1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1699-1700)
  on line 1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1712-1712)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1213..1215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1213-1215)
  on lines 1217..1218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1217-1218)
  on lines 1223..1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1223-1226)
  on lines 1228..1230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1228-1230)
  on lines 1232..1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1232-1234)
  on lines 1236..1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1236-1237)
  on lines 1242..1245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1242-1245)
  on lines 1247..1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1247-1249)
  on lines 1251..1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1251-1253)
  on lines 1255..1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1255-1256)
  on lines 1261..1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1261-1262)
  on line 1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1266-1266)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 927..929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:927-929)
  on lines 931..933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:931-933)
  on lines 935..936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:935-936)
  on line 940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:940-940)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1818..1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1818-1820)
  on lines 1822..1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1822-1824)
  on lines 1826..1827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1826-1827)
  on line 1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1831-1831)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1616..1618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1616-1618)
  on lines 1620..1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1620-1621)
  on lines 1625..1628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1625-1628)
  on lines 1630..1632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1630-1632)
  on lines 1634..1635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1634-1635)
  on lines 1639..1642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1639-1642)
  on lines 1644..1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1644-1646)
  on lines 1648..1649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1648-1649)
  on lines 1653..1654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1653-1654)
  on line 1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1658-1658)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1438..1439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1438-1439)
  on line 1443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1443-1443)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1509..1511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1509-1511)
  on lines 1513..1514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1513-1514)
  on lines 1518..1521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1518-1521)
  on lines 1523..1525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1523-1525)
  on lines 1527..1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1527-1528)
  on lines 1532..1535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1532-1535)
  on lines 1537..1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1537-1539)
  on lines 1541..1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1541-1542)
  on lines 1546..1547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1546-1547)
  on line 1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1551-1551)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1396-1396)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2541..2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2541-2543)
  on lines 2545..2546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2545-2546)
  on line 2549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2549-2549)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2352..2354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2352-2354)
  on lines 2356..2357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2356-2357)
  on line 2360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2360-2360)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2615..2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2615-2617)
  on lines 2619..2620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2619-2620)
  on line 2623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2623-2623)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2389..2391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2389-2391)
  on lines 2393..2394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2393-2394)
  on line 2397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2397-2397)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2504..2506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2504-2506)
  on lines 2508..2509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2508-2509)
  on line 2512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2512-2512)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 2957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2957-2957)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2250-2250)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2230-2230)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2578..2580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2578-2580)
  on lines 2582..2583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2582-2583)
  on line 2586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2586-2586)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2914-2914)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1280..1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1280-1281)
  on lines 1288..1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1288-1290)
  on lines 1292..1293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1292-1293)
  on lines 1295..1296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1295-1296)
  on lines 1303..1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1303-1305)
  on lines 1307..1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1307-1308)
  on lines 1310..1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1310-1311)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1143..1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1143-1144)
  on lines 1146..1147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1146-1147)
  on lines 1154..1156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1154-1156)
  on lines 1158..1159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1158-1159)
  on lines 1161..1162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1161-1162)
  on lines 1169..1171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1169-1171)
  on lines 1173..1174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1173-1174)
  on lines 1176..1177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1176-1177)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 950..951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:950-951)
  on lines 953..954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:953-954)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1723..1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1723-1724)
  on lines 1734..1735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1734-1735)
  on lines 1745..1746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1745-1746)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1562..1563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1562-1563)
  on lines 1573..1574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1573-1574)
  on lines 1584..1585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1584-1585)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on lines 2559..2560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2559-2560)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 2370..2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2370-2371)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on lines 2522..2523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2522-2523)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on lines 2670..2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2670-2671)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on lines 2596..2597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2596-2597)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on lines 2633..2634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2633-2634)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 2407..2408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2407-2408)
[Warning][Deadcode] Function 'sign' has dead code:
  on line 2987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2987-2987)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2128-2128)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 3018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:3018-3018)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 520
  dead: 679 (455 in uncalled functions)
  total lines: 1199
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1720:9-1720:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2519:7-2519:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1731:11-1731:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2537:7-2537:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1741:11-1741:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1742:13-1742:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:923:7-923:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2556:7-2556:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1559:9-1559:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2574:7-2574:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1570:11-1570:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1139:7-1139:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:947:7-947:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1140:9-1140:19)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1580:11-1580:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1581:13-1581:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2593:7-2593:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2348:7-2348:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1814:7-1814:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1611:7-1611:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1612:9-1612:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2611:7-2611:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2367:7-2367:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2630:7-2630:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2385:7-2385:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1204:7-1204:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1844:11-1844:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1409:11-1409:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1209:11-1209:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2404:7-2404:18)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:176:7-176:14)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2667:7-2667:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1434:11-1434:22)
[Warning][Deadcode][CWE-570] condition '! privkey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2986:7-2986:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1903:10-1903:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1456:11-1456:22)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:3015:9-3015:16)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring1_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1684:13-1684:50)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:232:7-232:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1504:7-1504:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1505:9-1505:19)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring2_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1698:15-1698:52)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1273:7-1273:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:2500:7-2500:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product29.cil.c:1277:11-1277:21)
[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
