./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/diskperf.i.cil-2.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/diskperf.i.cil-2.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/ntdrivers/diskperf.i.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] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2625:7-2637:7 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3049:9-3061:9 with factor 8
[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] Enabled congruence domain.
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3231:3-3231:15)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3231:3-3231:15)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3231:3-3231:15)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3278:17-3278:56)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3278:17-3278:56)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3278:17-3278:56)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3278:17-3278:56)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3278:17-3278:56)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2424:3-2424:29)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2424:3-2424:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2424:3-2424:29)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3283:17-3283:63)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3283:17-3283:63)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3283:17-3283:63)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3283:17-3283:63)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3283:17-3283:63)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2607:11-2607:68)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2611:9-2611:35)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2611:9-2611:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2611:9-2611:35)
[Info][Unsound] Unknown value in {&frequency___0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2620:7-2620:55)
[Warning][Unknown] lval (& totalCounters)->QueryTime points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:44:170-44:173)
[Warning][Unknown] lval (& totalCounters)->QueryTime points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1566:6-1566:57)
[Warning][Unknown] lval (& totalCounters)->QueryTime points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:26:141-26:144)
[Warning][Unknown] lval (& totalCounters)->QueryTime points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1567:6-1567:57)
[Warning][Unknown] lval (& totalCounters)->QueryTime points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1568:1-1568:1)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3159:3-3159:71)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3160:3-3160:77)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3165:5-3165:107)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3166:5-3166:109)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3167:5-3167:107)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3169:5-3169:71)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3170:5-3170:73)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3171:5-3171:71)
[Info][Unsound] Unknown value in {&(alloc@sid:853)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2633:9-2633:68)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3161:3-3161:53)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3162:3-3162:55)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3163:3-3163:55)
[Info][Unsound] Unknown value in {&(alloc@sid:853)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2633:9-2633:68)
[Info][Unsound] Unknown value in {&(alloc@sid:853)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2633:9-2633:68)
[Info][Unsound] Unknown value in {&(alloc@sid:853)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2633:9-2633:68)
[Info][Unsound] Unknown value in {&(alloc@sid:853)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2633:9-2633:68)
[Info][Unsound] Unknown value in {&(alloc@sid:853)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2633:9-2633:68)
[Info][Unsound] Unknown value in {&(alloc@sid:853)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2633:9-2633:68)
[Info][Unsound] Unknown value in {&(alloc@sid:853)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2633:9-2633:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2634:9-2634:122)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2640:7-2640:62)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2642:9-2642:89)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2644:11-2644:102)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2644:11-2644:102)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2662:5-2662:31)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2662:5-2662:31)
[Info][Unsound] Unknown value in {&(alloc@sid:853)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2662:5-2662:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2662:5-2662:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2667:5-2667:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2669:5-2669:66)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2669:5-2669:66)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2669:5-2669:66)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2669:5-2669:66)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3288:17-3288:61)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3288:17-3288:61)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3288:17-3288:61)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3288:17-3288:61)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3288:17-3288:61)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2257:9-2257:58)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2257:9-2257:58)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2257:9-2257:58)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2257:9-2257:58)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2257:9-2257:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2332:3-2332:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2335:3-2335:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2335:3-2335:64)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2335:3-2335:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2335:3-2335:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2247:9-2247:56)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2247:9-2247:56)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2247:9-2247:56)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2247:9-2247:56)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2247:9-2247:56)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2287:3-2287:60)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2287:3-2287:60)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2287:3-2287:60)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2287:3-2287:60)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2287:3-2287:60)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2399:3-2399:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2399:3-2399:31)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2402:3-2402:54)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2403:3-2403:53)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2404:3-2404:67)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2404:3-2404:67)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2404:3-2404:67)
[Info][Unsound] Unknown address in {&(alloc@sid:850)[3]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2404:3-2404:67)
[Info][Unsound] Unknown value in {&(alloc@sid:850)[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2404:3-2404:67)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2404:3-2404:67)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2404:3-2404:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3857:7-3857:63)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3857:7-3857:63)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3857:7-3857:63)
[Info][Unsound] Unknown address in {&(alloc@sid:850)[3]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3857:7-3857:63)
[Info][Unsound] Unknown value in {&(alloc@sid:850)[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3857:7-3857:63)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3857:7-3857:63)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3857:7-3857:63)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2408:5-2408:55)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2408:5-2408:55)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2288:3-2288:82)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2288:3-2288:82)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2288:3-2288:82)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2288:3-2288:82)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2153:3-2153:50)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2289:3-2289:39)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2289:3-2289:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2289:3-2289:39)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2768:3-2770:50)
[Info][Unsound] Unknown value in {&ioStatus} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2768:3-2770:50)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2768:3-2770:50)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2768:3-2770:50)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2774:5-2774:58)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2774:5-2774:58)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2774:5-2774:58)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2969:3-2969:119)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2969:3-2969:119)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2969:3-2969:119)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2972:7-2972:65)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2974:5-2974:41)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2975:5-2975:47)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2976:5-2976:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2977:5-2977:79)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2978:5-2978:57)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2781:3-2781:67)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2785:5-2785:55)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2785:5-2785:55)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2816:5-2818:52)
[Info][Unsound] Unknown value in {&ioStatus} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2816:5-2818:52)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2816:5-2818:52)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2816:5-2818:52)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2823:7-2823:60)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2823:7-2823:60)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2823:7-2823:60)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2830:5-2830:69)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2834:7-2834:57)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2834:7-2834:57)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2857:7-2859:89)
[Info][Unsound] Unknown value in {&ioStatus} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2857:7-2859:89)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2857:7-2859:89)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2857:7-2859:89)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2864:9-2864:62)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2864:9-2864:62)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2864:9-2864:62)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2871:7-2871:71)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2875:9-2875:59)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2875:9-2875:59)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2887:7-2887:60)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2887:7-2887:60)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2887:7-2887:60)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2896:5-2896:107)
[Warning][Unknown] Pointer (void *)deviceExtension->PhysicalDeviceName.Buffer has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2897:5-2897:89)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2903:5-2905:64)
[Info][Unsound] Unknown value in {&ioStatus} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2903:5-2905:64)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2903:5-2905:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2903:5-2905:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2909:7-2909:60)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2909:7-2909:60)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2909:7-2909:60)
[Info][Imprecise] Invalidating expressions: deviceExtension->PhysicalDeviceNameBuffer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2794:5-2795:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2916:5-2916:69)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2920:7-2920:57)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2920:7-2920:57)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2950:3-2950:74)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2950:3-2950:74)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2950:3-2950:74)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2292:3-2292:29)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2292:3-2292:29)
[Info][Unsound] Unknown address in {&(alloc@sid:850)[3]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2292:3-2292:29)
[Info][Unsound] Unknown value in {&(alloc@sid:850)[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2292:3-2292:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2292:3-2292:29)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2252:9-2252:57)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2252:9-2252:57)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2252:9-2252:57)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2252:9-2252:57)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2252:9-2252:57)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2305:3-2305:44)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2305:3-2305:44)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2305:3-2305:44)
[Warning][Unknown] lval (& wmilibContext)->GuidCount points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1526:10-1526:28)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1526:10-1526:28)
[Warning][Unknown] lval (& wmilibContext)->GuidCount points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1527:5-1527:20)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1527:5-1527:20)
[Warning][Unknown] lval (& wmilibContext)->GuidCount points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1528:12-1528:20)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1528:12-1528:20)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2309:3-2309:60)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2309:3-2309:60)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2309:3-2309:60)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2309:3-2309:60)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2309:3-2309:60)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2375:3-2375:78)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2376:3-2376:87)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2377:3-2377:95)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2379:3-2379:25)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2397:3-2397:95)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2398:3-2398:57)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2399:3-2399:31)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2400:3-2400:25)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2401:3-2401:26)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2402:3-2402:54)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2403:3-2403:53)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2404:3-2404:67)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:136-22:139)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3846:7-3846:52)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3846:7-3846:52)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3849:9-3849:22)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3857:7-3857:63)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2274:3-2274:36)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2275:3-2275:26)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:26:141-26:144)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4022:8-4022:37)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4022:8-4022:37)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4026:11-4026:13)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2277:11-2277:24)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3858:7-3858:26)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3886:9-3886:24)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3889:9-3889:34)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3892:9-3892:26)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3923:11-3923:22)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2408:5-2408:55)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4035:7-4035:52)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4035:7-4035:52)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4067:15-4067:18)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4069:15-4069:28)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2409:5-2409:22)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2414:11-2414:18)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2314:3-2314:29)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2314:3-2314:29)
[Info][Unsound] Unknown address in {&(alloc@sid:850)[3]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2314:3-2314:29)
[Info][Unsound] Unknown value in {&(alloc@sid:850)[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2314:3-2314:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2314:3-2314:29)
[Warning][Unknown] lval (& deviceExtension)->WmilibContext points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3939:3-3939:9)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3293:17-3293:63)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3293:17-3293:63)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3293:17-3293:63)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3293:17-3293:63)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3293:17-3293:63)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2356:3-2356:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2359:3-2359:63)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2359:3-2359:63)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2359:3-2359:63)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2359:3-2359:63)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3298:17-3298:63)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3298:17-3298:63)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3298:17-3298:63)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3298:17-3298:63)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3298:17-3298:63)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2735:3-2735:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2737:3-2737:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2737:3-2737:64)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2737:3-2737:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2737:3-2737:64)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3386:11-3386:18)
[Warning][Deadcode] Function 'InterlockedIncrement' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1519:1-1521:1)
[Warning][Deadcode] Function 'InterlockedDecrement' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1522:1-1524:1)
[Warning][Deadcode] Function 'KeGetCurrentProcessorNumber' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1531:2-1537:1)
[Warning][Deadcode] Function 'WmiCompleteRequest' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2019:1-2024:1)
[Warning][Deadcode] Function 'DriverEntry' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2115:1-2146:1)
[Warning][Deadcode] Function 'DiskPerfAddDevice' is uncalled: 32 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2158:1-2228:1)
[Warning][Deadcode] Function 'DiskPerfReadWrite' is uncalled: 40 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2429:1-2517:1)
[Warning][Deadcode] Function 'DiskPerfIoCompletion' is uncalled: 29 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2518:1-2585:1)
[Warning][Deadcode] Function 'DiskPerfWmi' is uncalled: 19 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2675:1-2727:1)
[Warning][Deadcode] Function 'DiskPerfUnload' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2742:1-2748:1)
[Warning][Deadcode] Function 'DiskperfQueryWmiRegInfo' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2987:1-3012:1)
[Warning][Deadcode] Function 'DiskperfQueryWmiDataBlock' is uncalled: 38 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3013:1-3099:1)
[Warning][Deadcode] Function 'DiskperfWmiFunctionControl' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3100:1-3153:1)
[Warning][Deadcode] Function 'ExAcquireFastMutex' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3391:1-3397:1)
[Warning][Deadcode] Function 'ExReleaseFastMutex' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3399:1-3405:1)
[Warning][Deadcode] Function 'ExFreePool' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3423:1-3429:1)
[Warning][Deadcode] Function 'ExfInterlockedInsertHeadList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3433:1-3441:1)
[Warning][Deadcode] Function 'ExfInterlockedInsertTailList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3445:1-3453:1)
[Warning][Deadcode] Function 'ExfInterlockedRemoveHeadList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3456:1-3463:1)
[Warning][Deadcode] Function 'IoAllocateMdl' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3467:1-3492:1)
[Warning][Deadcode] Function 'IoAttachDeviceToDeviceStack' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3495:1-3515:1)
[Warning][Deadcode] Function 'IoBuildAsynchronousFsdRequest' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3522:1-3549:1)
[Warning][Deadcode] Function 'IoCreateDevice' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3593:1-3620:1)
[Warning][Deadcode] Function 'IoCreateSymbolicLink' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3623:1-3643:1)
[Warning][Deadcode] Function 'IoDeleteDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3645:1-3651:1)
[Warning][Deadcode] Function 'IoDeleteSymbolicLink' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3653:1-3673:1)
[Warning][Deadcode] Function 'IoDetachDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3675:1-3681:1)
[Warning][Deadcode] Function 'IoFreeIrp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3683:1-3689:1)
[Warning][Deadcode] Function 'IoFreeMdl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3691:1-3697:1)
[Warning][Deadcode] Function 'IoGetConfigurationInformation' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3699:1-3708:1)
[Warning][Deadcode] Function 'IoQueryDeviceDescription' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3727:1-3760:1)
[Warning][Deadcode] Function 'IoRegisterDeviceInterface' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3765:1-3788:1)
[Warning][Deadcode] Function 'IoReleaseCancelSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3790:1-3796:1)
[Warning][Deadcode] Function 'IoSetDeviceInterfaceState' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3799:1-3819:1)
[Warning][Deadcode] Function 'IoSetHardErrorOrVerifyDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3821:1-3827:1)
[Warning][Deadcode] Function 'KeAcquireSpinLockRaiseToDpc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3943:1-3949:1)
[Warning][Deadcode] Function 'KeDelayExecutionThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3953:1-3973:1)
[Warning][Deadcode] Function 'KeInitializeEvent' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3976:1-3982:1)
[Warning][Deadcode] Function 'KeInitializeSemaphore' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3985:1-3991:1)
[Warning][Deadcode] Function 'KeInitializeSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3993:1-3999:1)
[Warning][Deadcode] Function 'KeReleaseSemaphore' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4002:1-4009:1)
[Warning][Deadcode] Function 'KfReleaseSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4012:1-4018:1)
[Warning][Deadcode] Function 'MmAllocateContiguousMemory' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4079:1-4105:1)
[Warning][Deadcode] Function 'MmFreeContiguousMemory' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4107:1-4113:1)
[Warning][Deadcode] Function 'MmMapLockedPagesSpecifyCache' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4120:1-4128:1)
[Warning][Deadcode] Function 'MmPageEntireDriver' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4130:1-4136:1)
[Warning][Deadcode] Function 'MmResetDriverPaging' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4138:1-4144:1)
[Warning][Deadcode] Function 'MmUnlockPages' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4146:1-4152:1)
[Warning][Deadcode] Function 'ObReferenceObjectByHandle' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4159:1-4180:1)
[Warning][Deadcode] Function 'ObfDereferenceObject' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4182:1-4188:1)
[Warning][Deadcode] Function 'PoStartNextPowerIrp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4277:1-4283:1)
[Warning][Deadcode] Function 'PsCreateSystemThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4291:1-4313:1)
[Warning][Deadcode] Function 'PsTerminateSystemThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4315:1-4335:1)
[Warning][Deadcode] Function 'RtlAnsiStringToUnicodeString' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4339:1-4361:1)
[Warning][Deadcode] Function 'RtlCompareMemory' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4365:1-4372:1)
[Warning][Deadcode] Function 'RtlCopyUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4375:1-4382:1)
[Warning][Deadcode] Function 'RtlDeleteRegistryValue' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4386:1-4407:1)
[Warning][Deadcode] Function 'RtlFreeUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4409:1-4415:1)
[Warning][Deadcode] Function 'RtlInitString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4418:1-4424:1)
[Warning][Deadcode] Function 'RtlInitUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4427:1-4434:1)
[Warning][Deadcode] Function 'RtlQueryRegistryValues' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4440:1-4462:1)
[Warning][Deadcode] Function 'ZwClose' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4464:1-4484:1)
[Warning][Deadcode] Function 'WmiSystemControl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4485:1-4492:1)
[Warning][Deadcode] Function 'DiskPerfDispatchPnp' has dead code:
  on line 2244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2244-2244)
