./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_product34.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_product34.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_product34.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_product34.cil.c:2818:3-2839:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2875:3-2900:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2960:5-2980: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_product34.cil.c:254:1-264:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:343:1-354:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:355:1-366:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:462:1-476:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:480:1-505:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:506:1-525:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:530:1-553:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:554:1-573:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:621:1-645:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:655:1-723:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:724:1-792:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:986:1-1009:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1010:1-1029:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1733:1-1747:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1928:1-1937:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2074:1-2082:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2109:1-2123:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2351:1-2365:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2387:1-2402:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2479:1-2499:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2500:1-2515:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2518:1-2538:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2539:1-2554:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2747:1-2792:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2793:1-2848:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2849:1-2908:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2911:1-3013:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:3014:1-3059:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:3060:1-3105:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2104-2104)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1146-1146)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2095-2095)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1370-1370)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 871..873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:871-873)
  on lines 875..876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:875-876)
  on lines 881..884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:881-884)
  on lines 886..888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:886-888)
  on lines 890..892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:890-892)
  on lines 894..895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:894-895)
  on lines 900..903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:900-903)
  on lines 905..907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:905-907)
  on lines 909..911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:909-911)
  on lines 913..914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:913-914)
  on lines 919..920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:919-920)
  on line 924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:924-924)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 590..591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:590-591)
  on line 598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:598-598)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1426..1427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1426-1427)
  on line 1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1442-1442)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1481..1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1481-1482)
  on line 1489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1489-1489)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1274..1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1274-1276)
  on lines 1278..1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1278-1279)
  on lines 1283..1286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1283-1286)
  on lines 1288..1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1288-1290)
  on lines 1292..1293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1292-1293)
  on lines 1297..1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1297-1300)
  on lines 1302..1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1302-1304)
  on lines 1306..1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1306-1307)
  on lines 1311..1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1311-1312)
  on line 1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1316-1316)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1096..1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1096-1097)
  on line 1101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1101-1101)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1167..1169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1167-1169)
  on lines 1171..1172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1171-1172)
  on lines 1176..1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1176-1179)
  on lines 1181..1183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1181-1183)
  on lines 1185..1186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1185-1186)
  on lines 1190..1193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1190-1193)
  on lines 1195..1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1195-1197)
  on lines 1199..1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1199-1200)
  on lines 1204..1205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1204-1205)
  on line 1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1209-1209)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1054-1054)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2603..2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2603-2604)
  on line 2610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2610-2610)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2414..2415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2414-2415)
  on line 2421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2421-2421)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2377..2378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2377-2378)
  on line 2384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2384-2384)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2677..2678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2677-2678)
  on line 2684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2684-2684)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2451..2452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2451-2452)
  on line 2458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2458-2458)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1786-1786)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1795-1795)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2566..2567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2566-2567)
  on line 2573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2573-2573)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1812..1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1812-1813)
  on line 1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1820-1820)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2071-2071)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2051-2051)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2640..2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2640-2641)
  on line 2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2647-2647)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2714..2715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2714-2715)
  on line 2721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2721-2721)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1777-1777)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 938..939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:938-939)
  on lines 946..948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:946-948)
  on lines 950..951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:950-951)
  on lines 953..954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:953-954)
  on lines 961..963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:961-963)
  on lines 965..966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:965-966)
  on lines 968..969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:968-969)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 801..802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:801-802)
  on lines 804..805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:804-805)
  on lines 812..814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:812-814)
  on lines 816..817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:816-817)
  on lines 819..820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:819-820)
  on lines 827..829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:827-829)
  on lines 831..832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:831-832)
  on lines 834..835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:834-835)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 608..609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:608-609)
  on lines 611..612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:611-612)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1450-1450)
  on lines 1455..1456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1455-1456)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1381..1382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1381-1382)
  on lines 1392..1393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1392-1393)
  on lines 1403..1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1403-1404)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1220..1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1220-1221)
  on lines 1231..1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1231-1232)
  on lines 1242..1243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1242-1243)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2621-2621)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2432-2432)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2584-2584)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2732-2732)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2658-2658)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2695-2695)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2469-2469)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1958-1958)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 663
  dead: 568 (374 in uncalled functions)
  total lines: 1231
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1425:7-1425:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1217:9-1217:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:298:7-298:10)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:589:11-589:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1228:11-1228:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:797:7-797:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1449:7-1449:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:798:9-798:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:605:7-605:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2565:9-2565:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1238:11-1238:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1452:9-1452:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1239:13-1239:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1269:7-1269:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1270:9-1270:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2583:9-2583:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1480:11-1480:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2602:9-2602:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1811:9-1811:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:862:7-862:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2620:9-2620:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1502:11-1502:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2376:9-2376:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1067:11-1067:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:867:11-867:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2639:9-2639:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1092:11-1092:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2164:10-2164:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2657:9-2657:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2413:9-2413:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2676:9-2676:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1114:11-1114:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2431:9-2431:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2694:9-2694:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2450:9-2450:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1162:7-1162:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1163:9-1163:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2713:9-2713:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2468:9-2468:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:931:7-931:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:935:11-935:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:2731:9-2731:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1378:9-1378:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1389:11-1389:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1399:11-1399:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product34.cil.c:1400:13-1400:23)
[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
