./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_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_spec1_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_spec1_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_spec1_product26.cil.c:2707:3-2728:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2764:3-2789:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2849:5-2869: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 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:192:1-202:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:281:1-292:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:293:1-304:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:480:1-488:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:721:1-735:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:857:1-866:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1131:1-1145:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1149:1-1174:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1175:1-1194:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1199:1-1222:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1223:1-1242:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1290:1-1314:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1324:1-1392:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1393:1-1461:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2183:1-2197:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2240:1-2254:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2276:1-2291:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2368:1-2388:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2389:1-2404:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2407:1-2427:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2428:1-2443:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2520:1-2538:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2539:1-2554:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2557:1-2575:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2576:1-2591:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2594:1-2612:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2613:1-2628:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2636:1-2681:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2682:1-2737:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2738:1-2797:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2800:1-2902:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2903:1-2948:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2949:1-2994:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1118-1118)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1815-1815)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:501-501)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2039-2039)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1540..1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1540-1542)
  on lines 1544..1545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1544-1545)
  on lines 1550..1553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1550-1553)
  on lines 1555..1557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1555-1557)
  on lines 1559..1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1559-1561)
  on lines 1563..1564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1563-1564)
  on lines 1569..1572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1569-1572)
  on lines 1574..1576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1574-1576)
  on lines 1578..1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1578-1580)
  on lines 1582..1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1582-1583)
  on lines 1588..1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1588-1589)
  on line 1593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1593-1593)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1267-1267)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1676-1676)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2111-2111)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2158-2158)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1943..1945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1943-1945)
  on lines 1947..1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1947-1948)
  on lines 1952..1955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1952-1955)
  on lines 1957..1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1957-1959)
  on lines 1961..1962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1961-1962)
  on lines 1966..1969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1966-1969)
  on lines 1971..1973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1971-1973)
  on lines 1975..1976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1975-1976)
  on lines 1980..1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1980-1981)
  on line 1985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1985-1985)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1765..1766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1765-1766)
  on line 1770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1770-1770)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1836..1838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1836-1838)
  on lines 1840..1841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1840-1841)
  on lines 1845..1848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1845-1848)
  on lines 1850..1852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1850-1852)
  on lines 1854..1855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1854-1855)
  on lines 1859..1862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1859-1862)
  on lines 1864..1866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1864-1866)
  on lines 1868..1869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1868-1869)
  on lines 1873..1874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1873-1874)
  on line 1878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1878-1878)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1723-1723)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2492..2493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2492-2493)
  on line 2499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2499-2499)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2303..2304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2303-2304)
  on line 2310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2310-2310)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2266..2267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2266-2267)
  on line 2273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2273-2273)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2340..2341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2340-2341)
  on line 2347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2347-2347)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:774-774)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:783-783)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2455..2456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2455-2456)
  on line 2462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2462-2462)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 800..801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:800-801)
  on line 808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:808-808)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:477-477)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:457-457)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:765-765)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1607..1608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1607-1608)
  on lines 1615..1617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1615-1617)
  on lines 1619..1620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1619-1620)
  on lines 1622..1623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1622-1623)
  on lines 1630..1632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1630-1632)
  on lines 1634..1635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1634-1635)
  on lines 1637..1638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1637-1638)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1470..1471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1470-1471)
  on lines 1473..1474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1473-1474)
  on lines 1481..1483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1481-1483)
  on lines 1485..1486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1485-1486)
  on lines 1488..1489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1488-1489)
  on lines 1496..1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1496-1498)
  on lines 1500..1501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1500-1501)
  on lines 1503..1504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1503-1504)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1277..1278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1277-1278)
  on lines 1280..1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1280-1281)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1684-1684)
  on lines 1689..1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1689-1690)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2119-2119)
  on lines 2124..2125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2124-2125)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2050..2051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2050-2051)
  on lines 2061..2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2061-2062)
  on lines 2072..2073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2072-2073)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1889..1890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1889-1890)
  on lines 1900..1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1900-1901)
  on lines 1911..1912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1911-1912)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2510-2510)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2321-2321)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2473-2473)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2358-2358)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:887-887)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 605
  dead: 577 (397 in uncalled functions)
  total lines: 1182
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:930:10-930:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1831:7-1831:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1832:9-1832:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1600:7-1600:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2302:9-2302:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1604:11-1604:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2047:9-2047:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2320:9-2320:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2058:11-2058:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2339:9-2339:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2068:11-2068:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2069:13-2069:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2357:9-2357:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1886:9-1886:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1897:11-1897:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1466:7-1466:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1274:7-1274:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2118:7-2118:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1467:9-1467:19)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1683:7-1683:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1907:11-1907:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2121:9-2121:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1908:13-1908:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1686:9-1686:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1938:7-1938:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1939:9-1939:19)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:799:9-799:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1531:7-1531:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2171:11-2171:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1736:11-1736:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2454:9-2454:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1536:11-1536:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1761:11-1761:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2472:9-2472:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:236:7-236:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2491:9-2491:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:1783:11-1783:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2509:9-2509:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product26.cil.c:2265:9-2265: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
