./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_spec7_product30.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_spec7_product30.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_spec7_product30.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_spec7_product30.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.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_spec7_product30.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_spec7_product30.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_spec7_product30.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_spec7_product30.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_spec7_product30.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_spec7_product30.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:662:1-676:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:679:1-697:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:698:1-713:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:790:1-810:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:811:1-826:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:829:1-849:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:850:1-865:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1016:1-1034:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1085:1-1099:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1130:1-1144:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1148:1-1173:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1174:1-1193:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1198:1-1221:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1222:1-1241:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1245:1-1268:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1269:1-1288:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1289:1-1313:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1323:1-1391:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1392:1-1460:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1461:1-1516:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1526:1-1594:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1595:1-1650:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2089:1-2112:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2113:1-2132:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2194:1-2203:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2400:1-2414:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2590:1-2617:1)
[Warning][Deadcode] Function 'printMail__wrappee__AutoResponder' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2618:1-2636:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2637:1-2655:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2656:1-2669:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2699:1-2707:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2821:1-2831:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2910:1-2921:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2922:1-2933:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2186-2186)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1814-1814)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2720-2720)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2020..2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2020-2022)
  on lines 2024..2026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2024-2026)
  on lines 2028..2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2028-2029)
  on line 2038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2038-2038)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 1667..1668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1667-1668)
  on line 1675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1675-1675)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2149..2150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2149-2150)
  on line 2157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2157-2157)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1942..1944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1942-1944)
  on lines 1946..1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1946-1947)
  on lines 1951..1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1951-1954)
  on lines 1956..1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1956-1958)
  on lines 1960..1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1960-1961)
  on lines 1965..1968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1965-1968)
  on lines 1970..1972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1970-1972)
  on lines 1974..1975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1974-1975)
  on lines 1979..1980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1979-1980)
  on line 1984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1984-1984)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1764..1765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1764-1765)
  on line 1769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1769-1769)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1835..1837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1835-1837)
  on lines 1839..1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1839-1840)
  on lines 1844..1847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1844-1847)
  on lines 1849..1851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1849-1851)
  on lines 1853..1854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1853-1854)
  on lines 1858..1861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1858-1861)
  on lines 1863..1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1863-1865)
  on lines 1867..1868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1867-1868)
  on lines 1872..1873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1872-1873)
  on line 1877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1877-1877)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1714..1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1714-1715)
  on line 1722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1722-1722)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 914..915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:914-915)
  on line 921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:921-921)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 725..726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:725-726)
  on line 732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:732-732)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 988..989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:988-989)
  on line 995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:995-995)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 762..763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:762-763)
  on line 769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:769-769)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2453-2453)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2462-2462)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 877..878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:877-878)
  on line 884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:884-884)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2479..2480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2479-2480)
  on line 2487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2487-2487)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2696-2696)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2676-2676)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 951..952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:951-952)
  on line 958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:958-958)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2444-2444)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1683-1683)
  on lines 1688..1689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1688-1689)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2049..2050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2049-2050)
  on lines 2060..2061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2060-2061)
  on lines 2071..2072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2071-2072)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1888..1889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1888-1889)
  on lines 1899..1900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1899-1900)
  on lines 1910..1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1910-1911)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:932-932)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:743-743)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:895-895)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1043-1043)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:969-969)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1006-1006)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:780-780)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2224-2224)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 521
  dead: 653 (528 in uncalled functions)
  total lines: 1174
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:779:9-779:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2170:11-2170:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1735:11-1735:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1042:9-1042:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1760:11-1760:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2865:7-2865:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1782:11-1782:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2019:11-2019:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:876:9-876:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1830:7-1830:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1831:9-1831:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:894:9-894:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2046:9-2046:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:913:9-913:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2057:11-2057:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2067:11-2067:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:931:9-931:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2068:13-2068:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:950:9-950:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1885:9-1885:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1666:11-1666:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:463:10-463:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1896:11-1896:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:968:9-968:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:724:9-724:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1682:7-1682:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1906:11-1906:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1907:13-1907:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1685:9-1685:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:987:9-987:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:742:9-742:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1937:7-1937:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1938:9-1938:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1005:9-1005:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:761:9-761:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2148:11-2148:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:2478:9-2478:21)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product30.cil.c:1713:11-1713:22)
[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
