./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_spec4_product34.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_spec4_product34.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_spec4_product34.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_spec4_product34.cil.c:2784:3-2805:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2841:3-2866:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2926:5-2946: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_spec4_product34.cil.c:199:1-209:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:288:1-299:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:300:1-311:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:408:1-422:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:426:1-451:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:452:1-471:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:476:1-499:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:500:1-519:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:567:1-591:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:601:1-669:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:670:1-738:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:932:1-955:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:956:1-975:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1686:1-1700:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1884:1-1898:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1920:1-1935:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2012:1-2032:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2033:1-2048:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2051:1-2071:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2072:1-2087:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2494:1-2503:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2556:1-2570:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2682:1-2690:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2713:1-2758:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2759:1-2814:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2815:1-2874:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2877:1-2979:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2980:1-3025:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:3026:1-3071:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:54-54)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1092-1092)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2703-2703)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1316-1316)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 817..819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:817-819)
  on lines 821..822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:821-822)
  on lines 827..830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:827-830)
  on lines 832..834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:832-834)
  on lines 836..838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:836-838)
  on lines 840..841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:840-841)
  on lines 846..849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:846-849)
  on lines 851..853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:851-853)
  on lines 855..857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:855-857)
  on lines 859..860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:859-860)
  on lines 865..866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:865-866)
  on line 870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:870-870)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 536..537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:536-537)
  on line 544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:544-544)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1372..1373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1372-1373)
  on line 1388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1388-1388)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1427..1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1427-1428)
  on line 1435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1435-1435)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1220..1222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1220-1222)
  on lines 1224..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1224-1225)
  on lines 1229..1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1229-1232)
  on lines 1234..1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1234-1236)
  on lines 1238..1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1238-1239)
  on lines 1243..1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1243-1246)
  on lines 1248..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1248-1250)
  on lines 1252..1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1252-1253)
  on lines 1257..1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1257-1258)
  on line 1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1262-1262)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1042..1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1042-1043)
  on line 1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1047-1047)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1113..1115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1113-1115)
  on lines 1117..1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1117-1118)
  on lines 1122..1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1122-1125)
  on lines 1127..1129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1127-1129)
  on lines 1131..1132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1131-1132)
  on lines 1136..1139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1136-1139)
  on lines 1141..1143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1141-1143)
  on lines 1145..1146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1145-1146)
  on lines 1150..1151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1150-1151)
  on line 1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1155-1155)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1000-1000)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2136..2137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2136-2137)
  on line 2143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2143-2143)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1947..1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1947-1948)
  on line 1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1954-1954)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1910..1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1910-1911)
  on line 1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1917-1917)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2210..2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2210-2211)
  on line 2217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2217-2217)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1984..1985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1984-1985)
  on line 1991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1991-1991)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1739-1739)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1748-1748)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2099..2100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2099-2100)
  on line 2106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2106-2106)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1765..1766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1765-1766)
  on line 1773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1773-1773)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2679-2679)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2659-2659)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2173..2174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2173-2174)
  on line 2180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2180-2180)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2247..2248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2247-2248)
  on line 2254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2254-2254)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1730-1730)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 884..885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:884-885)
  on lines 892..894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:892-894)
  on lines 896..897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:896-897)
  on lines 899..900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:899-900)
  on lines 907..909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:907-909)
  on lines 911..912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:911-912)
  on lines 914..915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:914-915)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 747..748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:747-748)
  on lines 750..751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:750-751)
  on lines 758..760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:758-760)
  on lines 762..763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:762-763)
  on lines 765..766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:765-766)
  on lines 773..775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:773-775)
  on lines 777..778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:777-778)
  on lines 780..781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:780-781)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 554..555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:554-555)
  on lines 557..558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:557-558)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1396-1396)
  on lines 1401..1402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1401-1402)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1327..1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1327-1328)
  on lines 1338..1339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1338-1339)
  on lines 1349..1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1349-1350)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1166..1167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1166-1167)
  on lines 1177..1178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1177-1178)
  on lines 1188..1189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1188-1189)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2154-2154)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1965-1965)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2117-2117)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2265-2265)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2191-2191)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2228-2228)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2002-2002)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2524-2524)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 648
  dead: 568 (374 in uncalled functions)
  total lines: 1216
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2001:9-2001:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1215:7-1215:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1216:9-1216:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2264:9-2264:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1426:11-1426:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1764:9-1764:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:808:7-808:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1448:11-1448:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1013:11-1013:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2313:10-2313:11)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:813:11-813:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1038:11-1038:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2098:9-2098:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1060:11-1060:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2116:9-2116:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2135:9-2135:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1108:7-1108:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1109:9-1109:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:877:7-877:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2153:9-2153:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:881:11-881:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1909:9-1909:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1324:9-1324:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2172:9-2172:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1335:11-1335:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1345:11-1345:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2190:9-2190:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1346:13-1346:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1946:9-1946:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1371:7-1371:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2209:9-2209:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1964:9-1964:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1163:9-1163:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:243:7-243:10)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:535:11-535:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2227:9-2227:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1174:11-1174:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1983:9-1983:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:743:7-743:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1395:7-1395:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:744:9-744:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:551:7-551:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1184:11-1184:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1398:9-1398:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:1185:13-1185:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product34.cil.c:2246:9-2246: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
