./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_spec1_productSimulator.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_spec1_productSimulator.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_spec1_productSimulator.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_spec1_productSimulator.cil.c:2002:3-2023:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2059:3-2084:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2144:5-2164: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 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:559:1-567:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:952:1-966:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1163:1-1177:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1199:1-1214:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1291:1-1311:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1312:1-1327:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1330:1-1350:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1351:1-1366:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1715:1-1725:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1804:1-1815:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1816:1-1827:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1931:1-1976:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1977:1-2032:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2033:1-2092:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2095:1-2197:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2198:1-2243:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2244:1-2289:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2300:1-2314:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2318:1-2343:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2344:1-2363:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2368:1-2391:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2392:1-2411:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2459:1-2483:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2493:1-2561:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2562:1-2630:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3459:1-3473:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1921-1921)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2984-2984)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:580-580)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 3208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3208-3208)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2709..2711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2709-2711)
  on lines 2713..2714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2713-2714)
  on lines 2719..2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2719-2722)
  on lines 2724..2726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2724-2726)
  on lines 2728..2730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2728-2730)
  on lines 2732..2733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2732-2733)
  on lines 2738..2741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2738-2741)
  on lines 2743..2745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2743-2745)
  on lines 2747..2749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2747-2749)
  on lines 2751..2752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2751-2752)
  on lines 2757..2758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2757-2758)
  on line 2762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2762-2762)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 2436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2436-2436)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2845-2845)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 3280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3280-3280)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 3327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3327-3327)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 3112..3114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3112-3114)
  on lines 3116..3117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3116-3117)
  on lines 3121..3124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3121-3124)
  on lines 3126..3128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3126-3128)
  on lines 3130..3131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3130-3131)
  on lines 3135..3138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3135-3138)
  on lines 3140..3142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3140-3142)
  on lines 3144..3145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3144-3145)
  on lines 3149..3150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3149-3150)
  on line 3154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3154-3154)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2934..2935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2934-2935)
  on line 2939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2939-2939)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 3005..3007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3005-3007)
  on lines 3009..3010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3009-3010)
  on lines 3014..3017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3014-3017)
  on lines 3019..3021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3019-3021)
  on lines 3023..3024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3023-3024)
  on lines 3028..3031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3028-3031)
  on lines 3033..3035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3033-3035)
  on lines 3037..3038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3037-3038)
  on lines 3042..3043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3042-3043)
  on line 3047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3047-3047)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2892-2892)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1415..1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1415-1416)
  on line 1422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1422-1422)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1226..1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1226-1227)
  on line 1233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1233-1233)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1189..1190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1189-1190)
  on line 1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1196-1196)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1489..1490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1489-1490)
  on line 1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1496-1496)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1263..1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1263-1264)
  on line 1270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1270-1270)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1005-1005)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1014-1014)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1378..1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1378-1379)
  on line 1385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1385-1385)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1031..1032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1031-1032)
  on line 1039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1039-1039)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:552-552)
  on line 554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:554-554)
  on line 556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:556-556)
[Warning][Deadcode] Function 'isReadable__before__Encrypt' has dead code:
  on line 518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:518-518)
[Warning][Deadcode] Function 'isReadable__role__Encrypt' has dead code:
  on line 538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:538-538)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1452..1453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1452-1453)
  on line 1459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1459-1459)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1526..1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1526-1527)
  on line 1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1533-1533)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:996-996)
[Warning][Deadcode] Function 'outgoing__before__AddressBook' has dead code:
  on line 685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:685-685)
  on line 687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:687-687)
[Warning][Deadcode] Function 'printMail__before__Sign' has dead code:
  on line 439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:439-439)
  on line 441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:441-441)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 3359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3359-3359)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2776..2777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2776-2777)
  on lines 2784..2786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2784-2786)
  on lines 2788..2789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2788-2789)
  on lines 2791..2792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2791-2792)
  on lines 2799..2801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2799-2801)
  on lines 2803..2804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2803-2804)
  on lines 2806..2807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2806-2807)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2639..2640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2639-2640)
  on lines 2642..2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2642-2643)
  on lines 2650..2652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2650-2652)
  on lines 2654..2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2654-2655)
  on lines 2657..2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2657-2658)
  on lines 2665..2667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2665-2667)
  on lines 2669..2670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2669-2670)
  on lines 2672..2673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2672-2673)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 2446..2447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2446-2447)
  on lines 2449..2450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2449-2450)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2853-2853)
  on lines 2858..2859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2858-2859)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 3288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3288-3288)
  on lines 3293..3294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3293-3294)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 3219..3220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3219-3220)
  on lines 3230..3231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3230-3231)
  on lines 3241..3242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3241-3242)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 3058..3059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3058-3059)
  on lines 3069..3070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3069-3070)
  on lines 3080..3081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3080-3081)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1433-1433)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1244-1244)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1396-1396)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1544-1544)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1470-1470)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1507-1507)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1281-1281)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3429-3429)
  on line 3445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3445-3445)
  on line 3454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3454-3454)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 810
  dead: 553 (351 in uncalled functions)
  total lines: 1363
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Encrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3393:7-3393:35)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Decrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3398:11-3398:39)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2952:11-2952:22)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3401:13-3401:39)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Encrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3403:15-3403:43)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:545:7-545:33)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Keys' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3421:29-3421:52)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1188:9-1188:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3000:7-3000:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3001:9-3001:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1225:9-1225:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1243:9-1243:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1262:9-1262:20)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:678:7-678:33)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3055:9-3055:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1280:9-1280:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3066:11-3066:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2635:7-2635:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2636:9-2636:19)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3076:11-3076:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:140:10-140:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3077:13-3077:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3107:7-3107:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3108:9-3108:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2700:7-2700:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2705:11-2705:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1377:9-1377:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1395:9-1395:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1414:9-1414:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1432:9-1432:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1451:9-1451:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2769:7-2769:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2773:11-2773:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3216:9-3216:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1469:9-1469:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3227:11-3227:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1488:9-1488:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3237:11-3237:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3238:13-3238:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1506:9-1506:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1525:9-1525:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3287:7-3287:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2443:7-2443:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2852:7-2852:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1543:9-1543:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3290:9-3290:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2855:9-2855:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:1030:9-1030:21)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:432:7-432:33)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:3340:11-3340:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2905:11-2905:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_productSimulator.cil.c:2930:11-2930:22)
[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
