./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_spec6_product28.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_spec6_product28.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_spec6_product28.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_spec6_product28.cil.c:911:3-932:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:968:3-993:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1053:5-1073: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_spec6_product28.cil.c:184:1-194:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:273:1-284:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:285:1-296:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:525:1-539:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:553:1-562:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:572:1-580:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:581:1-589:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:700:1-727:1)
[Warning][Deadcode] Function 'printMail__wrappee__Encrypt' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:728:1-746:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:747:1-765:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:766:1-779:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:809:1-817:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:840:1-885:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:886:1-941:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:942:1-1001:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1004:1-1106:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1107:1-1152:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1153:1-1198:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1248:1-1262:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1478:1-1487:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1519:1-1533:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1536:1-1554:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1555:1-1570:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1647:1-1667:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1668:1-1683:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1686:1-1706:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1707:1-1722:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1873:1-1891:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1927:1-1941:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1945:1-1970:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1971:1-1990:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1995:1-2018:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2019:1-2038:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2042:1-2065:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2066:1-2085:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2086:1-2110:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2120:1-2188:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2189:1-2257:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2258:1-2313:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2323:1-2391:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2392:1-2447:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2451:1-2474:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2475:1-2494:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2886:1-2909:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2910:1-2929:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2983-2983)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 176..178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:176-178)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2611-2611)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:830-830)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2794..2795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2794-2795)
  on lines 2808..2809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2808-2809)
  on lines 2816..2819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2816-2819)
  on lines 2821..2823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2821-2823)
  on lines 2825..2826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2825-2826)
  on lines 2830..2831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2830-2831)
  on line 2835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2835-2835)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2941..2943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2941-2943)
  on lines 2945..2947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2945-2947)
  on lines 2949..2950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2949-2950)
  on line 2954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2954-2954)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2739..2741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2739-2741)
  on lines 2743..2744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2743-2744)
  on lines 2748..2751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2748-2751)
  on lines 2753..2755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2753-2755)
  on lines 2757..2758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2757-2758)
  on lines 2762..2765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2762-2765)
  on lines 2767..2769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2767-2769)
  on lines 2771..2772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2771-2772)
  on lines 2776..2777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2776-2777)
  on line 2781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2781-2781)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2561..2562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2561-2562)
  on line 2566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2566-2566)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2632..2634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2632-2634)
  on lines 2636..2637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2636-2637)
  on lines 2641..2644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2641-2644)
  on lines 2646..2648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2646-2648)
  on lines 2650..2651 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2650-2651)
  on lines 2655..2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2655-2658)
  on lines 2660..2662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2660-2662)
  on lines 2664..2665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2664-2665)
  on lines 2669..2670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2669-2670)
  on line 2674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2674-2674)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2510..2512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2510-2512)
  on lines 2514..2515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2514-2515)
  on line 2519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2519-2519)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1770..1772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1770-1772)
  on lines 1774..1775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1774-1775)
  on line 1778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1778-1778)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1581..1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1581-1583)
  on lines 1585..1586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1585-1586)
  on line 1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1589-1589)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1844..1846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1844-1846)
  on lines 1848..1849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1848-1849)
  on line 1852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1852-1852)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1618..1620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1618-1620)
  on lines 1622..1623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1622-1623)
  on line 1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1626-1626)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1733..1735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1733-1735)
  on lines 1737..1738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1737-1738)
  on line 1741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1741-1741)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:612-612)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:806-806)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:786-786)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1807..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1807-1809)
  on lines 1811..1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1811-1812)
  on line 1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1815-1815)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:569-569)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2846..2847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2846-2847)
  on lines 2857..2858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2857-2858)
  on lines 2868..2869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2868-2869)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2685..2686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2685-2686)
  on lines 2696..2697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2696-2697)
  on lines 2707..2708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2707-2708)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on lines 1788..1789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1788-1789)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 1599..1600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1599-1600)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on lines 1751..1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1751-1752)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on lines 1899..1900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1899-1900)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on lines 1825..1826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1825-1826)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on lines 1862..1863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1862-1863)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 1636..1637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1636-1637)
[Warning][Deadcode] Function 'sign' has dead code:
  on line 635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:635-635)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1508-1508)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:666-666)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 449
  dead: 718 (557 in uncalled functions)
  total lines: 1167
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1729:7-1729:18)
[Warning][Deadcode][CWE-570] condition '! privkey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:634:7-634:16)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2843:9-2843:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1748:7-1748:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2854:11-2854:21)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:663:9-663:16)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1766:7-1766:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2864:11-2864:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2865:13-2865:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1785:7-1785:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2682:9-2682:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.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_spec6_product28.cil.c:2693:11-2693:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1303:10-1303:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2703:11-2703:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2704:13-2704:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1822:7-1822:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1577:7-1577:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2937:7-2937:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2734:7-2734:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2735:9-2735:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1840:7-1840:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2506:9-2506:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1596:7-1596:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1859:7-1859:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1614:7-1614:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2967:11-2967:22)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:172:7-172:14)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2532:11-2532:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1633:7-1633:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:1896:7-1896:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2557:11-2557:22)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2793:11-2793:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2579:11-2579:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:228:7-228:10)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2802:9-2802:20)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring1_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2807:13-2807:50)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2627:7-2627:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product28.cil.c:2628:9-2628:19)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
