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


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1651:3-1672:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1708:3-1733:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1793:5-1813: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_spec11_product35.cil.c:71:1-85:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:107:1-122:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:199:1-219:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:220:1-235:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:238:1-258:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:259:1-274:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:490:1-504:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:508:1-533:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:534:1-553:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:558:1-581:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:582:1-601:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:649:1-673:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:683:1-751:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:752:1-820:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1580:1-1625:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1626:1-1681:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1682:1-1741:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1744:1-1846:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1847:1-1892:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1893:1-1938:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2175:1-2189:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2303:1-2311:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2558:1-2572:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2780:1-2789:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2911:1-2921:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:3000:1-3011:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:3012:1-3023:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2772-2772)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1174-1174)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2324-2324)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1398-1398)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 899..901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:899-901)
  on lines 903..904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:903-904)
  on lines 909..912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:909-912)
  on lines 914..916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:914-916)
  on lines 918..920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:918-920)
  on lines 922..923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:922-923)
  on lines 928..931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:928-931)
  on lines 933..935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:933-935)
  on lines 937..939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:937-939)
  on lines 941..942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:941-942)
  on lines 947..948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:947-948)
  on line 952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:952-952)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:626-626)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1035-1035)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1470-1470)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1517-1517)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1302..1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1302-1304)
  on lines 1306..1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1306-1307)
  on lines 1311..1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1311-1314)
  on lines 1316..1318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1316-1318)
  on lines 1320..1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1320-1321)
  on lines 1325..1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1325-1328)
  on lines 1330..1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1330-1332)
  on lines 1334..1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1334-1335)
  on lines 1339..1340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1339-1340)
  on line 1344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1344-1344)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1124..1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1124-1125)
  on line 1129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1129-1129)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1195..1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1195-1197)
  on lines 1199..1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1199-1200)
  on lines 1204..1207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1204-1207)
  on lines 1209..1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1209-1211)
  on lines 1213..1214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1213-1214)
  on lines 1218..1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1218-1221)
  on lines 1223..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1223-1225)
  on lines 1227..1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1227-1228)
  on lines 1232..1233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1232-1233)
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1237-1237)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1082-1082)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 323..324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:323-324)
  on line 330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:330-330)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 134..135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:134-135)
  on line 141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:141-141)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 97..98 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:97-98)
  on line 104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:104-104)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 397..398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:397-398)
  on line 404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:404-404)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 171..172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:171-172)
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:178-178)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2611-2611)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2620-2620)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 286..287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:286-287)
  on line 293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:293-293)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2637..2638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2637-2638)
  on line 2645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2645-2645)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2300-2300)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2280-2280)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 360..361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:360-361)
  on line 367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:367-367)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 434..435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:434-435)
  on line 441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:441-441)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2602-2602)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 966..967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:966-967)
  on lines 974..976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:974-976)
  on lines 978..979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:978-979)
  on lines 981..982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:981-982)
  on lines 989..991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:989-991)
  on lines 993..994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:993-994)
  on lines 996..997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:996-997)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 829..830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:829-830)
  on lines 832..833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:832-833)
  on lines 840..842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:840-842)
  on lines 844..845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:844-845)
  on lines 847..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:847-848)
  on lines 855..857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:855-857)
  on lines 859..860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:859-860)
  on lines 862..863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:862-863)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 636..637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:636-637)
  on lines 639..640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:639-640)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1043-1043)
  on lines 1048..1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1048-1049)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1478-1478)
  on lines 1483..1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1483-1484)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1409..1410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1409-1410)
  on lines 1420..1421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1420-1421)
  on lines 1431..1432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1431-1432)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1248..1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1248-1249)
  on lines 1259..1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1259-1260)
  on lines 1270..1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1270-1271)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:341-341)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:152-152)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:304-304)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:452-452)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:378-378)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:415-415)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:189-189)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2810-2810)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 686
  dead: 547 (355 in uncalled functions)
  total lines: 1233
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1142:11-1142:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1190:7-1190:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1191:9-1191:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:959:7-959:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:963:11-963:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:285:9-285:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1990:10-1990:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1406:9-1406:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1417:11-1417:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:303:9-303:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1427:11-1427:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1428:13-1428:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:322:9-322:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1245:9-1245:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:340:9-340:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:96:9-96:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2955:7-2955:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1256:11-1256:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:359:9-359:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:2636:9-2636:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:825:7-825:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1477:7-1477:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:826:9-826:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:633:7-633:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1042:7-1042:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1266:11-1266:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1480:9-1480:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1267:13-1267:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1045:9-1045:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:377:9-377:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:133:9-133:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1297:7-1297:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1298:9-1298:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:396:9-396:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:151:9-151:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:414:9-414:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:170:9-170:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:890:7-890:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1530:11-1530:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1095:11-1095:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:895:11-895:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:433:9-433:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:188:9-188:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:1120:11-1120:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product35.cil.c:451:9-451: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
