./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_product14.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_product14.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_product14.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_product14.cil.c:2229:3-2250:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2286:3-2311:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2371:5-2391: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_product14.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_product14.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_product14.cil.c:289:1-300:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:438:1-452:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:456:1-481:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:482:1-501:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:506:1-529:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:530:1-549:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:597:1-621:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:631:1-699:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:700:1-768:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:962:1-985:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:986:1-1005:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1397:1-1420:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1421:1-1440:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1490:1-1499:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1696:1-1710:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1724:1-1733:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1743:1-1751:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1752:1-1760:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2021:1-2035:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2051:1-2078:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2079:1-2097:1)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2098:1-2106:1)
[Warning][Deadcode] Function 'isReadable' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2107:1-2126:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2127:1-2135:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2158:1-2203:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2204:1-2259:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2260:1-2319:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2322:1-2424:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2425:1-2470:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2471:1-2516:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2531:1-2545:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2548:1-2566:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2567:1-2582:1)
[Warning][Deadcode] Function 'getEmailFrom' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2585:1-2603:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2659:1-2679:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2680:1-2695:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2698:1-2718:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2719:1-2734:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2811:1-2829:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2830:1-2845:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2848:1-2866:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2867:1-2882:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2885:1-2903:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2904:1-2919:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2042-2042)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 180..182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:180-182)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1122-1122)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2148-2148)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1313..1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1313-1316)
  on lines 1318..1320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1318-1320)
  on lines 1322..1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1322-1323)
  on lines 1327..1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1327-1330)
  on lines 1332..1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1332-1334)
  on lines 1336..1337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1336-1337)
  on lines 1341..1342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1341-1342)
  on line 1346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1346-1346)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 847..849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:847-849)
  on lines 851..852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:851-852)
  on lines 857..860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:857-860)
  on lines 862..864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:862-864)
  on lines 866..868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:866-868)
  on lines 870..871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:870-871)
  on lines 876..879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:876-879)
  on lines 881..883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:881-883)
  on lines 885..887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:885-887)
  on lines 889..890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:889-890)
  on lines 895..896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:895-896)
  on line 900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:900-900)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 561..563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:561-563)
  on lines 565..567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:565-567)
  on lines 569..570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:569-570)
  on line 574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:574-574)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1452..1454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1452-1454)
  on lines 1456..1458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1456-1458)
  on lines 1460..1461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1460-1461)
  on line 1465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1465-1465)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1250..1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1250-1252)
  on lines 1254..1255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1254-1255)
  on lines 1259..1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1259-1262)
  on lines 1264..1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1264-1266)
  on lines 1268..1269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1268-1269)
  on lines 1273..1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1273-1276)
  on lines 1278..1280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1278-1280)
  on lines 1282..1283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1282-1283)
  on lines 1287..1288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1287-1288)
  on line 1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1292-1292)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1072..1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1072-1073)
  on line 1077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1077-1077)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1143..1145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1143-1145)
  on lines 1147..1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1147-1148)
  on lines 1152..1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1152-1155)
  on lines 1157..1159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1157-1159)
  on lines 1161..1162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1161-1162)
  on lines 1166..1169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1166-1169)
  on lines 1171..1173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1171-1173)
  on lines 1175..1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1175-1176)
  on lines 1180..1181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1180-1181)
  on line 1185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1185-1185)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1014..1015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1014-1015)
  on line 1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1030-1030)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2782..2784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2782-2784)
  on lines 2786..2787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2786-2787)
  on line 2790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2790-2790)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2630..2632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2630-2632)
  on lines 2634..2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2634-2635)
  on line 2638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2638-2638)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2745..2747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2745-2747)
  on lines 2749..2750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2749-2750)
  on line 2753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2753-2753)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1783-1783)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1740-1740)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 914..915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:914-915)
  on lines 922..924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:922-924)
  on lines 926..927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:926-927)
  on lines 929..930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:929-930)
  on lines 937..939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:937-939)
  on lines 941..942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:941-942)
  on lines 944..945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:944-945)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 777..778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:777-778)
  on lines 780..781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:780-781)
  on lines 788..790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:788-790)
  on lines 792..793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:792-793)
  on lines 795..796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:795-796)
  on lines 803..805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:803-805)
  on lines 807..808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:807-808)
  on lines 810..811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:810-811)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 584..585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:584-585)
  on lines 587..588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:587-588)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1357..1358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1357-1358)
  on lines 1368..1369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1368-1369)
  on lines 1379..1380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1379-1380)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1196..1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1196-1197)
  on lines 1207..1208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1207-1208)
  on lines 1218..1219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1218-1219)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on lines 2800..2801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2800-2801)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 2611..2612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2611-2612)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on lines 2763..2764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2763-2764)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 2648..2649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2648-2649)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1520-1520)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 438
  dead: 708 (494 in uncalled functions)
  total lines: 1146
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2797:7-2797:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1204:11-1204:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:773:7-773:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:774:9-774:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:581:7-581:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1214:11-1214:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1215:13-1215:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1448:7-1448:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1245:7-1245:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1013:7-1013:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1246:9-1246:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2608:7-2608:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:838:7-838:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2626:7-2626:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1478:11-1478:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1043:11-1043:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:843:11-843:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2645:7-2645:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1068:11-1068:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1299:7-1299:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1843:10-1843:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1090:11-1090:22)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.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_product14.cil.c:1138:7-1138:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1139:9-1139:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:907:7-907:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:911:11-911:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2741:7-2741:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1354:9-1354:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1365:11-1365:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.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_product14.cil.c:2760:7-2760:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1375:11-1375:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1376:13-1376:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:2778:7-2778:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:557:7-557:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product14.cil.c:1193:9-1193:19)
[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
