./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_productSimulator.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_productSimulator.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_productSimulator.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_productSimulator.cil.c:541:3-562:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:598:3-623:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:683:5-703: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 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:448:1-462:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:470:1-515:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:516:1-571:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:572:1-631:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:634:1-736:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:737:1-782:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:783:1-828:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:859:1-873:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:877:1-902:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:903:1-922:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:927:1-950:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:951:1-970:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1018:1-1042:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1052:1-1120:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1121:1-1189:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1932:1-1946:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1968:1-1983:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2060:1-2080:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2081:1-2096:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2099:1-2119:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2120:1-2135:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2548:1-2556:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2929:1-2943:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:3281:1-3291:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:3370:1-3381:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:3382:1-3393:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:3487-3487)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1543-1543)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2569-2569)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1767-1767)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1268..1270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1268-1270)
  on lines 1272..1273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1272-1273)
  on lines 1278..1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1278-1281)
  on lines 1283..1285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1283-1285)
  on lines 1287..1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1287-1289)
  on lines 1291..1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1291-1292)
  on lines 1297..1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1297-1300)
  on lines 1302..1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1302-1304)
  on lines 1306..1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1306-1308)
  on lines 1310..1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1310-1311)
  on lines 1316..1317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1316-1317)
  on line 1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1321-1321)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:995-995)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1404-1404)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1839-1839)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1886-1886)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1671..1673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1671-1673)
  on lines 1675..1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1675-1676)
  on lines 1680..1683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1680-1683)
  on lines 1685..1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1685-1687)
  on lines 1689..1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1689-1690)
  on lines 1694..1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1694-1697)
  on lines 1699..1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1699-1701)
  on lines 1703..1704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1703-1704)
  on lines 1708..1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1708-1709)
  on line 1713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1713-1713)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1493..1494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1493-1494)
  on line 1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1498-1498)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1564..1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1564-1566)
  on lines 1568..1569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1568-1569)
  on lines 1573..1576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1573-1576)
  on lines 1578..1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1578-1580)
  on lines 1582..1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1582-1583)
  on lines 1587..1590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1587-1590)
  on lines 1592..1594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1592-1594)
  on lines 1596..1597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1596-1597)
  on lines 1601..1602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1601-1602)
  on line 1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1606-1606)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1451-1451)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2184..2185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2184-2185)
  on line 2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2191-2191)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1995..1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1995-1996)
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2002-2002)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1958..1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1958-1959)
  on line 1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1965-1965)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2258..2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2258-2259)
  on line 2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2265-2265)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2032..2033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2032-2033)
  on line 2039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2039-2039)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2982-2982)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2991-2991)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2147..2148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2147-2148)
  on line 2154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2154-2154)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 3008..3009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:3008-3009)
  on line 3016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:3016-3016)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2541-2541)
  on line 2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2543-2543)
  on line 2545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2545-2545)
[Warning][Deadcode] Function 'isReadable__before__Encrypt' has dead code:
  on line 2507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2507-2507)
[Warning][Deadcode] Function 'isReadable__role__Encrypt' has dead code:
  on line 2527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2527-2527)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2221..2222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2221-2222)
  on line 2228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2228-2228)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2295..2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2295-2296)
  on line 2302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2302-2302)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2973-2973)
[Warning][Deadcode] Function 'outgoing__before__AddressBook' has dead code:
  on line 2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2658-2658)
  on line 2660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2660-2660)
[Warning][Deadcode] Function 'printMail__before__Sign' has dead code:
  on line 2428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2428-2428)
  on line 2430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2430-2430)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 70 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:70-70)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1335..1336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1335-1336)
  on lines 1343..1345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1343-1345)
  on lines 1347..1348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1347-1348)
  on lines 1350..1351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1350-1351)
  on lines 1358..1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1358-1360)
  on lines 1362..1363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1362-1363)
  on lines 1365..1366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1365-1366)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1198..1199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1198-1199)
  on lines 1201..1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1201-1202)
  on lines 1209..1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1209-1211)
  on lines 1213..1214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1213-1214)
  on lines 1216..1217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1216-1217)
  on lines 1224..1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1224-1226)
  on lines 1228..1229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1228-1229)
  on lines 1231..1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1231-1232)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1005..1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1005-1006)
  on lines 1008..1009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1008-1009)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1412-1412)
  on lines 1417..1418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1417-1418)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1847-1847)
  on lines 1852..1853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1852-1853)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1778..1779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1778-1779)
  on lines 1789..1790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1789-1790)
  on lines 1800..1801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1800-1801)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1617..1618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1617-1618)
  on lines 1628..1629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1628-1629)
  on lines 1639..1640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1639-1640)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2202-2202)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2013-2013)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2165-2165)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2313-2313)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2239-2239)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2276-2276)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2050-2050)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:140-140)
  on line 156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:156-156)
  on line 165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:165-165)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 818
  dead: 553 (351 in uncalled functions)
  total lines: 1371
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2146:9-2146:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2164:9-2164:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1259:7-1259:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1264:11-1264:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2183:9-2183:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2201:9-2201:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2220:9-2220:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2238:9-2238:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2257:9-2257:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1328:7-1328:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2275:9-2275:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1332:11-1332:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1775:9-1775:19)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Encrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:104:7-104:35)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2294:9-2294:20)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Decrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:109:11-109:39)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:112:13-112:39)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1786:11-1786:21)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Encrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:114:15-114:43)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1796:11-1796:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2312:9-2312:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1797:13-1797:23)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Keys' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:132:29-132:52)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1846:7-1846:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1002:7-1002:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1411:7-1411:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1849:9-1849:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1414:9-1414:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:3007:9-3007:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:219:10-219:11)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2421:7-2421:33)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1899:11-1899:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1464:11-1464:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1489:11-1489:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1957:9-1957:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1511:11-1511:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1994:9-1994:20)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2534:7-2534:33)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1559:7-1559:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1560:9-1560:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2012:9-2012:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2031:9-2031:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2049:9-2049:20)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:2651:7-2651:33)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1614:9-1614:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1625:11-1625:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1194:7-1194:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1195:9-1195:19)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1635:11-1635:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1636:13-1636:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1666:7-1666:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_productSimulator.cil.c:1667:9-1667:19)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
