./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_product17.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_product17.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_product17.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_product17.cil.c:481:3-502:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:538:3-563:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:623:5-643: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_product17.cil.c:188:1-198:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:277:1-288:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:289:1-300:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:370:1-379:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:410:1-455:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:456:1-511:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:512:1-571:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:574:1-676:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:677:1-722:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:723:1-768:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1122:1-1136:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1150:1-1159:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1169:1-1177:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1178:1-1186:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1306:1-1320:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1394:1-1408:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1412:1-1437:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1438:1-1457:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1462:1-1485:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1486:1-1505:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1553:1-1577:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1587:1-1655:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1656:1-1724:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1918:1-1941:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1942:1-1961:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2353:1-2376:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2377:1-2396:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2449:1-2476:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2477:1-2495:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2496:1-2509:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2519:1-2527:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2555:1-2569:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2572:1-2590:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2591:1-2606:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2683:1-2703:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2704:1-2719:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2722:1-2742:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2743:1-2758:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2761:1-2779:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2780:1-2795:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2798:1-2816:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2817:1-2832:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2909:1-2927:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2950-2950)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 180..182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:180-182)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2078-2078)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2540-2540)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2256..2258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2256-2258)
  on lines 2260..2262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2260-2262)
  on lines 2264..2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2264-2265)
  on lines 2275..2276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2275-2276)
  on lines 2289..2290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2289-2290)
  on line 2302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2302-2302)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1803..1805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1803-1805)
  on lines 1807..1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1807-1808)
  on lines 1813..1816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1813-1816)
  on lines 1818..1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1818-1820)
  on lines 1822..1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1822-1824)
  on lines 1826..1827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1826-1827)
  on lines 1832..1835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1832-1835)
  on lines 1837..1839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1837-1839)
  on lines 1841..1843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1841-1843)
  on lines 1845..1846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1845-1846)
  on lines 1851..1852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1851-1852)
  on line 1856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1856-1856)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 1517..1519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1517-1519)
  on lines 1521..1523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1521-1523)
  on lines 1525..1526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1525-1526)
  on line 1530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1530-1530)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2408..2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2408-2410)
  on lines 2412..2414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2412-2414)
  on lines 2416..2417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2416-2417)
  on line 2421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2421-2421)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2206..2208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2206-2208)
  on lines 2210..2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2210-2211)
  on lines 2215..2218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2215-2218)
  on lines 2220..2222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2220-2222)
  on lines 2224..2225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2224-2225)
  on lines 2229..2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2229-2232)
  on lines 2234..2236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2234-2236)
  on lines 2238..2239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2238-2239)
  on lines 2243..2244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2243-2244)
  on line 2248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2248-2248)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2028..2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2028-2029)
  on line 2033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2033-2033)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2099..2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2099-2101)
  on lines 2103..2104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2103-2104)
  on lines 2108..2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2108-2111)
  on lines 2113..2115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2113-2115)
  on lines 2117..2118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2117-2118)
  on lines 2122..2125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2122-2125)
  on lines 2127..2129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2127-2129)
  on lines 2131..2132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2131-2132)
  on lines 2136..2137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2136-2137)
  on line 2141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2141-2141)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1973..1975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1973-1975)
  on lines 1977..1979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1977-1979)
  on lines 1981..1982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1981-1982)
  on line 1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1986-1986)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2617..2619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2617-2619)
  on lines 2621..2622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2621-2622)
  on line 2625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2625-2625)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2880..2882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2880-2882)
  on lines 2884..2885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2884-2885)
  on line 2888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2888-2888)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2654..2656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2654-2656)
  on lines 2658..2659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2658-2659)
  on line 2662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2662-2662)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1197..1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1197-1198)
  on lines 1201..1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1201-1202)
  on line 1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1209-1209)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2516-2516)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2843..2845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2843-2845)
  on lines 2847..2848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2847-2848)
  on line 2851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2851-2851)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1166-1166)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1870..1871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1870-1871)
  on lines 1878..1880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1878-1880)
  on lines 1882..1883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1882-1883)
  on lines 1885..1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1885-1886)
  on lines 1893..1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1893-1895)
  on lines 1897..1898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1897-1898)
  on lines 1900..1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1900-1901)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1733..1734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1733-1734)
  on lines 1736..1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1736-1737)
  on lines 1744..1746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1744-1746)
  on lines 1748..1749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1748-1749)
  on lines 1751..1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1751-1752)
  on lines 1759..1761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1759-1761)
  on lines 1763..1764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1763-1764)
  on lines 1766..1767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1766-1767)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1540..1541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1540-1541)
  on lines 1543..1544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1543-1544)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2313..2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2313-2314)
  on lines 2324..2325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2324-2325)
  on lines 2335..2336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2335-2336)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2152..2153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2152-2153)
  on lines 2163..2164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2163-2164)
  on lines 2174..2175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2174-2175)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 2635..2636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2635-2636)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on lines 2935..2936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2935-2936)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on lines 2861..2862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2861-2862)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on lines 2898..2899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2898-2899)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 2672..2673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2672-2673)
[Warning][Deadcode] Function 'sign' has dead code:
  on line 1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1239-1239)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:400-400)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1276-1276)
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1279-1279)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 457
  dead: 703 (475 in uncalled functions)
  total lines: 1160
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1867:11-1867:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2310:9-2310:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2839:7-2839:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2321:11-2321:21)
[Warning][Deadcode][CWE-570] condition '! publicKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1196:7-1196:18)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1200:9-1200:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2331:11-2331:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2332:13-2332:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2858:7-2858:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2613:7-2613:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1513:7-1513:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2876:7-2876:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2149:9-2149:19)
[Warning][Deadcode][CWE-570] condition '! privkey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1238:7-1238:16)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2632:7-2632:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2160:11-2160:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2895:7-2895:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2650:7-2650:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1729:7-1729:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1730:9-1730:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1537:7-1537:18)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1269:7-1269:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2170:11-2170:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2171:13-2171:23)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1273:9-1273:16)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2404:7-2404:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2201:7-2201:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2669:7-2669:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2202:9-2202:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1969:7-1969:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2932:7-2932:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1794:7-1794:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2434:11-2434:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1999:11-1999:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1799:11-1799:21)
[Warning][Deadcode][CWE-571] condition 'sent_signed == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1351:7-1351:23)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:176:7-176:14)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2024:11-2024:22)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2255:7-2255: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_product17.cil.c:809:10-809:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2046:11-2046:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:232:7-232:10)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring1_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2274:13-2274:50)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2094:7-2094:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:2095:9-2095: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_product17.cil.c:2288:15-2288:52)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product17.cil.c:1863:7-1863:18)
[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
