./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_spec27_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_spec27_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_spec27_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_spec27_product29.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:268:5-288: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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:444:1-458:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:462:1-487:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:488:1-507:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:512:1-535:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:536:1-555:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:603:1-627:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:637:1-705:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:706:1-774:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:968:1-991:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:992:1-1011:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1403:1-1426:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1427:1-1446:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1510:1-1519:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1546:1-1560:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1585:1-1612:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1613:1-1631:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1632:1-1650:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1651:1-1664:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1694:1-1702:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2144:1-2158:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2172:1-2181:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2191:1-2199:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2200:1-2208:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2328:1-2342:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2345:1-2363:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2364:1-2379:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2456:1-2476:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2477:1-2492:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2495:1-2515:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2516:1-2531:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2815:1-2825:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2904:1-2915:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2916:1-2927:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1567-1567)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 2807..2809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2807-2809)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1128-1128)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1715-1715)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1325..1326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1325-1326)
  on lines 1339..1340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1339-1340)
  on line 1352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1352-1352)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 853..855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:853-855)
  on lines 857..858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:857-858)
  on lines 863..866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:863-866)
  on lines 868..870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:868-870)
  on lines 872..874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:872-874)
  on lines 876..877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:876-877)
  on lines 882..885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:882-885)
  on lines 887..889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:887-889)
  on lines 891..893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:891-893)
  on lines 895..896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:895-896)
  on lines 901..902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:901-902)
  on line 906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:906-906)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 567..569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:567-569)
  on lines 571..573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:571-573)
  on lines 575..576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:575-576)
  on line 580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:580-580)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1458..1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1458-1460)
  on lines 1462..1464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1462-1464)
  on lines 1466..1467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1466-1467)
  on line 1471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1471-1471)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1256..1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1256-1258)
  on lines 1260..1261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1260-1261)
  on lines 1265..1268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1265-1268)
  on lines 1270..1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1270-1272)
  on lines 1274..1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1274-1275)
  on lines 1279..1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1279-1282)
  on lines 1284..1286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1284-1286)
  on lines 1288..1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1288-1289)
  on lines 1293..1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1293-1294)
  on line 1298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1298-1298)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1078..1079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1078-1079)
  on line 1083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1083-1083)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1149..1151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1149-1151)
  on lines 1153..1154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1153-1154)
  on lines 1158..1161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1158-1161)
  on lines 1163..1165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1163-1165)
  on lines 1167..1168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1167-1168)
  on lines 1172..1175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1172-1175)
  on lines 1177..1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1177-1179)
  on lines 1181..1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1181-1182)
  on lines 1186..1187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1186-1187)
  on line 1191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1191-1191)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1036-1036)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2579..2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2579-2581)
  on lines 2583..2584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2583-2584)
  on line 2587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2587-2587)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2390..2392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2390-2392)
  on lines 2394..2395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2394-2395)
  on line 2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2398-2398)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2653..2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2653-2655)
  on lines 2657..2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2657-2658)
  on line 2661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2661-2661)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2427..2429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2427-2429)
  on lines 2431..2432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2431-2432)
  on line 2435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2435-2435)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2542..2544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2542-2544)
  on lines 2546..2547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2546-2547)
  on line 2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2550-2550)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2223..2224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2223-2224)
  on line 2231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2231-2231)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1691-1691)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1671-1671)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2616..2618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2616-2618)
  on lines 2620..2621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2620-2621)
  on line 2624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2624-2624)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2690..2692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2690-2692)
  on lines 2694..2695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2694-2695)
  on line 2698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2698-2698)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2188-2188)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 920..921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:920-921)
  on lines 928..930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:928-930)
  on lines 932..933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:932-933)
  on lines 935..936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:935-936)
  on lines 943..945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:943-945)
  on lines 947..948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:947-948)
  on lines 950..951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:950-951)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 783..784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:783-784)
  on lines 786..787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:786-787)
  on lines 794..796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:794-796)
  on lines 798..799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:798-799)
  on lines 801..802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:801-802)
  on lines 809..811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:809-811)
  on lines 813..814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:813-814)
  on lines 816..817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:816-817)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 590..591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:590-591)
  on lines 593..594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:593-594)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1363..1364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1363-1364)
  on lines 1374..1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1374-1375)
  on lines 1385..1386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1385-1386)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1202..1203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1202-1203)
  on lines 1213..1214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1213-1214)
  on lines 1224..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1224-1225)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on lines 2597..2598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2597-2598)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 2408..2409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2408-2409)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on lines 2560..2561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2560-2561)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on lines 2708..2709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2708-2709)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on lines 2634..2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2634-2635)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on lines 2671..2672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2671-2672)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 2445..2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2445-2446)
[Warning][Deadcode] Function 'sign' has dead code:
  on line 2261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2261-2261)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1540-1540)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 2292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2292-2292)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 513
  dead: 678 (446 in uncalled functions)
  total lines: 1191
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1360:9-1360:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1371:11-1371:21)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2803:7-2803:14)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1381:11-1381:22)
[Warning][Deadcode][CWE-570] condition '! privkey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2260:7-2260:16)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1382:13-1382:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2538:7-2538:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:563:7-563:18)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2289:9-2289:16)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1199:9-1199:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2557:7-2557:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1210:11-1210:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:779:7-779:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:780:9-780:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:587:7-587:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2575:7-2575:18)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2859:7-2859:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1220:11-1220:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1221:13-1221:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1767:10-1767:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1454:7-1454:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1251:7-1251:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1252:9-1252:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2594:7-2594:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2612:7-2612:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:844:7-844:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2631:7-2631:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2386:7-2386:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1484:11-1484:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1049:11-1049:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:849:11-849:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2649:7-2649:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2405:7-2405:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1074:11-1074:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2668:7-2668:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2423:7-2423:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2686:7-2686:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1096:11-1096:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2442:7-2442:18)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring1_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1324:13-1324:50)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2705:7-2705:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1144:7-1144:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1145:9-1145:19)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring2_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:1338:15-1338:52)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:913:7-913:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:917:11-917:21)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product29.cil.c:2222:9-2222: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
