./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_product28.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_product28.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_product28.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_product28.cil.c:1180:3-1201:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1237:3-1262:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1322:5-1342: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_product28.cil.c:84:1-111:1)
[Warning][Deadcode] Function 'printMail__wrappee__Encrypt' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:112:1-130:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:131:1-149:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:150:1-163:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:193:1-201:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:222:1-231:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:418:1-432:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:446:1-455:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:465:1-473:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:474:1-482:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:704:1-714:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:793:1-804:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:805:1-816:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1109:1-1154:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1155:1-1210:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1211:1-1270:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1273:1-1375:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1376:1-1421:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1422:1-1467:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1470:1-1484:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1504:1-1518:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1522:1-1547:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1548:1-1567:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1572:1-1595:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1596:1-1615:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1619:1-1642:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1643:1-1662:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1663:1-1687:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1697:1-1765:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1766:1-1834:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1835:1-1890:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1900:1-1968:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:1969:1-2024:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2028:1-2051:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2052:1-2071:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2463:1-2486:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2487:1-2506:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2562:1-2576:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2579:1-2597:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2598:1-2613:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2690:1-2710:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2711:1-2726:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2729:1-2749:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2750:1-2765:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2916:1-2934:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:54-54)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 696..698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:696-698)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2188-2188)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:214-214)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2371..2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2371-2372)
  on lines 2385..2386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2385-2386)
  on lines 2393..2396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2393-2396)
  on lines 2398..2400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2398-2400)
  on lines 2402..2403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2402-2403)
  on lines 2407..2408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2407-2408)
  on line 2412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2412-2412)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2518..2520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2518-2520)
  on lines 2522..2524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2522-2524)
  on lines 2526..2527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2526-2527)
  on line 2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2531-2531)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2316..2318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2316-2318)
  on lines 2320..2321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2320-2321)
  on lines 2325..2328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2325-2328)
  on lines 2330..2332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2330-2332)
  on lines 2334..2335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2334-2335)
  on lines 2339..2342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2339-2342)
  on lines 2344..2346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2344-2346)
  on lines 2348..2349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2348-2349)
  on lines 2353..2354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2353-2354)
  on line 2358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2358-2358)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2138..2139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2138-2139)
  on line 2143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2143-2143)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2209..2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2209-2211)
  on lines 2213..2214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2213-2214)
  on lines 2218..2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2218-2221)
  on lines 2223..2225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2223-2225)
  on lines 2227..2228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2227-2228)
  on lines 2232..2235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2232-2235)
  on lines 2237..2239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2237-2239)
  on lines 2241..2242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2241-2242)
  on lines 2246..2247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2246-2247)
  on line 2251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2251-2251)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2087..2089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2087-2089)
  on lines 2091..2092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2091-2092)
  on line 2096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2096-2096)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2813..2815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2813-2815)
  on lines 2817..2818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2817-2818)
  on line 2821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2821-2821)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2624..2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2624-2626)
  on lines 2628..2629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2628-2629)
  on line 2632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2632-2632)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2887..2889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2887-2889)
  on lines 2891..2892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2891-2892)
  on line 2895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2895-2895)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2661..2663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2661-2663)
  on lines 2665..2666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2665-2666)
  on line 2669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2669-2669)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2776..2778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2776-2778)
  on lines 2780..2781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2780-2781)
  on line 2784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2784-2784)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 497..498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:497-498)
  on line 505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:505-505)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:190-190)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:170-170)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2850..2852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2850-2852)
  on lines 2854..2855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2854-2855)
  on line 2858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2858-2858)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:462-462)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2423..2424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2423-2424)
  on lines 2434..2435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2434-2435)
  on lines 2445..2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2445-2446)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2262..2263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2262-2263)
  on lines 2273..2274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2273-2274)
  on lines 2284..2285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2284-2285)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on lines 2831..2832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2831-2832)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 2642..2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2642-2643)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on lines 2794..2795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2794-2795)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on lines 2942..2943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2942-2943)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on lines 2868..2869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2868-2869)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on lines 2905..2906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2905-2906)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 2679..2680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2679-2680)
[Warning][Deadcode] Function 'sign' has dead code:
  on line 528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:528-528)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:252-252)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:563-563)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 432
  dead: 720 (557 in uncalled functions)
  total lines: 1152
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:911:10-911:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2828:7-2828:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2134:11-2134:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2846:7-2846:18)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2370:11-2370:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2156:11-2156:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2379:9-2379:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2865:7-2865:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2620:7-2620:18)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring1_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2384:13-2384:50)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:692:7-692:14)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2883:7-2883:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2639:7-2639:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2204:7-2204:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2205:9-2205:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2902:7-2902:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2657:7-2657:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2420:9-2420:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2676:7-2676:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2431:11-2431:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:748:7-748:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2939:7-2939:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2441:11-2441:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2442:13-2442:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2259:9-2259:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2270:11-2270:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2280:11-2280:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2281:13-2281:23)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:496:9-496:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2514:7-2514:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2311:7-2311:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2312:9-2312:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2772:7-2772:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2083:9-2083:20)
[Warning][Deadcode][CWE-570] condition '! privkey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:527:7-527:16)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2791:7-2791:18)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:560:9-560:16)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2544:11-2544:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2809:7-2809:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product28.cil.c:2109:11-2109:22)
[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