[Warning][Deadcode] Function 'DiskPerfDispatchPower' has dead code:
  on line 2352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2352-2352)
[Warning][Deadcode] Function 'DiskPerfForwardIrpSynchronous' has dead code:
  on line 2383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2383-2383)
  on line 2388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2388-2388)
[Warning][Deadcode] Function 'DiskPerfRegisterDevice' has dead code:
  on line 2808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2808-2808)
  on line 2810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2810-2810)
  on line 2849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2849-2849)
  on line 2851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2851-2851)
  on line 2942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2942-2942)
  on line 2944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2944-2944)
  on line 2954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2954-2954)
[Warning][Deadcode] Function 'DiskPerfSendToNextDriver' has dead code:
  on line 2328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2328-2328)
[Warning][Deadcode] Function 'IoBuildDeviceIoControlRequest' has dead code:
  on line 3573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3573-3573)
[Warning][Deadcode] Function 'IofCallDriver' has dead code:
  on lines 3862..3863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3862-3863)
  on line 3884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3884-3884)
  on line 3918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3918-3918)
[Warning][Deadcode] Function 'KeWaitForSingleObject' has dead code:
  on line 4053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4053-4053)
  on line 4065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4065-4065)
[Warning][Deadcode] Function 'PoCallDriver' has dead code:
  on line 4201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4201-4201)
  on lines 4203..4204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4203-4204)
  on line 4207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4207-4207)
  on lines 4209..4210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4209-4210)
  on line 4216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4216-4216)
  on line 4218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4218-4218)
  on line 4234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4234-4234)
  on lines 4251..4252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4251-4252)
  on lines 4255..4257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4255-4257)
  on lines 4259..4260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4259-4260)
  on line 4268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4268-4268)
