./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_spec1_product32.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_spec1_product32.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_spec1_product32.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_spec1_product32.cil.c:1280:3-1301:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1337:3-1362:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1422:5-1442: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 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:64:1-73:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:566:1-580:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:767:1-781:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:784:1-802:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:803:1-818:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:895:1-915:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:916:1-931:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:934:1-954:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:955:1-970:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1121:1-1139:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1187:1-1201:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1209:1-1254:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1255:1-1310:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1311:1-1370:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1373:1-1475:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1476:1-1521:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1522:1-1567:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1590:1-1604:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1608:1-1633:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1634:1-1653:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1658:1-1681:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1682:1-1701:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1749:1-1773:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1783:1-1851:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1852:1-1920:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2549:1-2572:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2573:1-2592:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2643:1-2670:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2671:1-2689:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2690:1-2708:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2709:1-2722:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2752:1-2760:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2874:1-2884:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2963:1-2974:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2975:1-2986:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:3070-3070)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2274-2274)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2773-2773)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2498-2498)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1999..2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1999-2001)
  on lines 2003..2004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2003-2004)
  on lines 2009..2012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2009-2012)
  on lines 2014..2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2014-2016)
  on lines 2018..2020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2018-2020)
  on lines 2022..2023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2022-2023)
  on lines 2028..2031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2028-2031)
  on lines 2033..2035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2033-2035)
  on lines 2037..2039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2037-2039)
  on lines 2041..2042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2041-2042)
  on lines 2047..2048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2047-2048)
  on line 2052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2052-2052)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1726-1726)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2135-2135)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2617-2617)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2402..2404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2402-2404)
  on lines 2406..2407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2406-2407)
  on lines 2411..2414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2411-2414)
  on lines 2416..2418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2416-2418)
  on lines 2420..2421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2420-2421)
  on lines 2425..2428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2425-2428)
  on lines 2430..2432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2430-2432)
  on lines 2434..2435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2434-2435)
  on lines 2439..2440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2439-2440)
  on line 2444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2444-2444)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2224..2225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2224-2225)
  on line 2229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2229-2229)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2295..2297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2295-2297)
  on lines 2299..2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2299-2300)
  on lines 2304..2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2304-2307)
  on lines 2309..2311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2309-2311)
  on lines 2313..2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2313-2314)
  on lines 2318..2321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2318-2321)
  on lines 2323..2325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2323-2325)
  on lines 2327..2328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2327-2328)
  on lines 2332..2333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2332-2333)
  on line 2337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2337-2337)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2182-2182)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1019..1020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1019-1020)
  on line 1026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1026-1026)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 830..831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:830-831)
  on line 837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:837-837)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1093..1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1093-1094)
  on line 1100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1100-1100)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 867..868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:867-868)
  on line 874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:874-874)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:619-619)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:628-628)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 982..983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:982-983)
  on line 989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:989-989)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 645..646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:645-646)
  on line 653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:653-653)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2749-2749)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2729-2729)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1056..1057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1056-1057)
  on line 1063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1063-1063)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:610-610)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2066..2067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2066-2067)
  on lines 2074..2076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2074-2076)
  on lines 2078..2079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2078-2079)
  on lines 2081..2082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2081-2082)
  on lines 2089..2091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2089-2091)
  on lines 2093..2094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2093-2094)
  on lines 2096..2097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2096-2097)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1929..1930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1929-1930)
  on lines 1932..1933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1932-1933)
  on lines 1940..1942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1940-1942)
  on lines 1944..1945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1944-1945)
  on lines 1947..1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1947-1948)
  on lines 1955..1957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1955-1957)
  on lines 1959..1960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1959-1960)
  on lines 1962..1963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1962-1963)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1736..1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1736-1737)
  on lines 1739..1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1739-1740)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2143-2143)
  on lines 2148..2149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2148-2149)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2509..2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2509-2510)
  on lines 2520..2521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2520-2521)
  on lines 2531..2532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2531-2532)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2348..2349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2348-2349)
  on lines 2359..2360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2359-2360)
  on lines 2370..2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2370-2371)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1037-1037)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:848-848)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1000-1000)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1148-1148)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1074-1074)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1111-1111)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:885-885)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 94 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:94-94)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 602
  dead: 608 (426 in uncalled functions)
  total lines: 1210
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1092:9-1092:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2517:11-2517:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:847:9-847:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2527:11-2527:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2528:13-2528:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1110:9-1110:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:866:9-866:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2345:9-2345:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:884:9-884:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2356:11-2356:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1147:9-1147:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1925:7-1925:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1926:9-1926:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1733:7-1733:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2142:7-2142:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2366:11-2366:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2367:13-2367:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2145:9-2145:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:644:9-644:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2397:7-2397:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2398:9-2398:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2918:7-2918:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1990:7-1990:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2630:11-2630:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2195:11-2195:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1995:11-1995:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:981:9-981:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2220:11-2220:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:147:10-147:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:999:9-999:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1018:9-1018:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2242:11-2242:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1036:9-1036:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2290:7-2290:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2291:9-2291:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1055:9-1055:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2059:7-2059:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2063:11-2063:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:1073:9-1073:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:829:9-829:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product32.cil.c:2506:9-2506:19)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
