./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_product34.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_product34.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_product34.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_product34.cil.c:195:3-216:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:252:3-277:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:337:5-357:5 with factor 2
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:102:1-116:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:124:1-169:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:170:1-225:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:226:1-285:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:288:1-390:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:391:1-436:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:437:1-482:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:513:1-527:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:531:1-556:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:557:1-576:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:581:1-604:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:605:1-624:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:672:1-696:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:706:1-774:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:775:1-843:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1037:1-1060:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1061:1-1080:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1568:1-1577:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1833:1-1847:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2363:1-2371:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2395:1-2409:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2431:1-2446:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2523:1-2543:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2544:1-2559:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2562:1-2582:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2583:1-2598:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2882:1-2892:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2971:1-2982:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2983:1-2994:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 96 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:96-96)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1197-1197)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2384-2384)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1421-1421)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 922..924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:922-924)
  on lines 926..927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:926-927)
  on lines 932..935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:932-935)
  on lines 937..939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:937-939)
  on lines 941..943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:941-943)
  on lines 945..946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:945-946)
  on lines 951..954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:951-954)
  on lines 956..958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:956-958)
  on lines 960..962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:960-962)
  on lines 964..965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:964-965)
  on lines 970..971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:970-971)
  on line 975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:975-975)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 641..642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:641-642)
  on line 649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:649-649)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1477..1478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1477-1478)
  on line 1493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1493-1493)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1532..1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1532-1533)
  on line 1540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1540-1540)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1325..1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1325-1327)
  on lines 1329..1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1329-1330)
  on lines 1334..1337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1334-1337)
  on lines 1339..1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1339-1341)
  on lines 1343..1344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1343-1344)
  on lines 1348..1351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1348-1351)
  on lines 1353..1355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1353-1355)
  on lines 1357..1358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1357-1358)
  on lines 1362..1363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1362-1363)
  on line 1367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1367-1367)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1147..1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1147-1148)
  on line 1152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1152-1152)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1218..1220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1218-1220)
  on lines 1222..1223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1222-1223)
  on lines 1227..1230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1227-1230)
  on lines 1232..1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1232-1234)
  on lines 1236..1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1236-1237)
  on lines 1241..1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1241-1244)
  on lines 1246..1248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1246-1248)
  on lines 1250..1251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1250-1251)
  on lines 1255..1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1255-1256)
  on line 1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1260-1260)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1105-1105)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2647..2648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2647-2648)
  on line 2654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2654-2654)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2458..2459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2458-2459)
  on line 2465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2465-2465)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2421..2422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2421-2422)
  on line 2428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2428-2428)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2721..2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2721-2722)
  on line 2728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2728-2728)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2495..2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2495-2496)
  on line 2502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2502-2502)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1886-1886)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1895-1895)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2610..2611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2610-2611)
  on line 2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2617-2617)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1912..1913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1912-1913)
  on line 1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1920-1920)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2360-2360)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2340-2340)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2684..2685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2684-2685)
  on line 2691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2691-2691)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2758..2759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2758-2759)
  on line 2765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2765-2765)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1877-1877)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 989..990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:989-990)
  on lines 997..999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:997-999)
  on lines 1001..1002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1001-1002)
  on lines 1004..1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1004-1005)
  on lines 1012..1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1012-1014)
  on lines 1016..1017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1016-1017)
  on lines 1019..1020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1019-1020)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 852..853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:852-853)
  on lines 855..856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:855-856)
  on lines 863..865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:863-865)
  on lines 867..868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:867-868)
  on lines 870..871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:870-871)
  on lines 878..880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:878-880)
  on lines 882..883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:882-883)
  on lines 885..886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:885-886)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 659..660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:659-660)
  on lines 662..663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:662-663)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1501-1501)
  on lines 1506..1507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1506-1507)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1432..1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1432-1433)
  on lines 1443..1444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1443-1444)
  on lines 1454..1455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1454-1455)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1271..1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1271-1272)
  on lines 1282..1283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1282-1283)
  on lines 1293..1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1293-1294)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2665-2665)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2476-2476)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2628-2628)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2776-2776)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2702-2702)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2739-2739)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2513-2513)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1598-1598)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 648
  dead: 568 (374 in uncalled functions)
  total lines: 1216
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2512:9-2512:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1213:7-1213:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2775:9-2775:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1214:9-1214:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:982:7-982:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:986:11-986:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1429:9-1429:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1440:11-1440:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2071:10-2071:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1450:11-1450:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1451:13-1451:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1476:7-1476:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1268:9-1268:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2609:9-2609:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:640:11-640:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1279:11-1279:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:848:7-848:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1500:7-1500:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:849:9-849:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:656:7-656:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2627:9-2627:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1289:11-1289:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1503:9-1503:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1290:13-1290:23)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2926:7-2926:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2646:9-2646:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1320:7-1320:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1321:9-1321:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1531:11-1531:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2664:9-2664:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2420:9-2420:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2683:9-2683:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:913:7-913:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1553:11-1553:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1118:11-1118:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:918:11-918:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2701:9-2701:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2457:9-2457:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1911:9-1911:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1143:11-1143:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2720:9-2720:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2475:9-2475:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2738:9-2738:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2494:9-2494:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:1165:11-1165:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product34.cil.c:2757:9-2757: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