[Warning][Deadcode] Function 'errorFn' has dead code:
  on line 2033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2033-2033)
[Warning][Deadcode] Function 'main' has dead code:
  on line 3254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3254-3254)
  on line 3275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3275-3275)
  on lines 3323..3324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3323-3324)
  on lines 3331..3332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3331-3332)
  on line 3348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3348-3348)
  on line 3359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3359-3359)
  on line 3361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3361-3361)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 424
  dead: 427 (381 in uncalled functions)
  total lines: 851
[Warning][Deadcode][CWE-571] condition 'routine == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3855:9-3855:21)
[Warning][Deadcode][CWE-571] condition '(long )compRetStatus == -1073741802L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3866:9-3866:45)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2348:7-2348:14)
[Warning][Deadcode][CWE-570] condition 'compRegistered' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4200:7-4200:21)
[Warning][Deadcode][CWE-571] condition '(int )volumeNumber.VolumeManagerName[0] == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2929:11-2929:55)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2381:7-2381:14)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2386:9-2386:28)
[Warning][Deadcode][CWE-570] condition '! (status >= 0L)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3253:9-3253:25)
[Warning][Deadcode][CWE-570] condition '! (status >= 0L)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2952:7-2952:23)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3913:11-3913:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2625:14-2625:15)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4250:7-4250:14)
[Warning][Deadcode][CWE-570] condition 's == MPR1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4254:9-4254:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2625:14-2625:15)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4263:11-4263:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2625:14-2625:15)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3322:7-3322:18)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3330:9-3330:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2625:14-2625:15)
[Warning][Deadcode][CWE-570] condition 's != DC' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3346:19-3346:26)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2625:14-2625:15)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4039:9-4039:28)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:3358:17-3358:28)
[Warning][Deadcode][CWE-570] condition '! output' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2806:9-2806:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2625:14-2625:15)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:4051:11-4051:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2625:14-2625:15)
[Warning][Deadcode][CWE-570] condition '! output' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2847:11-2847:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2625:14-2625:15)
[Warning][Deadcode][CWE-571] condition 'isFixed == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1698:9-1698:21)
[Warning][Deadcode][CWE-571] condition '(unsigned long )PerformanceFrequency != (unsigned long )((void *)0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:1703:9-1703:45)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2625:14-2625:15)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/diskperf.i.cil-2.c:2324:7-2324:14)
[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
