./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.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 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] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] s, NP, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, irpStack__Parameters__DeviceIoControl__IoControlCode, irpStack__Parameters__DeviceIoControl__InputBufferLength, status, devExt__UpperConnectData__ClassService, sizeof__CONNECT_DATA, sizeof__INTERNAL_I8042_HOOK_KEYBOARD, __cil_tmp20, __cil_tmp24, __cil_tmp7, __cil_tmp8, tmp_ndt_9, tmp_ndt_10, returnVal, DeviceObject, Irp, lcontext, irpStack__MinorFunction, powerType, Irp, tmp, powerState__DeviceState, tmp___0, Irp__CurrentLocation, tmp___1, Irp__Tail__Overlay__CurrentStackLocation, Irp, tmp, Irp__CurrentLocation, tmp___0, DeviceObject__DeviceExtension__TopOfStack, tmp___1, tmp___2, irpStack__MajorFunction, devExt__UpperConnectData__ClassService, status, DeviceObject, Irp, tmp, tmp___0, tmp___1, Context, event, tmp_ndt_8, l, tmp, returnVal2, __cil_tmp7, tmp_ndt_6, tmp_ndt_7, DeviceObject, Irp, lcontext, tmp, status, irp_choice, tmp_ndt_1, tmp_ndt_2, tmp_ndt_3, tmp_ndt_4, tmp_ndt_5, pirp, irpStack__MinorFunction, status, Irp__Tail__Overlay__CurrentStackLocation, __cil_tmp23, Irp, devExt__TopOfStack, Irp__CurrentLocation, event
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:682:3-682:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:683:3-683:46)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:175:47-175:103)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:191:47-191:103)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:231:47-231:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:232:47-232:90)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:247:47-247:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:248:47-248:90)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:262:47-262:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:263:47-263:90)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:738:3-738:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:739:3-739:46)
[Warning][Deadcode] Function 'IofCallDriver' has dead code:
  on line 513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:513-513)
  on lines 529..530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:529-530)
  on line 546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:546-546)
[Warning][Deadcode] Function 'KbFilter_DispatchPassThrough' has dead code:
  on line 678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:678-678)
[Warning][Deadcode] Function 'KbFilter_PnP' has dead code:
  on line 172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:172-172)
  on line 179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:179-179)
  on line 184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:184-184)
  on line 227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:227-227)
  on line 243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:243-243)
  on line 258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:258-258)
[Warning][Deadcode] Function 'KbFilter_Power' has dead code:
  on line 713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:713-713)
  on line 734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:734-734)
[Warning][Deadcode] Function 'KeWaitForSingleObject' has dead code:
  on lines 591..592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:591-592)
  on line 596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:596-596)
  on line 607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:607-607)
[Warning][Deadcode] Function 'PoCallDriver' has dead code:
  on line 756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:756-756)
  on lines 759..760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:759-760)
  on line 762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:762-762)
  on line 778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:778-778)
  on lines 794..795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:794-795)
  on lines 799..802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:799-802)
  on lines 804..805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:804-805)
  on line 814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:814-814)
[Warning][Deadcode] Function 'errorFn' has dead code:
  on line 1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:1014-1014)
[Warning][Deadcode] Function 'main' has dead code:
  on line 348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:348-348)
  on line 377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:377-377)
  on lines 415..416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:415-416)
  on lines 423..424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:423-424)
  on line 443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:443-443)
  on line 445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:445-445)
[Warning][Deadcode] Function 'stubMoreProcessingRequired' has dead code:
  on line 475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:475-475)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 331
  dead: 41
  total lines: 372
[Warning][Deadcode][CWE-570] condition 'status < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:347:9-347:19)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:582:9-582:28)
[Warning][Deadcode][CWE-570] condition 'customIrp == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:590:9-590:23)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:594:11-594:20)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:177:51-177:58)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:793:7-793:14)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:182:53-182:72)
[Warning][Deadcode][CWE-570] condition 's == MPR1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:797:9-797:18)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:809:11-809:21)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:644:11-644:12)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:414:7-414:18)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:422:9-422:20)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:223:51-223:58)
[Warning][Deadcode][CWE-571] condition 's != UNLOADED' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:430:11-430:24)
[Warning][Deadcode][CWE-571] condition 'status != -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:431:13-431:25)
[Warning][Deadcode][CWE-571] condition 's != IPC' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:433:17-433:25)
[Warning][Deadcode][CWE-571] condition 's == DC' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:434:19-434:26)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:442:17-442:28)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:239:51-239:58)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:674:7-674:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:471:7-471:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:254:51-254:58)
[Warning][Deadcode][CWE-571] condition '__cil_tmp7 == -1073741802LL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:495:9-495:34)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:934:25-934:26)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:528:7-528:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:730:7-730:14)
[Warning][Deadcode][CWE-571] condition 'status >= 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:330:7-330:18)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:541:11-541:21)
[Warning][Deadcode][CWE-570] condition 'compRegistered' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-1.c:754:7-754:21)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
