./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-2.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] 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, i, j, i___0, j___0, k, size, r, 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-2.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-2.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-2.c:173:47-173:103)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:189:47-189:103)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:229:47-229:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:230:47-230:90)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:245:47-245:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:246:47-246:90)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:260:47-260:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:261:47-261:90)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.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-2.c:513-513)
  on lines 529..530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:529-530)
  on line 546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.c:678-678)
[Warning][Deadcode] Function 'KbFilter_PnP' has dead code:
  on line 170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:170-170)
  on line 177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:177-177)
  on line 182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:182-182)
  on line 225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:225-225)
  on line 241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:241-241)
  on line 256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:256-256)
[Warning][Deadcode] Function 'KbFilter_Power' has dead code:
  on line 713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:713-713)
  on line 734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.c:591-592)
  on line 596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:596-596)
  on line 607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.c:756-756)
  on lines 759..760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:759-760)
  on line 762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:762-762)
  on line 778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:778-778)
  on lines 794..795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:794-795)
  on lines 799..802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:799-802)
  on lines 804..805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:804-805)
  on line 814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.c:1014-1014)
[Warning][Deadcode] Function 'main' has dead code:
  on line 346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:346-346)
  on line 375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:375-375)
  on lines 413..414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:413-414)
  on lines 421..422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:421-422)
  on line 441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:441-441)
  on line 443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:443-443)
[Warning][Deadcode] Function 'stubMoreProcessingRequired' has dead code:
  on line 475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:475-475)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 332
  dead: 41
  total lines: 373
[Warning][Deadcode][CWE-570] condition 'status < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:345:9-345:19)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.c:590:9-590:23)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:175:51-175:58)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:594:11-594:20)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:180:53-180:72)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:793:7-793:14)
[Warning][Deadcode][CWE-570] condition 's == MPR1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.c:809:11-809:21)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:412:7-412:18)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.c:420:9-420:20)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:221:51-221:58)
[Warning][Deadcode][CWE-571] condition 's != UNLOADED' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:428:11-428:24)
[Warning][Deadcode][CWE-571] condition 'status != -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:429:13-429:25)
[Warning][Deadcode][CWE-571] condition 's != IPC' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:431:17-431:25)
[Warning][Deadcode][CWE-571] condition 's == DC' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:432:19-432:26)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:440:17-440:28)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c:237:51-237:58)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.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-2.c:252:51-252:58)
[Warning][Deadcode][CWE-571] condition '__cil_tmp7 == -1073741802LL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.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-2.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-2.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-2.c:328:7-328:18)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.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-2.c:754:7-754:21)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
