./goblint --conf conf/svcomp.json --set ana.malloc.unique_address_count 1 --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_simpl1.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 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"
[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, Context, event, tmp_ndt_4, l, tmp, returnVal2, tmp_ndt_2, tmp_ndt_3, DeviceObject, Irp, lcontext, tmp, status, irp_choice, tmp_ndt_1, irp, tmp, pirp, tmp___0, devobj, 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-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:169:47-169:103)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:185:47-185:103)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:224:47-224:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:225:47-225:90)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:240:47-240:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:241:47-241:90)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:255:47-255:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:256:47-256:90)
[Warning][Deadcode] Function 'IofCallDriver' has dead code:
  on line 460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:460-460)
  on lines 476..477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:476-477)
  on line 493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:493-493)
[Warning][Deadcode] Function 'KbFilter_PnP' has dead code:
  on line 166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:166-166)
  on line 173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:173-173)
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:178-178)
  on line 220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:220-220)
  on line 236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:236-236)
  on line 251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:251-251)
[Warning][Deadcode] Function 'KeWaitForSingleObject' has dead code:
  on lines 538..539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:538-539)
  on line 543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:543-543)
  on line 554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:554-554)
[Warning][Deadcode] Function 'errorFn' has dead code:
  on line 582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:582-582)
[Warning][Deadcode] Function 'main' has dead code:
  on line 344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:344-344)
  on line 347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:347-347)
  on line 356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:356-356)
  on lines 370..371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:370-371)
  on lines 378..379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:378-379)
  on line 398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:398-398)
  on line 400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:400-400)
[Warning][Deadcode] Function 'stubMoreProcessingRequired' has dead code:
  on line 431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:431-431)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 209
  dead: 25
  total lines: 234
[Warning][Deadcode][CWE-571] condition 'status >= 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:340:8-340:19)
[Warning][Deadcode][CWE-570] condition '! __cil_tmp8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:346:9-346:21)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:171:51-171:58)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:369:7-369:18)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:176:53-176:72)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:377:9-377:20)
[Warning][Deadcode][CWE-571] condition 's != UNLOADED' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:385:11-385:24)
[Warning][Deadcode][CWE-571] condition 'status != -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:386:13-386:25)
[Warning][Deadcode][CWE-571] condition 's != IPC' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:388:17-388:25)
[Warning][Deadcode][CWE-571] condition 's == DC' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:389:19-389:26)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:397:17-397:28)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:427:7-427:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:216:51-216:58)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:232:51-232:58)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:247:51-247:58)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:475:7-475:14)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:488:11-488:21)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:529:9-529:28)
[Warning][Deadcode][CWE-571] condition 'status >= 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:323:7-323:18)
[Warning][Deadcode][CWE-570] condition 'customIrp == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:537:9-537:23)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl1.cil.c:541:11-541:20)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
