./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_spec7_product35.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec7_product35.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1846:3-1867:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1903:3-1928:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1988:5-2008: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 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:201:1-209:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:471:1-485:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:699:1-713:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:717:1-742:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:743:1-762:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:767:1-790:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:791:1-810:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:858:1-882:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:892:1-960:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:961:1-1029:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1775:1-1820:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1821:1-1876:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1877:1-1936:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1939:1-2041:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2042:1-2087:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2088:1-2133:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2148:1-2157:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2291:1-2301:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2380:1-2391:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2392:1-2403:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2499:1-2513:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2535:1-2550:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2627:1-2647:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2648:1-2663:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2666:1-2686:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2687:1-2702:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2140-2140)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1383-1383)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:222-222)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1607-1607)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1108..1110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1108-1110)
  on lines 1112..1113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1112-1113)
  on lines 1118..1121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1118-1121)
  on lines 1123..1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1123-1125)
  on lines 1127..1129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1127-1129)
  on lines 1131..1132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1131-1132)
  on lines 1137..1140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1137-1140)
  on lines 1142..1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1142-1144)
  on lines 1146..1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1146-1148)
  on lines 1150..1151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1150-1151)
  on lines 1156..1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1156-1157)
  on line 1161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1161-1161)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:835-835)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1244-1244)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1679-1679)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1726-1726)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1511..1513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1511-1513)
  on lines 1515..1516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1515-1516)
  on lines 1520..1523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1520-1523)
  on lines 1525..1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1525-1527)
  on lines 1529..1530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1529-1530)
  on lines 1534..1537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1534-1537)
  on lines 1539..1541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1539-1541)
  on lines 1543..1544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1543-1544)
  on lines 1548..1549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1548-1549)
  on line 1553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1553-1553)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1333..1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1333-1334)
  on line 1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1338-1338)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1404..1406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1404-1406)
  on lines 1408..1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1408-1409)
  on lines 1413..1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1413-1416)
  on lines 1418..1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1418-1420)
  on lines 1422..1423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1422-1423)
  on lines 1427..1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1427-1430)
  on lines 1432..1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1432-1434)
  on lines 1436..1437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1436-1437)
  on lines 1441..1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1441-1442)
  on line 1446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1446-1446)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1291-1291)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2751..2752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2751-2752)
  on line 2758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2758-2758)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2562..2563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2562-2563)
  on line 2569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2569-2569)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2525..2526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2525-2526)
  on line 2532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2532-2532)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2825..2826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2825-2826)
  on line 2832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2832-2832)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2599..2600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2599-2600)
  on line 2606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2606-2606)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:524-524)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:533-533)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2714..2715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2714-2715)
  on line 2721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2721-2721)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 550..551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:550-551)
  on line 558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:558-558)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:198-198)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:178-178)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2788..2789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2788-2789)
  on line 2795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2795-2795)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2862..2863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2862-2863)
  on line 2869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2869-2869)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:515-515)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1175..1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1175-1176)
  on lines 1183..1185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1183-1185)
  on lines 1187..1188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1187-1188)
  on lines 1190..1191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1190-1191)
  on lines 1198..1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1198-1200)
  on lines 1202..1203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1202-1203)
  on lines 1205..1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1205-1206)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1038..1039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1038-1039)
  on lines 1041..1042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1041-1042)
  on lines 1049..1051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1049-1051)
  on lines 1053..1054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1053-1054)
  on lines 1056..1057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1056-1057)
  on lines 1064..1066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1064-1066)
  on lines 1068..1069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1068-1069)
  on lines 1071..1072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1071-1072)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 845..846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:845-846)
  on lines 848..849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:848-849)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1252-1252)
  on lines 1257..1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1257-1258)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1687-1687)
  on lines 1692..1693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1692-1693)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1618..1619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1618-1619)
  on lines 1629..1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1629-1630)
  on lines 1640..1641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1640-1641)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1457..1458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1457-1458)
  on lines 1468..1469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1468-1469)
  on lines 1479..1480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1479-1480)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2769-2769)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2580-2580)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2732-2732)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2880-2880)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2806-2806)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2843-2843)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2617-2617)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2178-2178)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 684
  dead: 547 (355 in uncalled functions)
  total lines: 1231
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1475:11-1475:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1689:9-1689:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1476:13-1476:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1254:9-1254:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2861:9-2861:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1506:7-1506:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2616:9-2616:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1507:9-1507:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2335:7-2335:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2879:9-2879:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1099:7-1099:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1739:11-1739:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1304:11-1304:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1104:11-1104:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2928:10-2928:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1329:11-1329:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2713:9-2713:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1351:11-1351:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2731:9-2731:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1399:7-1399:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1400:9-1400:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2750:9-2750:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1168:7-1168:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1172:11-1172:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2768:9-2768:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2524:9-2524:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1615:9-1615:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2787:9-2787:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1626:11-1626:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1636:11-1636:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1637:13-1637:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2805:9-2805:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2561:9-2561:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2824:9-2824:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1454:9-1454:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2579:9-2579:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:549:9-549:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1465:11-1465:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2842:9-2842:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1034:7-1034:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:2598:9-2598:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1686:7-1686:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1035:9-1035:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:842:7-842:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product35.cil.c:1251:7-1251:18)
[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
