./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_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_spec7_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_spec7_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_spec7_product34.cil.c:634:3-655:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:691:3-716:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:776:5-796: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 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:190:1-200:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:279:1-290:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:291:1-302:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:504:1-512:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:563:1-608:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:609:1-664:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:665:1-724:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:727:1-829:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:830:1-875:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:876:1-921:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:935:1-949:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:971:1-986:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1063:1-1083:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1084:1-1099:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1102:1-1122:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1123:1-1138:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1326:1-1335:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1378:1-1392:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1396:1-1421:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1422:1-1441:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1446:1-1469:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1470:1-1489:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1537:1-1561:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1571:1-1639:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1640:1-1708:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1902:1-1925:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1926:1-1945:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2430:1-2444:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2651:1-2665:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:553-553)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2062-2062)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:525-525)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2286-2286)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1787..1789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1787-1789)
  on lines 1791..1792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1791-1792)
  on lines 1797..1800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1797-1800)
  on lines 1802..1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1802-1804)
  on lines 1806..1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1806-1808)
  on lines 1810..1811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1810-1811)
  on lines 1816..1819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1816-1819)
  on lines 1821..1823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1821-1823)
  on lines 1825..1827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1825-1827)
  on lines 1829..1830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1829-1830)
  on lines 1835..1836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1835-1836)
  on line 1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1840-1840)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 1506..1507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1506-1507)
  on line 1514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1514-1514)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2342..2343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2342-2343)
  on line 2358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2358-2358)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2397..2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2397-2398)
  on line 2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2405-2405)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2190..2192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2190-2192)
  on lines 2194..2195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2194-2195)
  on lines 2199..2202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2199-2202)
  on lines 2204..2206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2204-2206)
  on lines 2208..2209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2208-2209)
  on lines 2213..2216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2213-2216)
  on lines 2218..2220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2218-2220)
  on lines 2222..2223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2222-2223)
  on lines 2227..2228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2227-2228)
  on line 2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2232-2232)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2012..2013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2012-2013)
  on line 2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2017-2017)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2083..2085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2083-2085)
  on lines 2087..2088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2087-2088)
  on lines 2092..2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2092-2095)
  on lines 2097..2099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2097-2099)
  on lines 2101..2102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2101-2102)
  on lines 2106..2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2106-2109)
  on lines 2111..2113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2111-2113)
  on lines 2115..2116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2115-2116)
  on lines 2120..2121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2120-2121)
  on line 2125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2125-2125)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1970-1970)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1187..1188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1187-1188)
  on line 1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1194-1194)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 998..999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:998-999)
  on line 1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1005-1005)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 961..962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:961-962)
  on line 968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:968-968)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1261..1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1261-1262)
  on line 1268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1268-1268)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1035..1036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1035-1036)
  on line 1042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1042-1042)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2704-2704)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2713-2713)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1150..1151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1150-1151)
  on line 1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1157-1157)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2730..2731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2730-2731)
  on line 2738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2738-2738)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:501-501)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:481-481)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1224..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1224-1225)
  on line 1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1231-1231)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1298..1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1298-1299)
  on line 1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1305-1305)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2695-2695)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1854..1855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1854-1855)
  on lines 1862..1864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1862-1864)
  on lines 1866..1867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1866-1867)
  on lines 1869..1870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1869-1870)
  on lines 1877..1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1877-1879)
  on lines 1881..1882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1881-1882)
  on lines 1884..1885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1884-1885)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1717..1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1717-1718)
  on lines 1720..1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1720-1721)
  on lines 1728..1730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1728-1730)
  on lines 1732..1733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1732-1733)
  on lines 1735..1736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1735-1736)
  on lines 1743..1745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1743-1745)
  on lines 1747..1748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1747-1748)
  on lines 1750..1751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1750-1751)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1524..1525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1524-1525)
  on lines 1527..1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1527-1528)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2366-2366)
  on lines 2371..2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2371-2372)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2297..2298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2297-2298)
  on lines 2308..2309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2308-2309)
  on lines 2319..2320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2319-2320)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2136..2137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2136-2137)
  on lines 2147..2148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2147-2148)
  on lines 2158..2159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2158-2159)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1205-1205)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1016-1016)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1168-1168)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1316-1316)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1242-1242)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1279-1279)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1053-1053)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1356-1356)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 644
  dead: 568 (374 in uncalled functions)
  total lines: 1212
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2078:7-2078:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2079:9-2079:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1847:7-1847:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1851:11-1851:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1167:9-1167:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2294:9-2294:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1186:9-1186:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2882:10-2882:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2305:11-2305:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2315:11-2315:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2316:13-2316:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1204:9-1204:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:960:9-960:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2341:7-2341:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1223:9-1223:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2133:9-2133:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1505:11-1505:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2144:11-2144:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1241:9-1241:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:997:9-997:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1713:7-1713:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2365:7-2365:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1714:9-1714:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1521:7-1521:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2154:11-2154:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2368:9-2368:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2155:13-2155:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1260:9-1260:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1015:9-1015:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2185:7-2185:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2186:9-2186:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1278:9-1278:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1034:9-1034:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2396:11-2396:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1297:9-1297:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1052:9-1052:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1778:7-1778:18)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2729:9-2729:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2418:11-2418:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1983:11-1983:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1315:9-1315:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1783:11-1783:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2008:11-2008:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:234:7-234:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:2030:11-2030:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product34.cil.c:1149:9-1149: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
