./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_product34.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_product34.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_product34.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_product34.cil.c:987:3-1008:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1044:3-1069:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1129:5-1149: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 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:466:1-474:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:492:1-506:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:520:1-534:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:556:1-571:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:648:1-668:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:669:1-684:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:687:1-707:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:708:1-723:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:916:1-961:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:962:1-1017:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1018:1-1077:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1080:1-1182:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1183:1-1228:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1229:1-1274:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1305:1-1319:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1323:1-1348:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1349:1-1368:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1373:1-1396:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1397:1-1416:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1464:1-1488:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1498:1-1566:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1567:1-1635:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1829:1-1852:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1853:1-1872:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2573:1-2587:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2766:1-2775:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2897:1-2907:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2986:1-2997:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2998:1-3009:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:340-340)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1989-1989)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:487-487)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2213-2213)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1714..1716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1714-1716)
  on lines 1718..1719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1718-1719)
  on lines 1724..1727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1724-1727)
  on lines 1729..1731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1729-1731)
  on lines 1733..1735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1733-1735)
  on lines 1737..1738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1737-1738)
  on lines 1743..1746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1743-1746)
  on lines 1748..1750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1748-1750)
  on lines 1752..1754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1752-1754)
  on lines 1756..1757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1756-1757)
  on lines 1762..1763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1762-1763)
  on line 1767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1767-1767)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 1433..1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1433-1434)
  on line 1441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1441-1441)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2269..2270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2269-2270)
  on line 2285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2285-2285)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2324..2325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2324-2325)
  on line 2332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2332-2332)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2117..2119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2117-2119)
  on lines 2121..2122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2121-2122)
  on lines 2126..2129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2126-2129)
  on lines 2131..2133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2131-2133)
  on lines 2135..2136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2135-2136)
  on lines 2140..2143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2140-2143)
  on lines 2145..2147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2145-2147)
  on lines 2149..2150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2149-2150)
  on lines 2154..2155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2154-2155)
  on line 2159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2159-2159)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1939..1940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1939-1940)
  on line 1944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1944-1944)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2010..2012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2010-2012)
  on lines 2014..2015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2014-2015)
  on lines 2019..2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2019-2022)
  on lines 2024..2026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2024-2026)
  on lines 2028..2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2028-2029)
  on lines 2033..2036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2033-2036)
  on lines 2038..2040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2038-2040)
  on lines 2042..2043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2042-2043)
  on lines 2047..2048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2047-2048)
  on line 2052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2052-2052)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1897-1897)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 772..773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:772-773)
  on line 779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:779-779)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 583..584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:583-584)
  on line 590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:590-590)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 546..547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:546-547)
  on line 553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:553-553)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 846..847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:846-847)
  on line 853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:853-853)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 620..621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:620-621)
  on line 627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:627-627)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2626-2626)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2635-2635)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 735..736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:735-736)
  on line 742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:742-742)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2652..2653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2652-2653)
  on line 2660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2660-2660)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:463-463)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:443-443)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 809..810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:809-810)
  on line 816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:816-816)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 883..884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:883-884)
  on line 890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:890-890)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2617-2617)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1781..1782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1781-1782)
  on lines 1789..1791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1789-1791)
  on lines 1793..1794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1793-1794)
  on lines 1796..1797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1796-1797)
  on lines 1804..1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1804-1806)
  on lines 1808..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1808-1809)
  on lines 1811..1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1811-1812)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1644..1645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1644-1645)
  on lines 1647..1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1647-1648)
  on lines 1655..1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1655-1657)
  on lines 1659..1660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1659-1660)
  on lines 1662..1663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1662-1663)
  on lines 1670..1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1670-1672)
  on lines 1674..1675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1674-1675)
  on lines 1677..1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1677-1678)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1451..1452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1451-1452)
  on lines 1454..1455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1454-1455)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2293-2293)
  on lines 2298..2299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2298-2299)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2224..2225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2224-2225)
  on lines 2235..2236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2235-2236)
  on lines 2246..2247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2246-2247)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2063..2064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2063-2064)
  on lines 2074..2075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2074-2075)
  on lines 2085..2086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2085-2086)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:790-790)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:601-601)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:753-753)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:901-901)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:827-827)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:864-864)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:638-638)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2796-2796)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 656
  dead: 568 (374 in uncalled functions)
  total lines: 1224
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:771:9-771:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2005:7-2005:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2006:9-2006:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1774:7-1774:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1778:11-1778:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:789:9-789:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:545:9-545:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2221:9-2221:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:808:9-808:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2232:11-2232:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2242:11-2242:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2243:13-2243:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:826:9-826:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:582:9-582:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2268:7-2268:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:845:9-845:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2060:9-2060:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:600:9-600:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1432:11-1432:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2071:11-2071:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:863:9-863:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:619:9-619:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1640:7-1640:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2292:7-2292:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1641:9-1641:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1448:7-1448:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2081:11-2081:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2295:9-2295:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2082:13-2082:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:882:9-882:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:637:9-637:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2112:7-2112:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2113:9-2113:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2941:7-2941:10)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:98:10-98:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:900:9-900:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2323:11-2323:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2651:9-2651:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1705:7-1705:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:2345:11-2345:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1910:11-1910:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1710:11-1710:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1935:11-1935:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:734:9-734:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:1957:11-1957:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product34.cil.c:752:9-752:20)
[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
