./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_spec8_product35.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_spec8_product35.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_spec8_product35.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_spec8_product35.cil.c:1416:3-1437:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1473:3-1498:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1558:5-1578: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_spec8_product35.cil.c:325:1-339:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:695:1-705:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:784:1-795:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:796:1-807:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:906:1-915:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:949:1-963:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:985:1-1000:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1077:1-1097:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1098:1-1113:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1116:1-1136:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1137:1-1152:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1345:1-1390:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1391:1-1446:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1447:1-1506:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1509:1-1611:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1612:1-1657:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1658:1-1703:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1714:1-1728:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1732:1-1757:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1758:1-1777:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1782:1-1805:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1806:1-1825:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1873:1-1897:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1907:1-1975:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1976:1-2044:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:3097:1-3105:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:3123:1-3137:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:901-901)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2398-2398)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 3118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:3118-3118)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2622-2622)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2123..2125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2123-2125)
  on lines 2127..2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2127-2128)
  on lines 2133..2136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2133-2136)
  on lines 2138..2140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2138-2140)
  on lines 2142..2144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2142-2144)
  on lines 2146..2147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2146-2147)
  on lines 2152..2155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2152-2155)
  on lines 2157..2159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2157-2159)
  on lines 2161..2163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2161-2163)
  on lines 2165..2166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2165-2166)
  on lines 2171..2172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2171-2172)
  on line 2176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2176-2176)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1850-1850)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2259-2259)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2694-2694)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2741-2741)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2526..2528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2526-2528)
  on lines 2530..2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2530-2531)
  on lines 2535..2538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2535-2538)
  on lines 2540..2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2540-2542)
  on lines 2544..2545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2544-2545)
  on lines 2549..2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2549-2552)
  on lines 2554..2556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2554-2556)
  on lines 2558..2559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2558-2559)
  on lines 2563..2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2563-2564)
  on line 2568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2568-2568)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2348..2349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2348-2349)
  on line 2353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2353-2353)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2419..2421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2419-2421)
  on lines 2423..2424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2423-2424)
  on lines 2428..2431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2428-2431)
  on lines 2433..2435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2433-2435)
  on lines 2437..2438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2437-2438)
  on lines 2442..2445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2442-2445)
  on lines 2447..2449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2447-2449)
  on lines 2451..2452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2451-2452)
  on lines 2456..2457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2456-2457)
  on line 2461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2461-2461)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2306-2306)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1201..1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1201-1202)
  on line 1208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1208-1208)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1012..1013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1012-1013)
  on line 1019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1019-1019)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 975..976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:975-976)
  on line 982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:982-982)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1275..1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1275-1276)
  on line 1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1282-1282)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1049..1050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1049-1050)
  on line 1056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1056-1056)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:378-378)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:387-387)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1164..1165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1164-1165)
  on line 1171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1171-1171)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 404..405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:404-405)
  on line 412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:412-412)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 3094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:3094-3094)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 3074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:3074-3074)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1238..1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1238-1239)
  on line 1245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1245-1245)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1312..1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1312-1313)
  on line 1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1319-1319)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:369-369)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2190..2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2190-2191)
  on lines 2198..2200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2198-2200)
  on lines 2202..2203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2202-2203)
  on lines 2205..2206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2205-2206)
  on lines 2213..2215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2213-2215)
  on lines 2217..2218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2217-2218)
  on lines 2220..2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2220-2221)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2053..2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2053-2054)
  on lines 2056..2057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2056-2057)
  on lines 2064..2066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2064-2066)
  on lines 2068..2069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2068-2069)
  on lines 2071..2072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2071-2072)
  on lines 2079..2081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2079-2081)
  on lines 2083..2084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2083-2084)
  on lines 2086..2087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2086-2087)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1860..1861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1860-1861)
  on lines 1863..1864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1863-1864)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2267-2267)
  on lines 2272..2273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2272-2273)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2702-2702)
  on lines 2707..2708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2707-2708)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2633..2634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2633-2634)
  on lines 2644..2645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2644-2645)
  on lines 2655..2656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2655-2656)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2472..2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2472-2473)
  on lines 2483..2484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2483-2484)
  on lines 2494..2495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2494-2495)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1219-1219)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1030-1030)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1182-1182)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1330-1330)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1256-1256)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1293-1293)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1067-1067)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:936-936)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 696
  dead: 547 (355 in uncalled functions)
  total lines: 1243
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1200:9-1200:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2414:7-2414:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2415:9-2415:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2183:7-2183:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2187:11-2187:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1218:9-1218:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:974:9-974:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2630:9-2630:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1237:9-1237:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2641:11-2641:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2651:11-2651:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2652:13-2652:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1255:9-1255:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1011:9-1011:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1274:9-1274:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2469:9-2469:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1029:9-1029:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:739:7-739:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2480:11-2480:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1292:9-1292:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1048:9-1048:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2049:7-2049:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2701:7-2701:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2050:9-2050:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1857:7-1857:18)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:403:9-403:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2266:7-2266:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2490:11-2490:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2704:9-2704:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2491:13-2491:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2269:9-2269:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1311:9-1311:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1066:9-1066:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2521:7-2521:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2522:9-2522:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1329:9-1329:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2114:7-2114:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2754:11-2754:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2319:11-2319:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2119:11-2119:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2344:11-2344:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2804:10-2804:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1163:9-1163:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:2366:11-2366:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product35.cil.c:1181:9-1181:20)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
