./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_spec3_product25.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_spec3_product25.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_spec3_product25.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_spec3_product25.cil.c:538:3-559:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:595:3-620:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:680:5-700:5 with factor 2
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:71:1-85:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:107:1-122:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:199:1-219:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:220:1-235:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:238:1-258:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:259:1-274:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:277:1-295:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:296:1-311:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:314:1-332:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:333:1-348:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:467:1-512:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:513:1-568:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:569:1-628:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:631:1-733:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:734:1-779:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:780:1-825:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:829:1-843:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1103:1-1117:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1121:1-1146:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1147:1-1166:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1171:1-1194:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1195:1-1214:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1262:1-1286:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1296:1-1364:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1365:1-1433:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1627:1-1650:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1651:1-1670:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2169:1-2178:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2354:1-2368:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2679:1-2687:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2801:1-2811:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2890:1-2901:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2902:1-2913:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2997-2997)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1787-1787)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2700-2700)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1965..1967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1965-1967)
  on lines 1969..1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1969-1971)
  on lines 1973..1974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1973-1974)
  on line 2011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2011-2011)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1512..1514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1512-1514)
  on lines 1516..1517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1516-1517)
  on lines 1522..1525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1522-1525)
  on lines 1527..1529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1527-1529)
  on lines 1531..1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1531-1533)
  on lines 1535..1536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1535-1536)
  on lines 1541..1544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1541-1544)
  on lines 1546..1548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1546-1548)
  on lines 1550..1552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1550-1552)
  on lines 1554..1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1554-1555)
  on lines 1560..1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1560-1561)
  on line 1565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1565-1565)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 1231..1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1231-1232)
  on line 1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1239-1239)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2067..2068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2067-2068)
  on line 2083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2083-2083)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2122..2123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2122-2123)
  on line 2130 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2130-2130)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1915..1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1915-1917)
  on lines 1919..1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1919-1920)
  on lines 1924..1927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1924-1927)
  on lines 1929..1931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1929-1931)
  on lines 1933..1934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1933-1934)
  on lines 1938..1941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1938-1941)
  on lines 1943..1945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1943-1945)
  on lines 1947..1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1947-1948)
  on lines 1952..1953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1952-1953)
  on line 1957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1957-1957)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1737..1738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1737-1738)
  on line 1742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1742-1742)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1808..1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1808-1810)
  on lines 1812..1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1812-1813)
  on lines 1817..1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1817-1820)
  on lines 1822..1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1822-1824)
  on lines 1826..1827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1826-1827)
  on lines 1831..1834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1831-1834)
  on lines 1836..1838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1836-1838)
  on lines 1840..1841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1840-1841)
  on lines 1845..1846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1845-1846)
  on line 1850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1850-1850)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1687..1688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1687-1688)
  on line 1695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1695-1695)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 134..135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:134-135)
  on line 141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:141-141)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 97..98 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:97-98)
  on line 104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:104-104)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 397..398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:397-398)
  on line 404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:404-404)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 171..172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:171-172)
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:178-178)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2407-2407)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2416-2416)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2433..2434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2433-2434)
  on line 2441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2441-2441)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2676-2676)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 360..361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:360-361)
  on line 367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:367-367)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 434..435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:434-435)
  on line 441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:441-441)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2398-2398)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1579..1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1579-1580)
  on lines 1587..1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1587-1589)
  on lines 1591..1592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1591-1592)
  on lines 1594..1595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1594-1595)
  on lines 1602..1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1602-1604)
  on lines 1606..1607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1606-1607)
  on lines 1609..1610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1609-1610)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1442..1443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1442-1443)
  on lines 1445..1446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1445-1446)
  on lines 1453..1455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1453-1455)
  on lines 1457..1458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1457-1458)
  on lines 1460..1461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1460-1461)
  on lines 1468..1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1468-1470)
  on lines 1472..1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1472-1473)
  on lines 1475..1476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1475-1476)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1249..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1249-1250)
  on lines 1252..1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1252-1253)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2091-2091)
  on lines 2096..2097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2096-2097)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2022..2023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2022-2023)
  on lines 2033..2034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2033-2034)
  on lines 2044..2045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2044-2045)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1861..1862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1861-1862)
  on lines 1872..1873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1872-1873)
  on lines 1883..1884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1883-1884)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:152-152)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:452-452)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:378-378)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:415-415)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:189-189)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2199-2199)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 2523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2523-2523)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 589
  dead: 598 (402 in uncalled functions)
  total lines: 1187
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1503:7-1503:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2143:11-2143:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1708:11-1708:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1508:11-1508:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2513:7-2513:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1733:11-1733:22)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1964:7-1964:18)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2845:7-2845:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1755:11-1755:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1803:7-1803:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1804:9-1804:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:894:10-894:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1572:7-1572:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1576:11-1576:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2019:9-2019:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:96:9-96:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2030:11-2030:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:359:9-359:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2040:11-2040:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2041:13-2041:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:377:9-377:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2066:7-2066:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:133:9-133:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1858:9-1858:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:396:9-396:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1230:11-1230:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:151:9-151:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1869:11-1869:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1438:7-1438:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2090:7-2090:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1439:9-1439:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1246:7-1246:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1879:11-1879:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:414:9-414:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2093:9-2093:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1880:13-1880:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:170:9-170:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2432:9-2432:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1910:7-1910:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:433:9-433:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1911:9-1911:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:188:9-188:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:2121:11-2121:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:1686:11-1686:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product25.cil.c:451:9-451: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
