./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_spec4_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_spec4_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_spec4_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_spec4_productSimulator.cil.c:3158:3-3179:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3215:3-3240:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3300:5-3320: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_spec4_productSimulator.cil.c:338:1-352:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:735:1-749:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:968:1-982:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:986:1-1011:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1012:1-1031:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1036:1-1059:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1060:1-1079:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1127:1-1151:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1161:1-1229:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1230:1-1298:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2138:1-2152:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2174:1-2189:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2266:1-2286:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2287:1-2302:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2305:1-2325:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2326:1-2341:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2676:1-2686:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2765:1-2776:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2777:1-2788:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3056:1-3064:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3087:1-3132:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3133:1-3188:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3189:1-3248:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3251:1-3353:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3354:1-3399:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3400:1-3445:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:944-944)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1652-1652)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 3077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3077-3077)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1876-1876)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1377..1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1377-1379)
  on lines 1381..1382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1381-1382)
  on lines 1387..1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1387-1390)
  on lines 1392..1394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1392-1394)
  on lines 1396..1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1396-1398)
  on lines 1400..1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1400-1401)
  on lines 1406..1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1406-1409)
  on lines 1411..1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1411-1413)
  on lines 1415..1417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1415-1417)
  on lines 1419..1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1419-1420)
  on lines 1425..1426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1425-1426)
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1430-1430)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1104-1104)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1513-1513)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1948-1948)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1995-1995)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1780..1782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1780-1782)
  on lines 1784..1785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1784-1785)
  on lines 1789..1792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1789-1792)
  on lines 1794..1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1794-1796)
  on lines 1798..1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1798-1799)
  on lines 1803..1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1803-1806)
  on lines 1808..1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1808-1810)
  on lines 1812..1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1812-1813)
  on lines 1817..1818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1817-1818)
  on line 1822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1822-1822)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1602..1603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1602-1603)
  on line 1607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1607-1607)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1673..1675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1673-1675)
  on lines 1677..1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1677-1678)
  on lines 1682..1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1682-1685)
  on lines 1687..1689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1687-1689)
  on lines 1691..1692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1691-1692)
  on lines 1696..1699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1696-1699)
  on lines 1701..1703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1701-1703)
  on lines 1705..1706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1705-1706)
  on lines 1710..1711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1710-1711)
  on line 1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1715-1715)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1560-1560)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2390..2391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2390-2391)
  on line 2397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2397-2397)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2201..2202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2201-2202)
  on line 2208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2208-2208)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2164..2165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2164-2165)
  on line 2171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2171-2171)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2464..2465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2464-2465)
  on line 2471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2471-2471)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2238..2239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2238-2239)
  on line 2245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2245-2245)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:788-788)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:797-797)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2353..2354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2353-2354)
  on line 2360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2360-2360)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 814..815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:814-815)
  on line 822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:822-822)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 3053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3053-3053)
[Warning][Deadcode] Function 'isReadable__before__Encrypt' has dead code:
  on line 3015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3015-3015)
[Warning][Deadcode] Function 'isReadable__role__Encrypt' has dead code:
  on line 3035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:3035-3035)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2427..2428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2427-2428)
  on line 2434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2434-2434)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2501..2502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2501-2502)
  on line 2508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2508-2508)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:779-779)
[Warning][Deadcode] Function 'outgoing' has dead code:
  on line 550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:550-550)
  on line 552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:552-552)
[Warning][Deadcode] Function 'printMail__before__Verify' has dead code:
  on line 2972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2972-2972)
  on line 2974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2974-2974)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 2030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2030-2030)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1444..1445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1444-1445)
  on lines 1452..1454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1452-1454)
  on lines 1456..1457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1456-1457)
  on lines 1459..1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1459-1460)
  on lines 1467..1469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1467-1469)
  on lines 1471..1472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1471-1472)
  on lines 1474..1475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1474-1475)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1307..1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1307-1308)
  on lines 1310..1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1310-1311)
  on lines 1318..1320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1318-1320)
  on lines 1322..1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1322-1323)
  on lines 1325..1326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1325-1326)
  on lines 1333..1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1333-1335)
  on lines 1337..1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1337-1338)
  on lines 1340..1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1340-1341)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1114..1115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1114-1115)
  on lines 1117..1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1117-1118)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1521-1521)
  on lines 1526..1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1526-1527)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1956-1956)
  on lines 1961..1962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1961-1962)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1887..1888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1887-1888)
  on lines 1898..1899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1898-1899)
  on lines 1909..1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1909-1910)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1726..1727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1726-1727)
  on lines 1737..1738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1737-1738)
  on lines 1748..1749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1748-1749)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2408-2408)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2219-2219)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2371-2371)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2519-2519)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2445-2445)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2482-2482)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2256-2256)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2104-2104)
  on line 2125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2125-2125)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 813
  dead: 550 (351 in uncalled functions)
  total lines: 1363
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1520:7-1520:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1958:9-1958:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1523:9-1523:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2463:9-2463:20)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Sign' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:543:7-543:30)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2481:9-2481:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2500:9-2500:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2008:11-2008:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1573:11-1573:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2518:9-2518:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1598:11-1598:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1620:11-1620:22)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Sign' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2079:19-2079:44)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Verify' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2084:23-2084:50)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Sign' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2087:25-2087:48)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Sign' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2089:27-2089:52)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:109:10-109:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1668:7-1668:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1669:9-1669:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2163:9-2163:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1723:9-1723:19)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:813:9-813:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1734:11-1734:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2200:9-2200:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1303:7-1303:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1304:9-1304:19)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1744:11-1744:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1745:13-1745:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2218:9-2218:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1775:7-1775:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1776:9-1776:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2237:9-2237:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2255:9-2255:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1368:7-1368:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1373:11-1373:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2352:9-2352:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1437:7-1437:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1441:11-1441:21)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Sign' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2965:7-2965:30)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2370:9-2370:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1884:9-1884:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2389:9-2389:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1895:11-1895:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1905:11-1905:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1906:13-1906:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2407:9-2407:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2426:9-2426:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:2444:9-2444:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1955:7-1955:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_productSimulator.cil.c:1111:7-1111:18)
[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
