./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_spec11_product20.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_spec11_product20.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_spec11_product20.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_spec11_product20.cil.c:1571:3-1592:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1628:3-1653:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1713:5-1733: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_spec11_product20.cil.c:199:1-209:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:288:1-299:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:300:1-311:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:408:1-422:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:426:1-451:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:452:1-471:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:476:1-499:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:500:1-519:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:567:1-591:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:601:1-669:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:670:1-738:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1367:1-1390:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1391:1-1410:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1460:1-1469:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1500:1-1545:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1546:1-1601:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1602:1-1661:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1664:1-1766:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1767:1-1812:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1813:1-1858:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1881:1-1895:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2084:1-2098:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2226:1-2240:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2243:1-2261:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2262:1-2277:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2354:1-2374:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2375:1-2390:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2393:1-2413:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2414:1-2429:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2506:1-2524:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2525:1-2540:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2543:1-2561:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2562:1-2577:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2580:1-2598:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2599:1-2614:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2618:1-2645:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2646:1-2664:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2694:1-2702:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:54-54)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1092-1092)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2715-2715)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:817-819)
  on lines 821..822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:821-822)
  on lines 827..830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:827-830)
  on lines 832..834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:832-834)
  on lines 836..838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:836-838)
  on lines 840..841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:840-841)
  on lines 846..849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:846-849)
  on lines 851..853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:851-853)
  on lines 855..857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:855-857)
  on lines 859..860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:859-860)
  on lines 865..866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:865-866)
  on line 870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:870-870)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:544-544)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:953-953)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:1220-1222)
  on lines 1224..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1224-1225)
  on lines 1229..1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1229-1232)
  on lines 1234..1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1234-1236)
  on lines 1238..1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1238-1239)
  on lines 1243..1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1243-1246)
  on lines 1248..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1248-1250)
  on lines 1252..1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1252-1253)
  on lines 1257..1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1257-1258)
  on line 1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:1042-1043)
  on line 1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:1113-1115)
  on lines 1117..1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1117-1118)
  on lines 1122..1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1122-1125)
  on lines 1127..1129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1127-1129)
  on lines 1131..1132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1131-1132)
  on lines 1136..1139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1136-1139)
  on lines 1141..1143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1141-1143)
  on lines 1145..1146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1145-1146)
  on lines 1150..1151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1150-1151)
  on line 1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1155-1155)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1000-1000)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2478..2479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2478-2479)
  on line 2485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2485-2485)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2289..2290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2289-2290)
  on line 2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2296-2296)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2326..2327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2326-2327)
  on line 2333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2333-2333)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2137-2137)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2146-2146)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2441..2442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2441-2442)
  on line 2448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2448-2448)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2163..2164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2163-2164)
  on line 2171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2171-2171)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2691-2691)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2671-2671)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2128-2128)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 884..885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:884-885)
  on lines 892..894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:892-894)
  on lines 896..897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:896-897)
  on lines 899..900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:899-900)
  on lines 907..909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:907-909)
  on lines 911..912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:911-912)
  on lines 914..915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:747-748)
  on lines 750..751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:750-751)
  on lines 758..760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:758-760)
  on lines 762..763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:762-763)
  on lines 765..766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:765-766)
  on lines 773..775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:773-775)
  on lines 777..778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:777-778)
  on lines 780..781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:554-555)
  on lines 557..558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:557-558)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:961-961)
  on lines 966..967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:966-967)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1327..1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1327-1328)
  on lines 1338..1339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1338-1339)
  on lines 1349..1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:1166-1167)
  on lines 1177..1178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1177-1178)
  on lines 1188..1189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1188-1189)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2496-2496)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2307-2307)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2459-2459)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2344-2344)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1490-1490)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 539
  dead: 619 (446 in uncalled functions)
  total lines: 1158
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2306:9-2306:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.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_spec11_product20.cil.c:2325:9-2325:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2343:9-2343:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.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_spec11_product20.cil.c:1013:11-1013:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:1038:11-1038:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1060:11-1060:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2162:9-2162:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2440:9-2440:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.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_spec11_product20.cil.c:877:7-877:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:2458:9-2458:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:2477:9-2477:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1335:11-1335:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:2758:10-2758:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:2495:9-2495:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1346:13-1346:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:243:7-243:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:2288:9-2288:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:743:7-743:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.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_spec11_product20.cil.c:551:7-551:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:960:7-960:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1184:11-1184:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:1185:13-1185:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product20.cil.c:963:9-963: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
