./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_product14.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_product14.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_product14.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_product14.cil.c:1695:3-1716:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1752:3-1777:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1837:5-1857: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 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:78:1-92:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:96:1-121:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:122:1-141:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:146:1-169:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:170:1-189:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:237:1-261:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:271:1-339:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:340:1-408:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:602:1-625:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:626:1-645:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1037:1-1060:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1061:1-1080:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1349:1-1363:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1377:1-1386:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1396:1-1404:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1405:1-1413:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1462:1-1489:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1490:1-1508:1)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1509:1-1517:1)
[Warning][Deadcode] Function 'isReadable' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1518:1-1537:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1538:1-1546:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1564:1-1578:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1584:1-1593:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1624:1-1669:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1670:1-1725:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1726:1-1785:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1788:1-1890:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1891:1-1936:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1937:1-1982:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2306:1-2316:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2395:1-2406:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2407:1-2418:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2500:1-2514:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2517:1-2535:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2536:1-2551:1)
[Warning][Deadcode] Function 'getEmailFrom' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2554:1-2572:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2628:1-2648:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2649:1-2664:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2667:1-2687:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2688:1-2703:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2780:1-2798:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2799:1-2814:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2817:1-2835:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2836:1-2851:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2854:1-2872:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2873:1-2888:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2895-2895)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 2298..2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2298-2300)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:762-762)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1559-1559)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 953..956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:953-956)
  on lines 958..960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:958-960)
  on lines 962..963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:962-963)
  on lines 967..970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:967-970)
  on lines 972..974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:972-974)
  on lines 976..977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:976-977)
  on lines 981..982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:981-982)
  on line 986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:986-986)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 487..489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:487-489)
  on lines 491..492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:491-492)
  on lines 497..500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:497-500)
  on lines 502..504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:502-504)
  on lines 506..508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:506-508)
  on lines 510..511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:510-511)
  on lines 516..519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:516-519)
  on lines 521..523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:521-523)
  on lines 525..527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:525-527)
  on lines 529..530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:529-530)
  on lines 535..536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:535-536)
  on line 540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:540-540)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 201..203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:201-203)
  on lines 205..207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:205-207)
  on lines 209..210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:209-210)
  on line 214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:214-214)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1092..1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1092-1094)
  on lines 1096..1098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1096-1098)
  on lines 1100..1101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1100-1101)
  on line 1105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1105-1105)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 890..892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:890-892)
  on lines 894..895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:894-895)
  on lines 899..902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:899-902)
  on lines 904..906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:904-906)
  on lines 908..909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:908-909)
  on lines 913..916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:913-916)
  on lines 918..920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:918-920)
  on lines 922..923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:922-923)
  on lines 927..928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:927-928)
  on line 932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:932-932)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 712..713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:712-713)
  on line 717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:717-717)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 783..785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:783-785)
  on lines 787..788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:787-788)
  on lines 792..795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:792-795)
  on lines 797..799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:797-799)
  on lines 801..802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:801-802)
  on lines 806..809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:806-809)
  on lines 811..813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:811-813)
  on lines 815..816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:815-816)
  on lines 820..821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:820-821)
  on line 825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:825-825)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 654..655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:654-655)
  on line 670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:670-670)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2751..2753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2751-2753)
  on lines 2755..2756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2755-2756)
  on line 2759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2759-2759)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2599..2601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2599-2601)
  on lines 2603..2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2603-2604)
  on line 2607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2607-2607)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2714..2716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2714-2716)
  on lines 2718..2719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2718-2719)
  on line 2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2722-2722)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1428..1429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1428-1429)
  on line 1436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1436-1436)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1393-1393)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 554..555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:554-555)
  on lines 562..564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:562-564)
  on lines 566..567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:566-567)
  on lines 569..570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:569-570)
  on lines 577..579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:577-579)
  on lines 581..582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:581-582)
  on lines 584..585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:584-585)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 417..418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:417-418)
  on lines 420..421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:420-421)
  on lines 428..430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:428-430)
  on lines 432..433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:432-433)
  on lines 435..436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:435-436)
  on lines 443..445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:443-445)
  on lines 447..448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:447-448)
  on lines 450..451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:450-451)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 224..225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:224-225)
  on lines 227..228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:227-228)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 997..998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:997-998)
  on lines 1008..1009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1008-1009)
  on lines 1019..1020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1019-1020)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 836..837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:836-837)
  on lines 847..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:847-848)
  on lines 858..859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:858-859)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on lines 2769..2770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2769-2770)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 2580..2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2580-2581)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on lines 2732..2733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2732-2733)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 2617..2618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2617-2618)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1614-1614)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 425
  dead: 710 (494 in uncalled functions)
  total lines: 1135
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:844:11-844:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:413:7-413:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:414:9-414:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:221:7-221:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:854:11-854:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:855:13-855:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:885:7-885:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1088:7-1088:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:886:9-886:19)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:653:7-653:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2577:7-2577:18)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2294:7-2294:14)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2595:7-2595:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2032:10-2032:11)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1427:9-1427:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:478:7-478:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2614:7-2614:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1118:11-1118:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:683:11-683:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:483:11-483:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2350:7-2350:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:708:11-708:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:939:7-939:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:730:11-730:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:778:7-778:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:779:9-779:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2710:7-2710:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:547:7-547:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:551:11-551:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2729:7-2729:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:994:9-994:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2747:7-2747:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1005:11-1005:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1015:11-1015:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:1016:13-1016:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:2766:7-2766:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:197:7-197:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product14.cil.c:833:9-833:19)
[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
