./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_spec11_product26.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec11_product26.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1042:3-1063:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1099:3-1124:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1184:5-1204: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 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:71:1-85:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:107:1-122:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:199:1-219:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:220:1-235:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:238:1-258:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:259:1-274:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:351:1-369:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:370:1-385:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:388:1-406:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:407:1-422:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:425:1-443:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:444:1-459:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:553:1-561:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:582:1-591:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:764:1-774:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:853:1-864:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:865:1-876:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:971:1-1016:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1017:1-1072:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1073:1-1132:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1135:1-1237:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1238:1-1283:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1284:1-1329:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1570:1-1584:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1588:1-1613:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1614:1-1633:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1638:1-1661:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1662:1-1681:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1729:1-1753:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1763:1-1831:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1832:1-1900:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2821:1-2835:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2971:1-2985:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2966-2966)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2254-2254)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:574-574)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2478-2478)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1979..1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1979-1981)
  on lines 1983..1984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1983-1984)
  on lines 1989..1992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1989-1992)
  on lines 1994..1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1994-1996)
  on lines 1998..2000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1998-2000)
  on lines 2002..2003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2002-2003)
  on lines 2008..2011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2008-2011)
  on lines 2013..2015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2013-2015)
  on lines 2017..2019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2017-2019)
  on lines 2021..2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2021-2022)
  on lines 2027..2028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2027-2028)
  on line 2032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2032-2032)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1706-1706)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2115-2115)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2550-2550)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2597-2597)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2382..2384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2382-2384)
  on lines 2386..2387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2386-2387)
  on lines 2391..2394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2391-2394)
  on lines 2396..2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2396-2398)
  on lines 2400..2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2400-2401)
  on lines 2405..2408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2405-2408)
  on lines 2410..2412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2410-2412)
  on lines 2414..2415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2414-2415)
  on lines 2419..2420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2419-2420)
  on line 2424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2424-2424)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2204..2205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2204-2205)
  on line 2209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2209-2209)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2275..2277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2275-2277)
  on lines 2279..2280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2279-2280)
  on lines 2284..2287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2284-2287)
  on lines 2289..2291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2289-2291)
  on lines 2293..2294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2293-2294)
  on lines 2298..2301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2298-2301)
  on lines 2303..2305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2303-2305)
  on lines 2307..2308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2307-2308)
  on lines 2312..2313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2312-2313)
  on line 2317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2317-2317)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2162-2162)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 323..324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:323-324)
  on line 330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:330-330)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 134..135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:134-135)
  on line 141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:141-141)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 97..98 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:97-98)
  on line 104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:104-104)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 171..172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:171-172)
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:178-178)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2874-2874)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2883-2883)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 286..287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:286-287)
  on line 293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:293-293)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2900..2901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2900-2901)
  on line 2908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2908-2908)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:550-550)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:530-530)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2865-2865)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2046..2047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2046-2047)
  on lines 2054..2056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2054-2056)
  on lines 2058..2059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2058-2059)
  on lines 2061..2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2061-2062)
  on lines 2069..2071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2069-2071)
  on lines 2073..2074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2073-2074)
  on lines 2076..2077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2076-2077)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1909..1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1909-1910)
  on lines 1912..1913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1912-1913)
  on lines 1920..1922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1920-1922)
  on lines 1924..1925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1924-1925)
  on lines 1927..1928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1927-1928)
  on lines 1935..1937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1935-1937)
  on lines 1939..1940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1939-1940)
  on lines 1942..1943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1942-1943)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1716..1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1716-1717)
  on lines 1719..1720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1719-1720)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2123-2123)
  on lines 2128..2129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2128-2129)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2558-2558)
  on lines 2563..2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2563-2564)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2489..2490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2489-2490)
  on lines 2500..2501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2500-2501)
  on lines 2511..2512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2511-2512)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2328..2329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2328-2329)
  on lines 2339..2340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2339-2340)
  on lines 2350..2351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2350-2351)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:341-341)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:152-152)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:304-304)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:189-189)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:612-612)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 603
  dead: 577 (397 in uncalled functions)
  total lines: 1180
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2507:11-2507:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2508:13-2508:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2325:9-2325:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2336:11-2336:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1905:7-1905:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2557:7-2557:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1906:9-1906:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.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_spec11_product26.cil.c:2122:7-2122:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2346:11-2346:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2560:9-2560:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2347:13-2347:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2125:9-2125:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2377:7-2377:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2378:9-2378:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:285:9-285:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2899:9-2899:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:303:9-303:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1970:7-1970:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2610:11-2610:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:322:9-322:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2175:11-2175:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1975:11-1975:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:340:9-340:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:96:9-96:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2200:11-2200:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2222:11-2222:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:133:9-133:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:151:9-151:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2270:7-2270:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2271:9-2271:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:1370:10-1370:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2039:7-2039:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:170:9-170:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2043:11-2043:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2486:9-2486:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:188:9-188:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:808:7-808:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product26.cil.c:2497:11-2497:21)
[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
