./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_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_spec9_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_spec9_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_spec9_product32.cil.c:2512:3-2533:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2569:3-2594:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2654:5-2674: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_spec9_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_spec9_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_spec9_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_spec9_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_spec9_product32.cil.c:184:1-192:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:668:1-682:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:867:1-881:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:884:1-902:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:903:1-918:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:995:1-1015:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1016:1-1031:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1034:1-1054:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1055:1-1070:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1221:1-1239:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1258:1-1272:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1295:1-1309:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1313:1-1338:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1339:1-1358:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1363:1-1386:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1387:1-1406:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1454:1-1478:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1488:1-1556:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1557:1-1625:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2254:1-2277:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2278:1-2297:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2350:1-2359:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2441:1-2486:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2487:1-2542:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2543:1-2602:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2605:1-2707:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2708:1-2753:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2754:1-2799:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2898:1-2908:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2987:1-2998:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2999:1-3010:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2389-2389)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1979-1979)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:205-205)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2203-2203)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1704..1706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1704-1706)
  on lines 1708..1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1708-1709)
  on lines 1714..1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1714-1717)
  on lines 1719..1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1719-1721)
  on lines 1723..1725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1723-1725)
  on lines 1727..1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1727-1728)
  on lines 1733..1736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1733-1736)
  on lines 1738..1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1738-1740)
  on lines 1742..1744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1742-1744)
  on lines 1746..1747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1746-1747)
  on lines 1752..1753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1752-1753)
  on line 1757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1757-1757)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1431-1431)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1840-1840)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2322-2322)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2107..2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2107-2109)
  on lines 2111..2112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2111-2112)
  on lines 2116..2119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2116-2119)
  on lines 2121..2123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2121-2123)
  on lines 2125..2126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2125-2126)
  on lines 2130..2133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2130-2133)
  on lines 2135..2137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2135-2137)
  on lines 2139..2140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2139-2140)
  on lines 2144..2145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2144-2145)
  on line 2149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2149-2149)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1929..1930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1929-1930)
  on line 1934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1934-1934)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2000..2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2000-2002)
  on lines 2004..2005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2004-2005)
  on lines 2009..2012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2009-2012)
  on lines 2014..2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2014-2016)
  on lines 2018..2019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2018-2019)
  on lines 2023..2026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2023-2026)
  on lines 2028..2030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2028-2030)
  on lines 2032..2033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2032-2033)
  on lines 2037..2038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2037-2038)
  on line 2042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2042-2042)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1887-1887)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1119..1120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1119-1120)
  on line 1126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1126-1126)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 930..931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:930-931)
  on line 937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:937-937)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1193..1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1193-1194)
  on line 1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1200-1200)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 967..968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:967-968)
  on line 974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:974-974)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:721-721)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:730-730)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1082..1083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1082-1083)
  on line 1089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1089-1089)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 747..748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:747-748)
  on line 755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:755-755)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_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_spec9_product32.cil.c:161-161)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1156..1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1156-1157)
  on line 1163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1163-1163)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:712-712)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1771..1772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1771-1772)
  on lines 1779..1781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1779-1781)
  on lines 1783..1784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1783-1784)
  on lines 1786..1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1786-1787)
  on lines 1794..1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1794-1796)
  on lines 1798..1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1798-1799)
  on lines 1801..1802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1801-1802)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1634..1635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1634-1635)
  on lines 1637..1638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1637-1638)
  on lines 1645..1647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1645-1647)
  on lines 1649..1650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1649-1650)
  on lines 1652..1653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1652-1653)
  on lines 1660..1662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1660-1662)
  on lines 1664..1665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1664-1665)
  on lines 1667..1668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1667-1668)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1441..1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1441-1442)
  on lines 1444..1445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1444-1445)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1848-1848)
  on lines 1853..1854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1853-1854)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2214..2215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2214-2215)
  on lines 2225..2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2225-2226)
  on lines 2236..2237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2236-2237)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2053..2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2053-2054)
  on lines 2064..2065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2064-2065)
  on lines 2075..2076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2075-2076)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1137-1137)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:948-948)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1100-1100)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1248-1248)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1174-1174)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1211-1211)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:985-985)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2380-2380)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 610
  dead: 608 (426 in uncalled functions)
  total lines: 1218
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1764:7-1764:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1768:11-1768:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:258:10-258:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2211:9-2211:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1099:9-1099:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2222:11-2222:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1118:9-1118:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2232:11-2232:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2233:13-2233:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1136:9-1136:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2050:9-2050:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1155:9-1155:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2061:11-2061:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1630:7-1630:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1631:9-1631:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1438:7-1438:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1847:7-1847:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2071:11-2071:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1173:9-1173:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2072:13-2072:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:929:9-929:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1850:9-1850:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2102:7-2102:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1192:9-1192:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2103:9-2103:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:947:9-947:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1210:9-1210:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:966:9-966:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2942:7-2942:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1695:7-1695:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:2335:11-2335:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1900:11-1900:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:984:9-984:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1700:11-1700:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1247:9-1247:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1925:11-1925:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:746:9-746:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1947:11-1947:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1995:7-1995:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1996:9-1996:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product32.cil.c:1081:9-1081: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
