./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_spec9_product26.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_spec9_product26.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_spec9_product26.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_spec9_product26.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:268:5-288: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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:558:1-568:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:647:1-658:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:659:1-670:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1068:1-1076:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1103:1-1112:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1355:1-1369:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1533:1-1547:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1562:1-1576:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1598:1-1613:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1690:1-1710:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1711:1-1726:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1729:1-1749:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1750:1-1765:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1842:1-1860:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1861:1-1876:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1879:1-1897:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1898:1-1913:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1916:1-1934:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1935:1-1950:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1961:1-1975:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1979:1-2004:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2005:1-2024:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2029:1-2052:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2053:1-2072:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2120:1-2144:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2154:1-2222:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2223:1-2291:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1098-1098)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2645-2645)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1089-1089)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2869-2869)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2370..2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2370-2372)
  on lines 2374..2375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2374-2375)
  on lines 2380..2383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2380-2383)
  on lines 2385..2387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2385-2387)
  on lines 2389..2391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2389-2391)
  on lines 2393..2394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2393-2394)
  on lines 2399..2402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2399-2402)
  on lines 2404..2406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2404-2406)
  on lines 2408..2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2408-2410)
  on lines 2412..2413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2412-2413)
  on lines 2418..2419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2418-2419)
  on line 2423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2423-2423)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 2097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2097-2097)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2506-2506)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2941-2941)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2988-2988)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2773..2775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2773-2775)
  on lines 2777..2778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2777-2778)
  on lines 2782..2785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2782-2785)
  on lines 2787..2789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2787-2789)
  on lines 2791..2792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2791-2792)
  on lines 2796..2799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2796-2799)
  on lines 2801..2803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2801-2803)
  on lines 2805..2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2805-2806)
  on lines 2810..2811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2810-2811)
  on line 2815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2815-2815)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2595..2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2595-2596)
  on line 2600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2600-2600)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2666..2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2666-2668)
  on lines 2670..2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2670-2671)
  on lines 2675..2678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2675-2678)
  on lines 2680..2682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2680-2682)
  on lines 2684..2685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2684-2685)
  on lines 2689..2692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2689-2692)
  on lines 2694..2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2694-2696)
  on lines 2698..2699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2698-2699)
  on lines 2703..2704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2703-2704)
  on line 2708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2708-2708)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2553-2553)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1814..1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1814-1815)
  on line 1821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1821-1821)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1625..1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1625-1626)
  on line 1632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1632-1632)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1588..1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1588-1589)
  on line 1595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1595-1595)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1662..1663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1662-1663)
  on line 1669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1669-1669)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1408-1408)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1417-1417)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1777..1778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1777-1778)
  on line 1784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1784-1784)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1434..1435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1434-1435)
  on line 1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1442-1442)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1065-1065)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1045-1045)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1399-1399)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2437..2438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2437-2438)
  on lines 2445..2447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2445-2447)
  on lines 2449..2450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2449-2450)
  on lines 2452..2453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2452-2453)
  on lines 2460..2462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2460-2462)
  on lines 2464..2465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2464-2465)
  on lines 2467..2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2467-2468)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2300..2301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2300-2301)
  on lines 2303..2304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2303-2304)
  on lines 2311..2313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2311-2313)
  on lines 2315..2316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2315-2316)
  on lines 2318..2319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2318-2319)
  on lines 2326..2328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2326-2328)
  on lines 2330..2331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2330-2331)
  on lines 2333..2334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2333-2334)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 2107..2108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2107-2108)
  on lines 2110..2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2110-2111)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2514-2514)
  on lines 2519..2520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2519-2520)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2949-2949)
  on lines 2954..2955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2954-2955)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2880..2881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2880-2881)
  on lines 2891..2892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2891-2892)
  on lines 2902..2903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2902-2903)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2719..2720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2719-2720)
  on lines 2730..2731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2730-2731)
  on lines 2741..2742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2741-2742)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1832-1832)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1643-1643)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1795-1795)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1680-1680)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1133-1133)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 613
  dead: 577 (397 in uncalled functions)
  total lines: 1190
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2661:7-2661:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2662:9-2662:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:602:7-602:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2430:7-2430:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2434:11-2434:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1776:9-1776:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2877:9-2877:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2888:11-2888:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1794:9-1794:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2898:11-2898:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2899:13-2899:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1813:9-1813:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2716:9-2716:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1831:9-1831:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1587:9-1587:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2727:11-2727:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2296:7-2296:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2948:7-2948:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2297:9-2297:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2104:7-2104:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2513:7-2513:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2737:11-2737:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2951:9-2951:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2738:13-2738:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2516:9-2516:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1624:9-1624:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2768:7-2768:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2769:9-2769:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1642:9-1642:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1661:9-1661:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:798:10-798:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2361:7-2361:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:3001:11-3001:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2566:11-2566:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2366:11-2366:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1679:9-1679:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2591:11-2591:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:1433:9-1433:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product26.cil.c:2613:11-2613: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
