./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_spec7_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_spec7_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_spec7_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_spec7_product32.cil.c:1183:3-1204:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1240:3-1265:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1325:5-1345: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 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:75:1-102:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:103:1-121:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:122:1-140:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:141:1-154:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:184:1-192:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:210:1-224:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:230:1-239:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:495:1-509:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:716:1-730:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:733:1-751:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:752:1-767:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:844:1-864:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:865:1-880:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:883:1-903:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:904:1-919:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1070:1-1088:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1112:1-1157:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1158:1-1213:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1214:1-1273:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1276:1-1378:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1379:1-1424:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1425:1-1470:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1722:1-1736:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1740:1-1765:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1766:1-1785:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1790:1-1813:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1814:1-1833:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1881:1-1905:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1915:1-1983:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1984:1-2052:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2681:1-2704:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2705:1-2724:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2870:1-2880:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2959:1-2970:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2971:1-2982:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:269-269)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2406-2406)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:205-205)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2630-2630)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2131..2133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2131-2133)
  on lines 2135..2136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2135-2136)
  on lines 2141..2144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2141-2144)
  on lines 2146..2148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2146-2148)
  on lines 2150..2152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2150-2152)
  on lines 2154..2155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2154-2155)
  on lines 2160..2163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2160-2163)
  on lines 2165..2167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2165-2167)
  on lines 2169..2171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2169-2171)
  on lines 2173..2174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2173-2174)
  on lines 2179..2180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2179-2180)
  on line 2184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2184-2184)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1858-1858)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2267-2267)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2749-2749)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2534..2536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2534-2536)
  on lines 2538..2539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2538-2539)
  on lines 2543..2546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2543-2546)
  on lines 2548..2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2548-2550)
  on lines 2552..2553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2552-2553)
  on lines 2557..2560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2557-2560)
  on lines 2562..2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2562-2564)
  on lines 2566..2567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2566-2567)
  on lines 2571..2572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2571-2572)
  on line 2576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2576-2576)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2356..2357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2356-2357)
  on line 2361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2361-2361)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2427..2429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2427-2429)
  on lines 2431..2432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2431-2432)
  on lines 2436..2439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2436-2439)
  on lines 2441..2443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2441-2443)
  on lines 2445..2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2445-2446)
  on lines 2450..2453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2450-2453)
  on lines 2455..2457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2455-2457)
  on lines 2459..2460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2459-2460)
  on lines 2464..2465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2464-2465)
  on line 2469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2469-2469)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2314-2314)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 968..969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:968-969)
  on line 975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:975-975)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 779..780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:779-780)
  on line 786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:786-786)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1042..1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1042-1043)
  on line 1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1049-1049)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 816..817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:816-817)
  on line 823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:823-823)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:548-548)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:557-557)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 931..932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:931-932)
  on line 938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:938-938)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 574..575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:574-575)
  on line 582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:582-582)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:181-181)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:161-161)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1005..1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1005-1006)
  on line 1012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1012-1012)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:539-539)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2198..2199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2198-2199)
  on lines 2206..2208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2206-2208)
  on lines 2210..2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2210-2211)
  on lines 2213..2214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2213-2214)
  on lines 2221..2223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2221-2223)
  on lines 2225..2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2225-2226)
  on lines 2228..2229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2228-2229)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2061..2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2061-2062)
  on lines 2064..2065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2064-2065)
  on lines 2072..2074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2072-2074)
  on lines 2076..2077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2076-2077)
  on lines 2079..2080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2079-2080)
  on lines 2087..2089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2087-2089)
  on lines 2091..2092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2091-2092)
  on lines 2094..2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2094-2095)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1868..1869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1868-1869)
  on lines 1871..1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1871-1872)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2275-2275)
  on lines 2280..2281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2280-2281)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2641..2642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2641-2642)
  on lines 2652..2653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2652-2653)
  on lines 2663..2664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2663-2664)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2480..2481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2480-2481)
  on lines 2491..2492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2491-2492)
  on lines 2502..2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2502-2503)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:986-986)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:797-797)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:949-949)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1097-1097)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1023-1023)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1060-1060)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:834-834)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:260-260)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 598
  dead: 608 (426 in uncalled functions)
  total lines: 1206
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:573:9-573:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2762:11-2762:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2327:11-2327:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2127:11-2127:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2352:11-2352:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2374:11-2374:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:930:9-930:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2422:7-2422:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2423:9-2423:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1521:10-1521:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:948:9-948:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2191:7-2191:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2195:11-2195:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:967:9-967:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2914:7-2914:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2638:9-2638:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2649:11-2649:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:985:9-985:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2659:11-2659:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2660:13-2660:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1004:9-1004:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2477:9-2477:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1022:9-1022:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:778:9-778:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2488:11-2488:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1041:9-1041:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2057:7-2057:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2058:9-2058:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1865:7-1865:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2274:7-2274:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2498:11-2498:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:796:9-796:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2499:13-2499:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2277:9-2277:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1059:9-1059:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2529:7-2529:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:815:9-815:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2530:9-2530:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:833:9-833:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:1096:9-1096:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product32.cil.c:2122:7-2122: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
