./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_spec9_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_spec9_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_spec9_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_spec9_productSimulator.cil.c:1773:3-1794:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1830:3-1855:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1915:5-1935: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 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:358:1-372:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:394:1-409:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:486:1-506:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:507:1-522:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:525:1-545:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:546:1-561:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1120:1-1134:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1486:1-1496:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1575:1-1586:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1587:1-1598:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1702:1-1747:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1748:1-1803:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1804:1-1863:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1866:1-1968:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1969:1-2014:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2015:1-2060:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2390:1-2398:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2416:1-2430:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2441:1-2455:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2459:1-2484:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2485:1-2504:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2509:1-2532:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2533:1-2552:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2600:1-2624:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2634:1-2702:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2703:1-2771:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1692-1692)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 3125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3125-3125)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2411-2411)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 3349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3349-3349)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2850..2852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2850-2852)
  on lines 2854..2855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2854-2855)
  on lines 2860..2863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2860-2863)
  on lines 2865..2867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2865-2867)
  on lines 2869..2871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2869-2871)
  on lines 2873..2874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2873-2874)
  on lines 2879..2882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2879-2882)
  on lines 2884..2886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2884-2886)
  on lines 2888..2890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2888-2890)
  on lines 2892..2893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2892-2893)
  on lines 2898..2899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2898-2899)
  on line 2903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2903-2903)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 2577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2577-2577)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2986-2986)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 3421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3421-3421)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 3468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3468-3468)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 3253..3255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3253-3255)
  on lines 3257..3258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3257-3258)
  on lines 3262..3265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3262-3265)
  on lines 3267..3269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3267-3269)
  on lines 3271..3272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3271-3272)
  on lines 3276..3279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3276-3279)
  on lines 3281..3283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3281-3283)
  on lines 3285..3286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3285-3286)
  on lines 3290..3291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3290-3291)
  on line 3295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3295-3295)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 3075..3076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3075-3076)
  on line 3080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3080-3080)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 3146..3148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3146-3148)
  on lines 3150..3151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3150-3151)
  on lines 3155..3158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3155-3158)
  on lines 3160..3162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3160-3162)
  on lines 3164..3165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3164-3165)
  on lines 3169..3172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3169-3172)
  on lines 3174..3176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3174-3176)
  on lines 3178..3179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3178-3179)
  on lines 3183..3184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3183-3184)
  on line 3188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3188-3188)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 3033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3033-3033)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 610..611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:610-611)
  on line 617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:617-617)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 421..422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:421-422)
  on line 428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:428-428)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 384..385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:384-385)
  on line 391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:391-391)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 684..685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:684-685)
  on line 691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:691-691)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 458..459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:458-459)
  on line 465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:465-465)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1173-1173)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1182-1182)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 573..574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:573-574)
  on line 580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:580-580)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1199..1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1199-1200)
  on line 1207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1207-1207)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2383-2383)
  on line 2385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2385-2385)
  on line 2387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2387-2387)
[Warning][Deadcode] Function 'isReadable__before__Encrypt' has dead code:
  on line 2349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2349-2349)
[Warning][Deadcode] Function 'isReadable__role__Encrypt' has dead code:
  on line 2369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2369-2369)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 647..648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:647-648)
  on line 654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:654-654)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 721..722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:721-722)
  on line 728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:728-728)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1164-1164)
[Warning][Deadcode] Function 'outgoing__before__AddressBook' has dead code:
  on line 848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:848-848)
  on line 850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:850-850)
[Warning][Deadcode] Function 'printMail__before__Sign' has dead code:
  on line 2270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2270-2270)
  on line 2272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2272-2272)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 2112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2112-2112)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2917..2918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2917-2918)
  on lines 2925..2927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2925-2927)
  on lines 2929..2930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2929-2930)
  on lines 2932..2933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2932-2933)
  on lines 2940..2942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2940-2942)
  on lines 2944..2945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2944-2945)
  on lines 2947..2948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2947-2948)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2780..2781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2780-2781)
  on lines 2783..2784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2783-2784)
  on lines 2791..2793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2791-2793)
  on lines 2795..2796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2795-2796)
  on lines 2798..2799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2798-2799)
  on lines 2806..2808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2806-2808)
  on lines 2810..2811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2810-2811)
  on lines 2813..2814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2813-2814)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 2587..2588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2587-2588)
  on lines 2590..2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2590-2591)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2994-2994)
  on lines 2999..3000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2999-3000)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 3429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3429-3429)
  on lines 3434..3435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3434-3435)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 3360..3361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3360-3361)
  on lines 3371..3372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3371-3372)
  on lines 3382..3383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3382-3383)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 3199..3200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3199-3200)
  on lines 3210..3211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3210-3211)
  on lines 3221..3222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3221-3222)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:628-628)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:439-439)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:591-591)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:739-739)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:665-665)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:702-702)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:476-476)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2182-2182)
  on line 2198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2198-2198)
  on line 2207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2207-2207)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 818
  dead: 553 (351 in uncalled functions)
  total lines: 1371
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:475:9-475:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3378:11-3378:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3379:13-3379:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3428:7-3428:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2584:7-2584:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2993:7-2993:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3431:9-3431:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2996:9-2996:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:572:9-572:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3481:11-3481:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3046:11-3046:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:590:9-590:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:1198:9-1198:21)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Encrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2146:7-2146:35)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:609:9-609:20)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Decrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2151:11-2151:39)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3071:11-3071:22)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2154:13-2154:39)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:109:10-109:11)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Encrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2156:15-2156:43)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:627:9-627:20)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Keys' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2174:29-2174:52)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3093:11-3093:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:646:9-646:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:664:9-664:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3141:7-3141:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3142:9-3142:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:683:9-683:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:701:9-701:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:720:9-720:20)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2263:7-2263:33)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:738:9-738:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3196:9-3196:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3207:11-3207:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2776:7-2776:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2777:9-2777:19)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3217:11-3217:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3218:13-3218:23)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:841:7-841:33)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3248:7-3248:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3249:9-3249:19)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2376:7-2376:33)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2841:7-2841:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2846:11-2846:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:383:9-383:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:420:9-420:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2910:7-2910:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:438:9-438:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:2914:11-2914:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3357:9-3357:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:457:9-457:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_productSimulator.cil.c:3368:11-3368: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
