./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_spec27_product23.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_spec27_product23.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_spec27_product23.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_spec27_product23.cil.c:2364:3-2385:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2421:3-2446:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2506:5-2526: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_spec27_product23.cil.c:190:1-200:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:279:1-290:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:291:1-302:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:433:1-447:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:451:1-476:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:477:1-496:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:501:1-524:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:525:1-544:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:592:1-616:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:626:1-694:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:695:1-763:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1392:1-1415:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1416:1-1435:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1632:1-1646:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1825:1-1834:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1860:1-1874:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1888:1-1902:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1905:1-1923:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1924:1-1939:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2016:1-2036:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2037:1-2052:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2055:1-2075:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2076:1-2091:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2094:1-2112:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2113:1-2128:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2131:1-2149:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2150:1-2165:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2293:1-2338:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2339:1-2394:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2395:1-2454:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2457:1-2559:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2560:1-2605:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2606:1-2651:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2655:1-2682:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2683:1-2701:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2702:1-2715:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2725:1-2733:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2283-2283)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1117-1117)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2746-2746)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1328..1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1328-1329)
  on line 1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1341-1341)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 842..844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:842-844)
  on lines 846..847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:846-847)
  on lines 852..855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:852-855)
  on lines 857..859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:857-859)
  on lines 861..863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:861-863)
  on lines 865..866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:865-866)
  on lines 871..874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:871-874)
  on lines 876..878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:876-878)
  on lines 880..882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:880-882)
  on lines 884..885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:884-885)
  on lines 890..891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:890-891)
  on line 895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:895-895)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:569-569)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:978-978)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1460-1460)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1245..1247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1245-1247)
  on lines 1249..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1249-1250)
  on lines 1254..1257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1254-1257)
  on lines 1259..1261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1259-1261)
  on lines 1263..1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1263-1264)
  on lines 1268..1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1268-1271)
  on lines 1273..1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1273-1275)
  on lines 1277..1278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1277-1278)
  on lines 1282..1283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1282-1283)
  on line 1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1287-1287)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1067..1068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1067-1068)
  on line 1072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1072-1072)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1138..1140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1138-1140)
  on lines 1142..1143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1142-1143)
  on lines 1147..1150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1147-1150)
  on lines 1152..1154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1152-1154)
  on lines 1156..1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1156-1157)
  on lines 1161..1164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1161-1164)
  on lines 1166..1168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1166-1168)
  on lines 1170..1171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1170-1171)
  on lines 1175..1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1175-1176)
  on line 1180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1180-1180)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1025-1025)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1951..1952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1951-1952)
  on line 1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1958-1958)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2214..2215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2214-2215)
  on line 2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2221-2221)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1988..1989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1988-1989)
  on line 1995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1995-1995)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1685-1685)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1694-1694)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1711..1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1711-1712)
  on line 1719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1719-1719)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2722-2722)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2177..2178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2177-2178)
  on line 2184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2184-2184)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2251..2252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2251-2252)
  on line 2258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2258-2258)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1676-1676)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 909..910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:909-910)
  on lines 917..919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:917-919)
  on lines 921..922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:921-922)
  on lines 924..925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:924-925)
  on lines 932..934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:932-934)
  on lines 936..937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:936-937)
  on lines 939..940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:939-940)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 772..773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:772-773)
  on lines 775..776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:775-776)
  on lines 783..785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:783-785)
  on lines 787..788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:787-788)
  on lines 790..791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:790-791)
  on lines 798..800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:798-800)
  on lines 802..803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:802-803)
  on lines 805..806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:805-806)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 579..580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:579-580)
  on lines 582..583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:582-583)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:986-986)
  on lines 991..992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:991-992)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1352..1353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1352-1353)
  on lines 1363..1364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1363-1364)
  on lines 1374..1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1374-1375)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1191..1192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1191-1192)
  on lines 1202..1203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1202-1203)
  on lines 1213..1214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1213-1214)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1969-1969)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2269-2269)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2195-2195)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2232-2232)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2006-2006)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1855-1855)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1798-1798)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 554
  dead: 616 (437 in uncalled functions)
  total lines: 1170
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2005:9-2005:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1710:9-1710:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:768:7-768:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:769:9-769:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:576:7-576:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:985:7-985:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1209:11-1209:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1210:13-1210:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:988:9-988:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2268:9-2268:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1240:7-1240:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1241:9-1241:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1788:7-1788:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:833:7-833:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1473:11-1473:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1038:11-1038:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:838:11-838:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1063:11-1063:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1085:11-1085:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1133:7-1133:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1134:9-1134:19)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring2_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1327:15-1327:52)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:902:7-902:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2176:9-2176:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:906:11-906:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1349:9-1349:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2194:9-2194:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1950:9-1950:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1360:11-1360:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2213:9-2213:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2789:10-2789:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1370:11-1370:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1371:13-1371:23)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:234:7-234:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1968:9-1968:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2231:9-2231:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1987:9-1987:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1188:9-1188:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:2250:9-2250:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product23.cil.c:1199:11-1199:21)
[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
