./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_spec27_product17.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_spec27_product17.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_spec27_product17.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_spec27_product17.cil.c:1070:3-1091:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1127:3-1152:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1212:5-1232: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 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:206:1-220:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:234:1-243:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:253:1-261:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:262:1-270:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:502:1-512:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:591:1-602:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:603:1-614:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:717:1-726:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:977:1-991:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:999:1-1044:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1045:1-1100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1101:1-1160:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1163:1-1265:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1266:1-1311:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1312:1-1357:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1372:1-1386:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1390:1-1415:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1416:1-1435:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1440:1-1463:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1464:1-1483:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1531:1-1555:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1565:1-1633:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1634:1-1702:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1896:1-1919:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1920:1-1939:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2331:1-2354:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2355:1-2374:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2426:1-2453:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2454:1-2472:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2473:1-2486:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2496:1-2504:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2532:1-2546:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2549:1-2567:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2568:1-2583:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2660:1-2680:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2681:1-2696:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2699:1-2719:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2720:1-2735:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2738:1-2756:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2757:1-2772:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2775:1-2793:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2794:1-2809:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:972-972)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 494..496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:494-496)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2056-2056)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2517-2517)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2234..2236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2234-2236)
  on lines 2238..2240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2238-2240)
  on lines 2242..2243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2242-2243)
  on lines 2253..2254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2253-2254)
  on lines 2267..2268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2267-2268)
  on line 2280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2280-2280)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1781..1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1781-1783)
  on lines 1785..1786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1785-1786)
  on lines 1791..1794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1791-1794)
  on lines 1796..1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1796-1798)
  on lines 1800..1802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1800-1802)
  on lines 1804..1805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1804-1805)
  on lines 1810..1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1810-1813)
  on lines 1815..1817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1815-1817)
  on lines 1819..1821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1819-1821)
  on lines 1823..1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1823-1824)
  on lines 1829..1830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1829-1830)
  on line 1834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1834-1834)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 1495..1497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1495-1497)
  on lines 1499..1501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1499-1501)
  on lines 1503..1504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1503-1504)
  on line 1508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1508-1508)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2386..2388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2386-2388)
  on lines 2390..2392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2390-2392)
  on lines 2394..2395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2394-2395)
  on line 2399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2399-2399)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2184..2186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2184-2186)
  on lines 2188..2189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2188-2189)
  on lines 2193..2196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2193-2196)
  on lines 2198..2200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2198-2200)
  on lines 2202..2203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2202-2203)
  on lines 2207..2210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2207-2210)
  on lines 2212..2214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2212-2214)
  on lines 2216..2217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2216-2217)
  on lines 2221..2222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2221-2222)
  on line 2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2226-2226)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2006..2007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2006-2007)
  on line 2011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2011-2011)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2077..2079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2077-2079)
  on lines 2081..2082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2081-2082)
  on lines 2086..2089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2086-2089)
  on lines 2091..2093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2091-2093)
  on lines 2095..2096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2095-2096)
  on lines 2100..2103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2100-2103)
  on lines 2105..2107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2105-2107)
  on lines 2109..2110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2109-2110)
  on lines 2114..2115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2114-2115)
  on line 2119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2119-2119)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1951..1953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1951-1953)
  on lines 1955..1957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1955-1957)
  on lines 1959..1960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1959-1960)
  on line 1964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1964-1964)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2594..2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2594-2596)
  on lines 2598..2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2598-2599)
  on line 2602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2602-2602)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2857..2859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2857-2859)
  on lines 2861..2862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2861-2862)
  on line 2865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2865-2865)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2631..2633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2631-2633)
  on lines 2635..2636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2635-2636)
  on line 2639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2639-2639)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 281..282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:281-282)
  on lines 285..286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:285-286)
  on line 293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:293-293)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2493-2493)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2820..2822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2820-2822)
  on lines 2824..2825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2824-2825)
  on line 2828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2828-2828)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2894..2896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2894-2896)
  on lines 2898..2899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2898-2899)
  on line 2902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2902-2902)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:250-250)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1848..1849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1848-1849)
  on lines 1856..1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1856-1858)
  on lines 1860..1861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1860-1861)
  on lines 1863..1864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1863-1864)
  on lines 1871..1873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1871-1873)
  on lines 1875..1876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1875-1876)
  on lines 1878..1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1878-1879)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1711..1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1711-1712)
  on lines 1714..1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1714-1715)
  on lines 1722..1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1722-1724)
  on lines 1726..1727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1726-1727)
  on lines 1729..1730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1729-1730)
  on lines 1737..1739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1737-1739)
  on lines 1741..1742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1741-1742)
  on lines 1744..1745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1744-1745)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1518..1519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1518-1519)
  on lines 1521..1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1521-1522)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2291..2292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2291-2292)
  on lines 2302..2303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2302-2303)
  on lines 2313..2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2313-2314)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2130..2131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2130-2131)
  on lines 2141..2142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2141-2142)
  on lines 2152..2153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2152-2153)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 2612..2613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2612-2613)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on lines 2912..2913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2912-2913)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on lines 2838..2839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2838-2839)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on lines 2875..2876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2875-2876)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 2649..2650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2649-2650)
[Warning][Deadcode] Function 'sign' has dead code:
  on line 323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:323-323)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:747-747)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:354-354)
  on line 357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:357-357)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 448
  dead: 700 (466 in uncalled functions)
  total lines: 1148
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2816:7-2816:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2299:11-2299:21)
[Warning][Deadcode][CWE-570] condition '! publicKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:280:7-280:18)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:284:9-284:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2309:11-2309:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2310:13-2310:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2835:7-2835:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2590:7-2590:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1491:7-1491:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2853:7-2853:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2127:9-2127:19)
[Warning][Deadcode][CWE-570] condition '! privkey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:322:7-322:16)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2609:7-2609:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2138:11-2138:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:347:7-347:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2872:7-2872:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2627:7-2627:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1707:7-1707:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1708:9-1708:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1515:7-1515:18)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:351:9-351:16)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2148:11-2148:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2149:13-2149:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2890:7-2890:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2382:7-2382:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2179:7-2179:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2646:7-2646:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2180:9-2180:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1947:7-1947:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2909:7-2909:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1772:7-1772:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2412:11-2412:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1977:11-1977:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1777:11-1777:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:790:10-790:11)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:490:7-490:14)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2002:11-2002:22)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2233:7-2233:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2024:11-2024:22)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring1_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2252:13-2252:50)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:546:7-546:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2072:7-2072:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2073:9-2073:19)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring2_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2266:15-2266:52)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1841:7-1841:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:1845:11-1845:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product17.cil.c:2288:9-2288:19)
[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
