./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_product35.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_product35.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_product35.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_product35.cil.c:470:3-491:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:527:3-552:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:612:5-632: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_product35.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_product35.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_product35.cil.c:293:1-304:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:399:1-444:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:445:1-500:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:501:1-560:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:563:1-665:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:666:1-711:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:712:1-757:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1041:1-1055:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1246:1-1260:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1271:1-1285:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1289:1-1314:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1315:1-1334:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1339:1-1362:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1363:1-1382:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1430:1-1454:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1464:1-1532:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1533:1-1601:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2656:1-2664:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2682:1-2691:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2723:1-2737:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2759:1-2774:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2851:1-2871:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2872:1-2887:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2890:1-2910:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2911:1-2926:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3118-3118)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1955-1955)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2677-2677)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2179-2179)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1680..1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1680-1682)
  on lines 1684..1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1684-1685)
  on lines 1690..1693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1690-1693)
  on lines 1695..1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1695-1697)
  on lines 1699..1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1699-1701)
  on lines 1703..1704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1703-1704)
  on lines 1709..1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1709-1712)
  on lines 1714..1716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1714-1716)
  on lines 1718..1720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1718-1720)
  on lines 1722..1723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1722-1723)
  on lines 1728..1729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1728-1729)
  on line 1733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1733-1733)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1407-1407)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1816-1816)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2251-2251)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2298-2298)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2083..2085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2083-2085)
  on lines 2087..2088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2087-2088)
  on lines 2092..2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2092-2095)
  on lines 2097..2099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2097-2099)
  on lines 2101..2102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2101-2102)
  on lines 2106..2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2106-2109)
  on lines 2111..2113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2111-2113)
  on lines 2115..2116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2115-2116)
  on lines 2120..2121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2120-2121)
  on line 2125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2125-2125)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1905..1906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1905-1906)
  on line 1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1910-1910)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1976..1978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1976-1978)
  on lines 1980..1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1980-1981)
  on lines 1985..1988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1985-1988)
  on lines 1990..1992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1990-1992)
  on lines 1994..1995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1994-1995)
  on lines 1999..2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1999-2002)
  on lines 2004..2006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2004-2006)
  on lines 2008..2009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2008-2009)
  on lines 2013..2014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2013-2014)
  on line 2018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2018-2018)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1863-1863)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2975..2976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2975-2976)
  on line 2982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2982-2982)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2786..2787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2786-2787)
  on line 2793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2793-2793)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2749..2750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2749-2750)
  on line 2756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2756-2756)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 3049..3050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3049-3050)
  on line 3056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3056-3056)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2823..2824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2823-2824)
  on line 2830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2830-2830)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1094-1094)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1103-1103)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2938..2939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2938-2939)
  on line 2945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2945-2945)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1120..1121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1120-1121)
  on line 1128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1128-1128)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2653-2653)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2633-2633)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 3012..3013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3012-3013)
  on line 3019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3019-3019)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 3086..3087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3086-3087)
  on line 3093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3093-3093)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1085-1085)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1747..1748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1747-1748)
  on lines 1755..1757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1755-1757)
  on lines 1759..1760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1759-1760)
  on lines 1762..1763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1762-1763)
  on lines 1770..1772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1770-1772)
  on lines 1774..1775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1774-1775)
  on lines 1777..1778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1777-1778)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1610..1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1610-1611)
  on lines 1613..1614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1613-1614)
  on lines 1621..1623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1621-1623)
  on lines 1625..1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1625-1626)
  on lines 1628..1629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1628-1629)
  on lines 1636..1638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1636-1638)
  on lines 1640..1641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1640-1641)
  on lines 1643..1644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1643-1644)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1417..1418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1417-1418)
  on lines 1420..1421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1420-1421)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1824-1824)
  on lines 1829..1830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1829-1830)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2259-2259)
  on lines 2264..2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2264-2265)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2190..2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2190-2191)
  on lines 2201..2202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2201-2202)
  on lines 2212..2213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2212-2213)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2029..2030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2029-2030)
  on lines 2040..2041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2040-2041)
  on lines 2051..2052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2051-2052)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2993-2993)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2804-2804)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2956-2956)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 3104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3104-3104)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 3030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3030-3030)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 3067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3067-3067)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2841-2841)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2712-2712)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 688
  dead: 547 (355 in uncalled functions)
  total lines: 1235
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1676:11-1676:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3103:9-3103:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1901:11-1901:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2361:10-2361:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1923:11-1923:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1971:7-1971:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1972:9-1972:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2937:9-2937:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1740:7-1740:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1744:11-1744:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2187:9-2187:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2955:9-2955:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2198:11-2198:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2974:9-2974:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2208:11-2208:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2209:13-2209:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2992:9-2992:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2748:9-2748:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2026:9-2026:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3011:9-3011:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1119:9-1119:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2037:11-2037:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1606:7-1606:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2258:7-2258:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1607:9-1607:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1414:7-1414:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1823:7-1823:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3029:9-3029:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2047:11-2047:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2785:9-2785:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2261:9-2261:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2048:13-2048:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1826:9-1826:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3048:9-3048:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2078:7-2078:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2079:9-2079:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2803:9-2803:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.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_product35.cil.c:3066:9-3066:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2822:9-2822:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:3085:9-3085:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1671:7-1671:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2311:11-2311:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:2840:9-2840:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product35.cil.c:1876:11-1876: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
