./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_spec3_product30.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_spec3_product30.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_spec3_product30.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_spec3_product30.cil.c:697:3-718:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:754:3-779:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:839:5-859: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 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:75:1-102:1)
[Warning][Deadcode] Function 'printMail__wrappee__AutoResponder' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:103:1-121:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:122:1-140:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:141:1-154:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:184:1-192:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:230:1-244:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:247:1-265:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:266:1-281:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:358:1-378:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:379:1-394:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:397:1-417:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:418:1-433:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:584:1-602:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:626:1-671:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:672:1-727:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:728:1-787:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:790:1-892:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:893:1-938:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:939:1-984:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1111:1-1121:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1200:1-1211:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1212:1-1223:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1506:1-1515:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1713:1-1727:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1978:1-1992:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1996:1-2021:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2022:1-2041:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2046:1-2069:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2070:1-2089:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2093:1-2116:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2117:1-2136:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2137:1-2161:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2171:1-2239:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2240:1-2308:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2309:1-2364:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2374:1-2442:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2443:1-2498:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2937:1-2960:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2961:1-2980:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:3030:1-3044:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:214-214)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2662-2662)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:205-205)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2868..2870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2868-2870)
  on lines 2872..2874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2872-2874)
  on lines 2876..2877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2876-2877)
  on line 2886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2886-2886)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 2515..2516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2515-2516)
  on line 2523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2523-2523)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2997..2998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2997-2998)
  on line 3005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:3005-3005)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2790..2792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2790-2792)
  on lines 2794..2795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2794-2795)
  on lines 2799..2802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2799-2802)
  on lines 2804..2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2804-2806)
  on lines 2808..2809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2808-2809)
  on lines 2813..2816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2813-2816)
  on lines 2818..2820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2818-2820)
  on lines 2822..2823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2822-2823)
  on lines 2827..2828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2827-2828)
  on line 2832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2832-2832)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2612..2613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2612-2613)
  on line 2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2617-2617)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2683..2685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2683-2685)
  on lines 2687..2688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2687-2688)
  on lines 2692..2695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2692-2695)
  on lines 2697..2699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2697-2699)
  on lines 2701..2702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2701-2702)
  on lines 2706..2709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2706-2709)
  on lines 2711..2713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2711-2713)
  on lines 2715..2716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2715-2716)
  on lines 2720..2721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2720-2721)
  on line 2725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2725-2725)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2562..2563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2562-2563)
  on line 2570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2570-2570)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 482..483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:482-483)
  on line 489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:489-489)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 293..294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:293-294)
  on line 300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:300-300)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 556..557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:556-557)
  on line 563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:563-563)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 330..331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:330-331)
  on line 337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:337-337)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1766-1766)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1775-1775)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 445..446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:445-446)
  on line 452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:452-452)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1792..1793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1792-1793)
  on line 1800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1800-1800)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:181-181)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:161-161)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 519..520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:519-520)
  on line 526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:526-526)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1757-1757)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2531-2531)
  on lines 2536..2537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2536-2537)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2897..2898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2897-2898)
  on lines 2908..2909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2908-2909)
  on lines 2919..2920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2919-2920)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2736..2737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2736-2737)
  on lines 2747..2748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2747-2748)
  on lines 2758..2759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2758-2759)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:500-500)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:311-311)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:463-463)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:611-611)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:537-537)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:574-574)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:348-348)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1536-1536)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 540
  dead: 653 (528 in uncalled functions)
  total lines: 1193
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2630:11-2630:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:499:9-499:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:518:9-518:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2867:11-2867:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2678:7-2678:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2679:9-2679:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1155:7-1155:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:536:9-536:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:292:9-292:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2894:9-2894:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:555:9-555:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:310:9-310:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2905:11-2905:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:573:9-573:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1791:9-1791:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:329:9-329:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2915:11-2915:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2916:13-2916:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:347:9-347:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2733:9-2733:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2514:11-2514:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:610:9-610:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2744:11-2744:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2530:7-2530:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2754:11-2754:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2755:13-2755:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2533:9-2533:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2785:7-2785:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2786:9-2786:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2996:11-2996:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2561:11-2561:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:1328:10-1328:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:3018:11-3018:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2583:11-2583:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:444:9-444:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:2608:11-2608:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:462:9-462:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product30.cil.c:481:9-481: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
