./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_spec1_product29.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_spec1_product29.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_spec1_product29.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_spec1_product29.cil.c:538:3-559:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:595:3-620:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:680:5-700: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_spec1_product29.cil.c:71:1-85:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:88:1-106:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:107:1-122:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:199:1-219:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:220:1-235:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:238:1-258:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:259:1-274:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:425:1-443:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:467:1-512:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:513:1-568:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:569:1-628:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:631:1-733:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:734:1-779:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:780:1-825:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1068:1-1095:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1096:1-1114:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1115:1-1133:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1134:1-1147:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1177:1-1185:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1319:1-1329:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1408:1-1419:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1420:1-1431:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1528:1-1542:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1546:1-1571:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1572:1-1591:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1596:1-1619:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1620:1-1639:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1687:1-1711:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1721:1-1789:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1790:1-1858:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2052:1-2075:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2076:1-2095:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2487:1-2510:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2511:1-2530:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2580:1-2589:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2643:1-2657:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2847:1-2861:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2875:1-2884:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2894:1-2902:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2903:1-2911:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1505-1505)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 1311..1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1311-1313)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2212-2212)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1198-1198)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2409..2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2409-2410)
  on lines 2423..2424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2423-2424)
  on line 2436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2436-2436)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1937..1939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1937-1939)
  on lines 1941..1942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1941-1942)
  on lines 1947..1950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1947-1950)
  on lines 1952..1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1952-1954)
  on lines 1956..1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1956-1958)
  on lines 1960..1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1960-1961)
  on lines 1966..1969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1966-1969)
  on lines 1971..1973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1971-1973)
  on lines 1975..1977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1975-1977)
  on lines 1979..1980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1979-1980)
  on lines 1985..1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1985-1986)
  on line 1990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1990-1990)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 1651..1653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1651-1653)
  on lines 1655..1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1655-1657)
  on lines 1659..1660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1659-1660)
  on line 1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1664-1664)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2542..2544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2542-2544)
  on lines 2546..2548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2546-2548)
  on lines 2550..2551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2550-2551)
  on line 2555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2555-2555)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2340..2342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2340-2342)
  on lines 2344..2345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2344-2345)
  on lines 2349..2352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2349-2352)
  on lines 2354..2356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2354-2356)
  on lines 2358..2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2358-2359)
  on lines 2363..2366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2363-2366)
  on lines 2368..2370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2368-2370)
  on lines 2372..2373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2372-2373)
  on lines 2377..2378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2377-2378)
  on line 2382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2382-2382)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2162..2163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2162-2163)
  on line 2167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2167-2167)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2233..2235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2233-2235)
  on lines 2237..2238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2237-2238)
  on lines 2242..2245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2242-2245)
  on lines 2247..2249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2247-2249)
  on lines 2251..2252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2251-2252)
  on lines 2256..2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2256-2259)
  on lines 2261..2263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2261-2263)
  on lines 2265..2266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2265-2266)
  on lines 2270..2271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2270-2271)
  on line 2275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2275-2275)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2120-2120)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 322..324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:322-324)
  on lines 326..327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:326-327)
  on line 330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:330-330)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 133..135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:133-135)
  on lines 137..138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:137-138)
  on line 141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:141-141)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 396..398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:396-398)
  on lines 400..401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:400-401)
  on line 404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:404-404)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 170..172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:170-172)
  on lines 174..175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:174-175)
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:178-178)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 285..287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:285-287)
  on lines 289..290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:289-290)
  on line 293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:293-293)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2926..2927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2926-2927)
  on line 2934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2934-2934)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1174-1174)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1154-1154)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 359..361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:359-361)
  on lines 363..364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:363-364)
  on line 367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:367-367)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2891-2891)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2004..2005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2004-2005)
  on lines 2012..2014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2012-2014)
  on lines 2016..2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2016-2017)
  on lines 2019..2020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2019-2020)
  on lines 2027..2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2027-2029)
  on lines 2031..2032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2031-2032)
  on lines 2034..2035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2034-2035)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1867..1868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1867-1868)
  on lines 1870..1871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1870-1871)
  on lines 1878..1880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1878-1880)
  on lines 1882..1883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1882-1883)
  on lines 1885..1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1885-1886)
  on lines 1893..1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1893-1895)
  on lines 1897..1898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1897-1898)
  on lines 1900..1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1900-1901)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1674..1675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1674-1675)
  on lines 1677..1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1677-1678)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2447..2448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2447-2448)
  on lines 2458..2459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2458-2459)
  on lines 2469..2470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2469-2470)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2286..2287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2286-2287)
  on lines 2297..2298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2297-2298)
  on lines 2308..2309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2308-2309)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on lines 340..341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:340-341)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 151..152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:151-152)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on lines 303..304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:303-304)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on lines 451..452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:451-452)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on lines 377..378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:377-378)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on lines 414..415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:414-415)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 188..189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:188-189)
[Warning][Deadcode] Function 'sign' has dead code:
  on line 2964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2964-2964)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2610-2610)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 2995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2995-2995)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 507
  dead: 681 (455 in uncalled functions)
  total lines: 1188
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1647:7-1647:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2283:9-2283:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1363:7-1363:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2294:11-2294:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1863:7-1863:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1864:9-1864:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1671:7-1671:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2304:11-2304:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2305:13-2305:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2538:7-2538:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2335:7-2335:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2336:9-2336:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:281:7-281:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:300:7-300:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1928:7-1928:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:875:10-875:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2568:11-2568:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2133:11-2133:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1933:11-1933:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:318:7-318:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2158:11-2158:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:337:7-337:18)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2925:9-2925:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:355:7-355:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2180:11-2180:22)
[Warning][Deadcode][CWE-570] condition '! privkey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2963:7-2963:16)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:374:7-374:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:129:7-129:18)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring1_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2408:13-2408:50)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:392:7-392:18)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2992:9-2992:16)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2228:7-2228:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2229:9-2229:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:148:7-148:18)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring2_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2422:15-2422:52)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1997:7-1997:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:411:7-411:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:166:7-166:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2001:11-2001:21)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:1307:7-1307:14)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2444:9-2444:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:185:7-185:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2455:11-2455:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2465:11-2465:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:448:7-448:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product29.cil.c:2466:13-2466:23)
[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
