./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_spec6_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_spec6_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_spec6_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_spec6_product26.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:268:5-288: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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:558:1-568:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:647:1-658:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:659:1-670:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:776:1-790:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:794:1-819:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:820:1-839:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:844:1-867:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:868:1-887:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:935:1-959:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:969:1-1037:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1038:1-1106:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1828:1-1837:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1884:1-1898:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1920:1-1935:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2012:1-2032:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2033:1-2048:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2051:1-2071:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2072:1-2087:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2164:1-2182:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2183:1-2198:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2201:1-2219:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2220:1-2235:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2238:1-2256:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2257:1-2272:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2554:1-2568:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2650:1-2658:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2882:1-2896:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2327-2327)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1460-1460)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2671-2671)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1684-1684)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1185..1187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1185-1187)
  on lines 1189..1190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1189-1190)
  on lines 1195..1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1195-1198)
  on lines 1200..1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1200-1202)
  on lines 1204..1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1204-1206)
  on lines 1208..1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1208-1209)
  on lines 1214..1217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1214-1217)
  on lines 1219..1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1219-1221)
  on lines 1223..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1223-1225)
  on lines 1227..1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1227-1228)
  on lines 1233..1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1233-1234)
  on line 1238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1238-1238)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:912-912)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1321-1321)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1756-1756)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1803-1803)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1588..1590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1588-1590)
  on lines 1592..1593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1592-1593)
  on lines 1597..1600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1597-1600)
  on lines 1602..1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1602-1604)
  on lines 1606..1607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1606-1607)
  on lines 1611..1614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1611-1614)
  on lines 1616..1618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1616-1618)
  on lines 1620..1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1620-1621)
  on lines 1625..1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1625-1626)
  on line 1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1630-1630)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1410..1411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1410-1411)
  on line 1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1415-1415)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1481..1483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1481-1483)
  on lines 1485..1486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1485-1486)
  on lines 1490..1493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1490-1493)
  on lines 1495..1497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1495-1497)
  on lines 1499..1500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1499-1500)
  on lines 1504..1507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1504-1507)
  on lines 1509..1511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1509-1511)
  on lines 1513..1514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1513-1514)
  on lines 1518..1519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1518-1519)
  on line 1523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1523-1523)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1368-1368)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2136..2137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2136-2137)
  on line 2143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2143-2143)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1947..1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1947-1948)
  on line 1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1954-1954)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1910..1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1910-1911)
  on line 1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1917-1917)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1984..1985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1984-1985)
  on line 1991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1991-1991)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2935-2935)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2944-2944)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2099..2100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2099-2100)
  on line 2106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2106-2106)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 2969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2969-2969)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2647-2647)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2627-2627)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2926-2926)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1252..1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1252-1253)
  on lines 1260..1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1260-1262)
  on lines 1264..1265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1264-1265)
  on lines 1267..1268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1267-1268)
  on lines 1275..1277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1275-1277)
  on lines 1279..1280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1279-1280)
  on lines 1282..1283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1282-1283)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1115..1116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1115-1116)
  on lines 1118..1119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1118-1119)
  on lines 1126..1128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1126-1128)
  on lines 1130..1131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1130-1131)
  on lines 1133..1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1133-1134)
  on lines 1141..1143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1141-1143)
  on lines 1145..1146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1145-1146)
  on lines 1148..1149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1148-1149)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 922..923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:922-923)
  on lines 925..926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:925-926)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1329-1329)
  on lines 1334..1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1334-1335)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1764-1764)
  on lines 1769..1770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1769-1770)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1695..1696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1695-1696)
  on lines 1706..1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1706-1707)
  on lines 1717..1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1717-1718)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1534..1535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1534-1535)
  on lines 1545..1546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1545-1546)
  on lines 1556..1557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1556-1557)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2154-2154)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1965-1965)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2117-2117)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2002-2002)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1858-1858)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 618
  dead: 575 (397 in uncalled functions)
  total lines: 1193
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1713:11-1713:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1714:13-1714:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2001:9-2001:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:602:7-602:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1531:9-1531:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1542:11-1542:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1111:7-1111:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1763:7-1763:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1112:9-1112:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:919:7-919:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1328:7-1328:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1552:11-1552:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1766:9-1766:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1553:13-1553:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1331:9-1331:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1583:7-1583:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1584:9-1584:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2098:9-2098:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1176:7-1176:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2370:10-2370:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1816:11-1816:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1381:11-1381:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1181:11-1181:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2116:9-2116:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1406:11-1406:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2135:9-2135:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1428:11-1428:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:2153:9-2153:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1909:9-1909:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1476:7-1476:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1477:9-1477:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1946:9-1946:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1245:7-1245:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1249:11-1249:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1964:9-1964:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1692:9-1692:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1703:11-1703:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product26.cil.c:1983:9-1983: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
