./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_product23.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_product23.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_product23.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_product23.cil.c:677:3-698:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:734:3-759:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:819:5-839: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_product23.cil.c:190:1-200:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:279:1-290:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:291:1-302:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:606:1-651:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:652:1-707:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:708:1-767:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:770:1-872:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:873:1-918:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:919:1-964:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:997:1-1011:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1014:1-1032:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1033:1-1048:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1125:1-1145:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1146:1-1161:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1164:1-1184:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1185:1-1200:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1203:1-1221:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1222:1-1237:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1240:1-1258:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1259:1-1274:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1351:1-1369:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1388:1-1402:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1405:1-1414:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1443:1-1470:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1471:1-1489:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1490:1-1503:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1513:1-1521:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1740:1-1754:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1948:1-1962:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1966:1-1991:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1992:1-2011:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2016:1-2039:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2040:1-2059:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2107:1-2131:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2141:1-2209:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2210:1-2278:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2907:1-2930:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2931:1-2950:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:971-971)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2632-2632)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1534-1534)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2843..2844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2843-2844)
  on line 2856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2856-2856)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2357..2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2357-2359)
  on lines 2361..2362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2361-2362)
  on lines 2367..2370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2367-2370)
  on lines 2372..2374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2372-2374)
  on lines 2376..2378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2376-2378)
  on lines 2380..2381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2380-2381)
  on lines 2386..2389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2386-2389)
  on lines 2391..2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2391-2393)
  on lines 2395..2397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2395-2397)
  on lines 2399..2400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2399-2400)
  on lines 2405..2406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2405-2406)
  on line 2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2410-2410)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 2084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2084-2084)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2493-2493)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2975-2975)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2760..2762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2760-2762)
  on lines 2764..2765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2764-2765)
  on lines 2769..2772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2769-2772)
  on lines 2774..2776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2774-2776)
  on lines 2778..2779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2778-2779)
  on lines 2783..2786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2783-2786)
  on lines 2788..2790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2788-2790)
  on lines 2792..2793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2792-2793)
  on lines 2797..2798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2797-2798)
  on line 2802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2802-2802)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2582..2583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2582-2583)
  on line 2587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2587-2587)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2653..2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2653-2655)
  on lines 2657..2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2657-2658)
  on lines 2662..2665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2662-2665)
  on lines 2667..2669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2667-2669)
  on lines 2671..2672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2671-2672)
  on lines 2676..2679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2676-2679)
  on lines 2681..2683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2681-2683)
  on lines 2685..2686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2685-2686)
  on lines 2690..2691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2690-2691)
  on line 2695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2695-2695)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2540-2540)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1060..1061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1060-1061)
  on line 1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1067-1067)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1323..1324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1323-1324)
  on line 1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1330-1330)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1097..1098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1097-1098)
  on line 1104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1104-1104)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1793-1793)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1802-1802)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1819..1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1819-1820)
  on line 1827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1827-1827)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1510-1510)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1286..1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1286-1287)
  on line 1293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1293-1293)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1784-1784)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2424..2425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2424-2425)
  on lines 2432..2434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2432-2434)
  on lines 2436..2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2436-2437)
  on lines 2439..2440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2439-2440)
  on lines 2447..2449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2447-2449)
  on lines 2451..2452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2451-2452)
  on lines 2454..2455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2454-2455)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2287..2288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2287-2288)
  on lines 2290..2291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2290-2291)
  on lines 2298..2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2298-2300)
  on lines 2302..2303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2302-2303)
  on lines 2305..2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2305-2306)
  on lines 2313..2315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2313-2315)
  on lines 2317..2318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2317-2318)
  on lines 2320..2321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2320-2321)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 2094..2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2094-2095)
  on lines 2097..2098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2097-2098)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2501-2501)
  on lines 2506..2507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2506-2507)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2867..2868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2867-2868)
  on lines 2878..2879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2878-2879)
  on lines 2889..2890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2889-2890)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2706..2707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2706-2707)
  on lines 2717..2718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2717-2718)
  on lines 2728..2729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2728-2729)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1078-1078)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1378-1378)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1304-1304)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1341-1341)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1115-1115)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1435-1435)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1911-1911)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 560
  dead: 622 (446 in uncalled functions)
  total lines: 1182
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2648:7-2648:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1377:9-1377:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2649:9-2649:19)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring2_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2842:15-2842:52)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2417:7-2417:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2421:11-2421:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2864:9-2864:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2875:11-2875:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2885:11-2885:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2886:13-2886:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2703:9-2703:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2714:11-2714:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2283:7-2283:18)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1818:9-1818:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2284:9-2284:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2091:7-2091:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:420:10-420:11)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2500:7-2500:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2724:11-2724:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2725:13-2725:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2503:9-2503:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2755:7-2755:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2756:9-2756:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1285:9-1285:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2348:7-2348:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2988:11-2988:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1901:7-1901:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2553:11-2553:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2353:11-2353:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1303:9-1303:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1059:9-1059:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2578:11-2578:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1322:9-1322:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1077:9-1077:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:234:7-234:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1340:9-1340:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1096:9-1096:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:2600:11-2600:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product23.cil.c:1114:9-1114:20)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
