Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Benchmark: ntdrivers/diskperf_true-unreach-call.i.cil.c #5

Closed
marek-trtik opened this issue Nov 10, 2017 · 11 comments
Closed

Benchmark: ntdrivers/diskperf_true-unreach-call.i.cil.c #5

marek-trtik opened this issue Nov 10, 2017 · 11 comments
Assignees
@marek-trtik
Labels
bug

Comments

@marek-trtik
Copy link
Owner

marek-trtik commented Nov 10, 2017 •
edited
Loading

Current false(unreach-call); last year ERROR(42); should be true.
@marek-trtik marek-trtik self-assigned this Nov 10, 2017
@marek-trtik
Copy link
Owner Author

Log from last year:

./cbmc --graphml-witness witness.graphml --32 --propertyfile ../../sv-benchmarks/c/ReachSafety.prp ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c


--------------------------------------------------------------------------------


Unwind: 40
CBMC version 5.6 64-bit x86_64 linux
Parsing ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Converting
Type-checking diskperf_true-unreach-call.i.cil
Generating GOTO Program
Adding CPROVER library (x86_64)
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop DiskPerfDeviceControl.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.0 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
Not unwinding loop DiskPerfDeviceControl.0 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
**** WARNING: no body for function KeQueryPerformanceCounter
**** WARNING: no body for function KeQuerySystemTime
Unwinding loop DiskPerfDeviceControl.1 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.1 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Not unwinding loop DiskPerfDeviceControl.1 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfDeviceControl.2 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
**** WARNING: no body for function IoAllocateErrorLogEntry
Unwinding loop DiskPerfLogError.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Not unwinding loop DiskPerfLogError.0 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
**** WARNING: no body for function IoWriteErrorLogEntry
**** WARNING: no body for function swprintf
Unwinding loop DiskPerfRegisterDevice.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2743 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfLogError.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Not unwinding loop DiskPerfLogError.0 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Not unwinding loop DiskPerfLogError.0 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Not unwinding loop DiskPerfLogError.0 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Not unwinding loop DiskPerfLogError.0 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Not unwinding loop DiskPerfLogError.0 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.1 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Not unwinding loop DiskPerfRegisterDevice.1 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2843 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.2 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2847 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfLogError.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Not unwinding loop DiskPerfLogError.0 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.3 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2878 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
Unwinding loop DiskPerfRegisterDevice.4 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2888 function DiskPerfRegisterDevice thread 0
**** WARNING: no body for function IoWMIRegistrationControl
Unwinding loop DiskPerfLogError.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 33 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 34 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 35 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 36 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 37 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 38 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Unwinding loop DiskPerfLogError.0 iteration 39 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
Not unwinding loop DiskPerfLogError.0 iteration 40 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2923 function DiskPerfLogError thread 0
**** WARNING: no body for function InterlockedExchange
Unwinding loop DiskPerfRemoveDevice.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 29 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 30 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 31 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfRemoveDevice.0 iteration 32 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2254 function DiskPerfRemoveDevice thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 1 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 2 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 3 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 4 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 5 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 6 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 7 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 8 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 9 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 10 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 11 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 12 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 13 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 14 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 15 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 16 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 17 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 18 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 19 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 20 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 21 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 22 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 23 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 24 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 25 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 26 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 27 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
Unwinding loop DiskPerfForwardIrpSynchronous.0 iteration 28 (40 max) file ../../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2324 function DiskPerfForwardIrpSynchronous thread 0
size of program expression: 22049 steps
simple slicing removed 1197 assignments
Generated 15 VCC(s), 15 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with Glucose Syrup with simplifier
1351977 variables, 6269281 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 1.768s
VERIFICATION SUCCESSFUL
EC=42
UNKNOWN

@marek-trtik
Copy link
Owner Author

Log from current cbmc:

./xtest --graphml-witness witness.graphml --32 --propertyfile ../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c


--------------------------------------------------------------------------------


./xtest-binary --graphml-witness /tmp/BenchExec_run_mcc4mi2l/tmp/xtest-log.sKvOED.witness --unwind 2 --stop-on-fail --32 --function main ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c
Unwind: 2
CBMC version 5.8 64-bit x86_64 linux
Parsing ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Converting
Type-checking diskperf_true-unreach-call.i.cil
Generating GOTO Program
Adding CPROVER library (x86_64)
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
**** WARNING: no body for function KeQueryPerformanceCounter
**** WARNING: no body for function KeQuerySystemTime
Unwinding loop DiskPerfDeviceControl.0 iteration 1 (2 max) file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
Not unwinding loop DiskPerfDeviceControl.0 iteration 2 (2 max) file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2571 function DiskPerfDeviceControl thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
**** WARNING: no body for function IoAllocateErrorLogEntry
**** WARNING: no body for function IoWriteErrorLogEntry
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
**** WARNING: no body for function swprintf
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
**** WARNING: no body for function IoWMIRegistrationControl
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
**** WARNING: no body for function InterlockedExchange
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 1976 function errorFn thread 0
size of program expression: 4492 steps
simple slicing removed 129 assignments
Generated 29 VCC(s), 29 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with Glucose Syrup with simplifier
158249 variables, 473002 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.781s
Building error trace
Counterexample:

State 202 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3160 function main thread 0
----------------------------------------------------
  d={ .Type=0, .Size=0, .DeviceObject=((PDEVICE_OBJECT)NULL), .Flags=0ul,
    .DriverStart=NULL, .DriverSize=0ul, .DriverSection=NULL,
    .DriverExtension=((PDRIVER_EXTENSION)NULL), .DriverName={ .Length=0, .MaximumLength=0, .Buffer=((PWSTR)NULL) },
    .HardwareDatabase=((PUNICODE_STRING)NULL),
    .FastIoDispatch=((PFAST_IO_DISPATCH)NULL),
    .DriverInit=((signed int (*)(struct _DRIVER_OBJECT *, PUNICODE_STRING))NULL),
    .DriverStartIo=((const void (*)(PDEVICE_OBJECT, PIRP))NULL),
    .DriverUnload=((const void (*)(struct _DRIVER_OBJECT *))NULL),
    .MajorFunction={ ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL), ((PDRIVER_DISPATCH)NULL) } } ({ 0000000000000000, 0000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, { 0000000000000000, 0000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, { 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 } })

State 203 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3161 function main thread 0
----------------------------------------------------
  status=0 (00000000000000000000000000000000)

State 204 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3161 function main thread 0
----------------------------------------------------
  status=1 (00000000000000000000000000000001)

State 205 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3162 function main thread 0
----------------------------------------------------
  we_should_unload=0 (00000000000000000000000000000000)

State 206 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3162 function main thread 0
----------------------------------------------------
  we_should_unload=-2147483648 (10000000000000000000000000000000)

State 207 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3163 function main thread 0
----------------------------------------------------
  irp={ .Type=0, .Size=0, .MdlAddress=((PMDL)NULL), .Flags=0ul,
    .AssociatedIrp={ .MasterIrp=((PIRP)NULL) + -7733378 }, .ThreadListEntry={ .Flink=((struct _LIST_ENTRY *)NULL), .Blink=((struct _LIST_ENTRY *)NULL) },
    .IoStatus={ .__annonCompField4={ .Status=0 }, .Information=0ul },
    .RequestorMode=0,
    .PendingReturned=0, .StackCount=0,
    .CurrentLocation=0, .Cancel=0, .CancelIrql=0,
    .ApcEnvironment=0, .AllocationFlags=0, .UserIosb=((PIO_STATUS_BLOCK)NULL),
    .UserEvent=((PKEVENT)NULL), .Overlay={ .AsynchronousParameters={ .UserApcRoutine=((const void (*)(const void *, PIO_STATUS_BLOCK, unsigned long int))NULL), .UserApcContext=NULL } },
    .CancelRoutine=((const void (*)(PDEVICE_OBJECT, PIRP))NULL),
    .UserBuffer=NULL,
    .Tail={ .Overlay={ .__annonCompField15={ .DeviceQueueEntry={ .DeviceListEntry={ .Flink=((struct _LIST_ENTRY *)NULL), .Blink=((struct _LIST_ENTRY *)NULL) }, .SortKey=0ul,
    .Inserted=0, .$pad0=0 } }, .Thread=((PETHREAD)NULL),
    .AuxiliaryBuffer=((PCCHAR)NULL), .__annonCompField17={ .ListEntry={ .Flink=((struct _LIST_ENTRY *)NULL), .Blink=((struct _LIST_ENTRY *)NULL) }, .__annonCompField16={ .CurrentStackLocation=((struct _IO_STACK_LOCATION *)NULL) + 40 } },
    .OriginalFileObject=((PFILE_OBJECT)NULL) } } } ({ 0000000000000000, 0000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000100010011111111101111110, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000000000000000000000000000, 00000000000000000000000000000000, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, 00000000000000000000000000000000, { { { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, 00000000, 000000000000000000000000 }, 00000000000000000000000000000000, 00000000000000000000000000000000, { { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000101000 }, 00000000000000000000000000000000 } })

State 208 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3164 function main thread 0
----------------------------------------------------
  __BLAST_NONDET___0=0 (00000000000000000000000000000000)

State 209 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3164 function main thread 0
----------------------------------------------------
  __BLAST_NONDET___0=2 (00000000000000000000000000000010)

State 210 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3165 function main thread 0
----------------------------------------------------
  irp_choice=0 (00000000000000000000000000000000)

State 211 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3165 function main thread 0
----------------------------------------------------
  irp_choice=1073741824 (01000000000000000000000000000000)

State 212 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3166 function main thread 0
----------------------------------------------------
  devobj={ .Type=0, .Size=0, .ReferenceCount=0, .DriverObject=((struct _DRIVER_OBJECT *)NULL), .NextDevice=((PDEVICE_OBJECT)NULL),
    .AttachedDevice=((PDEVICE_OBJECT)NULL), .CurrentIrp=((PIRP)NULL),
    .Timer=((PIO_TIMER)NULL), .Flags=0ul,
    .Characteristics=0ul, .Vpb=((PVPB)NULL), .DeviceExtension=NULL + -7733311,
    .DeviceType=0ul, .StackSize=0,
    .$pad0=0, .Queue={ .ListEntry={ .Flink=((struct _LIST_ENTRY *)NULL), .Blink=((struct _LIST_ENTRY *)NULL) } }, .AlignmentRequirement=0ul,
    .DeviceQueue={ .Type=0, .Size=0, .DeviceListHead={ .Flink=((struct _LIST_ENTRY *)NULL), .Blink=((struct _LIST_ENTRY *)NULL) }, .Lock=0ul,
    .Busy=0, .$pad0=0 }, .Dpc={ .Type=0, .Number=0, .Importance=0, .DpcListEntry={ .Flink=((struct _LIST_ENTRY *)NULL), .Blink=((struct _LIST_ENTRY *)NULL) }, .DeferredRoutine=((const void (*)(PKDPC, const void *, const void *, const void *))NULL),
    .DeferredContext=NULL,
    .SystemArgument1=NULL, .SystemArgument2=NULL,
    .Lock=((PULONG_PTR)NULL) },
    .ActiveThreadCount=0ul,
    .SecurityDescriptor=NULL, .DeviceLock={ .Header={ .Type=0, .Absolute=0, .Size=0, .Inserted=0, .SignalState=0,
    .WaitListHead={ .Flink=((struct _LIST_ENTRY *)NULL), .Blink=((struct _LIST_ENTRY *)NULL) } } },
    .SectorSize=0,
    .Spare1=0, .DeviceObjectExtension=((struct _DEVOBJ_EXTENSION *)NULL), .Reserved=NULL } ({ 0000000000000000, 0000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000100010011111111111000001, 00000000000000000000000000000000, 00000000, 000000000000000000000000, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, { 0000000000000000, 0000000000000000, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, 00000000, 000000000000000000000000 }, { 0000000000000000, 00000000, 00000000, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, 00000000000000000000000000000000, { { 00000000, 00000000, 00000000, 00000000, 00000000000000000000000000000000, { 00000000000000000000000000000000, 00000000000000000000000000000000 } } }, 0000000000000000, 0000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 })

State 215 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3167 function main thread 0
----------------------------------------------------
  KeNumberProcessors=((PCCHAR)NULL) (00000000000000000000000000000000)

State 216 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3171 function main thread 0
----------------------------------------------------
  pirp=&irp!0@1.Type (00000011000000000000000000000000)

State 219 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2000 function _BLAST_init thread 0
----------------------------------------------------
  UNLOADED=0 (00000000000000000000000000000000)

State 220 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2001 function _BLAST_init thread 0
----------------------------------------------------
  NP=1 (00000000000000000000000000000001)

State 221 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2002 function _BLAST_init thread 0
----------------------------------------------------
  DC=2 (00000000000000000000000000000010)

State 222 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2003 function _BLAST_init thread 0
----------------------------------------------------
  SKIP1=3 (00000000000000000000000000000011)

State 223 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2004 function _BLAST_init thread 0
----------------------------------------------------
  SKIP2=4 (00000000000000000000000000000100)

State 224 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2005 function _BLAST_init thread 0
----------------------------------------------------
  MPR1=5 (00000000000000000000000000000101)

State 225 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2006 function _BLAST_init thread 0
----------------------------------------------------
  MPR3=6 (00000000000000000000000000000110)

State 226 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2007 function _BLAST_init thread 0
----------------------------------------------------
  IPC=7 (00000000000000000000000000000111)

State 227 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2008 function _BLAST_init thread 0
----------------------------------------------------
  s=0 (00000000000000000000000000000000)

State 228 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2009 function _BLAST_init thread 0
----------------------------------------------------
  pended=0 (00000000000000000000000000000000)

State 229 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2010 function _BLAST_init thread 0
----------------------------------------------------
  compFptr=((signed int (*)(PDEVICE_OBJECT, PIRP, const void *))NULL) (00000000000000000000000000000000)

State 230 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2011 function _BLAST_init thread 0
----------------------------------------------------
  compRegistered=0 (00000000000000000000000000000000)

State 231 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2012 function _BLAST_init thread 0
----------------------------------------------------
  lowerDriverReturn=0 (00000000000000000000000000000000)

State 232 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2013 function _BLAST_init thread 0
----------------------------------------------------
  setEventCalled=0 (00000000000000000000000000000000)

State 233 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2014 function _BLAST_init thread 0
----------------------------------------------------
  customIrp=0 (00000000000000000000000000000000)

State 236 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3175 function main thread 0
----------------------------------------------------
  s=1 (00000000000000000000000000000001)

State 237 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3176 function main thread 0
----------------------------------------------------
  customIrp=0 (00000000000000000000000000000000)

State 238 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3177 function main thread 0
----------------------------------------------------
  setEventCalled=0 (00000000000000000000000000000000)

State 239 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3178 function main thread 0
----------------------------------------------------
  lowerDriverReturn=0 (00000000000000000000000000000000)

State 240 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3179 function main thread 0
----------------------------------------------------
  compRegistered=0 (00000000000000000000000000000000)

State 241 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3180 function main thread 0
----------------------------------------------------
  compFptr=((signed int (*)(PDEVICE_OBJECT, PIRP, const void *))NULL) (00000000000000000000000000000000)

State 242 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3181 function main thread 0
----------------------------------------------------
  pended=0 (00000000000000000000000000000000)

State 243 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3182 function main thread 0
----------------------------------------------------
  irp={ .Type=0, .Size=0, .MdlAddress=((PMDL)NULL), .Flags=0ul,
    .AssociatedIrp={ .MasterIrp=((PIRP)NULL) + -7733378 }, .ThreadListEntry={ .Flink=((struct _LIST_ENTRY *)NULL), .Blink=((struct _LIST_ENTRY *)NULL) },
    .IoStatus={ .__annonCompField4={ .Status=0 }, .Information=0ul },
    .RequestorMode=0,
    .PendingReturned=0, .StackCount=0,
    .CurrentLocation=0, .Cancel=0, .CancelIrql=0,
    .ApcEnvironment=0, .AllocationFlags=0, .UserIosb=((PIO_STATUS_BLOCK)NULL),
    .UserEvent=((PKEVENT)NULL), .Overlay={ .AsynchronousParameters={ .UserApcRoutine=((const void (*)(const void *, PIO_STATUS_BLOCK, unsigned long int))NULL), .UserApcContext=NULL } },
    .CancelRoutine=((const void (*)(PDEVICE_OBJECT, PIRP))NULL),
    .UserBuffer=NULL,
    .Tail={ .Overlay={ .__annonCompField15={ .DeviceQueueEntry={ .DeviceListEntry={ .Flink=((struct _LIST_ENTRY *)NULL), .Blink=((struct _LIST_ENTRY *)NULL) }, .SortKey=0ul,
    .Inserted=0, .$pad0=0 } }, .Thread=((PETHREAD)NULL),
    .AuxiliaryBuffer=((PCCHAR)NULL), .__annonCompField17={ .ListEntry={ .Flink=((struct _LIST_ENTRY *)NULL), .Blink=((struct _LIST_ENTRY *)NULL) }, .__annonCompField16={ .CurrentStackLocation=((struct _IO_STACK_LOCATION *)NULL) + 40 } },
    .OriginalFileObject=((PFILE_OBJECT)NULL) } } } ({ 0000000000000000, 0000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000100010011111111101111110, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000000000000000000000000000, 00000000000000000000000000000000, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, 00000000000000000000000000000000, { { { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, 00000000, 000000000000000000000000 }, 00000000000000000000000000000000, 00000000000000000000000000000000, { { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000101000 }, 00000000000000000000000000000000 } })

State 244 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3183 function main thread 0
----------------------------------------------------
  myStatus=0 (00000000000000000000000000000000)

State 248 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3149 function stub_driver_init thread 0
----------------------------------------------------
  s=1 (00000000000000000000000000000001)

State 249 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3150 function stub_driver_init thread 0
----------------------------------------------------
  customIrp=0 (00000000000000000000000000000000)

State 250 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3151 function stub_driver_init thread 0
----------------------------------------------------
  setEventCalled=0 (00000000000000000000000000000000)

State 251 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3152 function stub_driver_init thread 0
----------------------------------------------------
  lowerDriverReturn=0 (00000000000000000000000000000000)

State 252 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3153 function stub_driver_init thread 0
----------------------------------------------------
  compRegistered=0 (00000000000000000000000000000000)

State 253 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3154 function stub_driver_init thread 0
----------------------------------------------------
  compFptr=((signed int (*)(PDEVICE_OBJECT, PIRP, const void *))NULL) (00000000000000000000000000000000)

State 254 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3155 function stub_driver_init thread 0
----------------------------------------------------
  pended=0 (00000000000000000000000000000000)

State 262 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3223 function main thread 0
----------------------------------------------------
  DeviceObject=&devobj!0@1.Type (00000100000000000000000000000000)

State 263 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3223 function main thread 0
----------------------------------------------------
  Irp=&irp!0@1.Type (00000011000000000000000000000000)

State 264 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2533 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  deviceExtension=((PDEVICE_EXTENSION)NULL) (00000000000000000000000000000000)

State 265 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2534 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  currentIrpStack=((PIO_STACK_LOCATION)NULL) (00000000000000000000000000000000)

State 266 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2535 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  status=0 (00000000000000000000000000000000)

State 267 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2536 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  i=0ul (00000000000000000000000000000000)

State 268 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2537 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  totalCounters=((PDISK_PERFORMANCE)NULL) (00000000000000000000000000000000)

State 269 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2538 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  diskCounters=((PDISK_PERFORMANCE)NULL) (00000000000000000000000000000000)

State 270 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2539 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  frequency={ .__annonCompField1={ .LowPart=340787200ul, .HighPart=-1898 } } ({ 00010100010100000000000000000000, 11111111111111111111100010010110 })

State 271 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2540 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  perfctr={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } } ({ 00000000000000000000000000000000, 00000000000000000000000000000000 })

State 272 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2541 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  difference={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } } ({ 00000000000000000000000000000000, 00000000000000000000000000000000 })

State 273 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2542 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  tmp=0 (00000000000000000000000000000000)

State 274 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2545 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  deviceExtension=((PDEVICE_EXTENSION)NULL) + -7733311 (00000000100010011111111111000001)

State 275 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2546 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  currentIrpStack=((PIO_STACK_LOCATION)NULL) + 40 (00000000000000000000000000101000)

State 278 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2552 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  diskCounters=((PDISK_PERFORMANCE)NULL) + 2 (00000000000000000000000000000010)

State 280 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2564 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  totalCounters=((PDISK_PERFORMANCE)NULL) + -7733378 (00000000100010011111111101111110)

State 283 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  s=NULL + -7733378 (00000000100010011111111101111110)

State 284 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  c=0 (00000000000000000000000000000000)

State 285 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2565 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  n=88ul (00000000000000000000000001011000)

State 297 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2566 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  perfctr={ .__annonCompField1={ .LowPart=1074476040ul, .HighPart=8388673 } } ({ 01000000000010110011010000001000, 00000000100000000000000001000001 })

State 301 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2568 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  i=0ul (00000000000000000000000000000000)

State 307 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2579 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  TotalCounters=((PDISK_PERFORMANCE)NULL) + -7733378 (00000000100010011111111101111110)

State 308 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2579 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  NewCounters=((PDISK_PERFORMANCE)NULL) + 2 (00000000000000000000000000000010)

State 309 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2579 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  Frequency={ .__annonCompField1={ .LowPart=340787200ul, .HighPart=-1898 } } ({ 00010100010100000000000000000000, 11111111111111111111100010010110 })

State 310 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3105 function DiskPerfAddCounters thread 0
----------------------------------------------------
  TotalCounters$object={ .BytesRead={ .__annonCompField1={ .LowPart=5ul, .HighPart=0 } }, .BytesWritten={ .__annonCompField1={ .LowPart=1ul, .HighPart=0 } },
    .ReadTime={ .__annonCompField1={ .LowPart=2ul, .HighPart=0 } },
    .WriteTime={ .__annonCompField1={ .LowPart=2ul, .HighPart=0 } },
    .IdleTime={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } },
    .ReadCount=1ul,
    .WriteCount=1ul, .QueueDepth=0ul, .SplitCount=1ul,
    .QueryTime={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } }, .StorageDeviceNumber=0ul,
    .StorageManagerName={ 0, 0, 0, 0, 0, 0, 0, 0 }, .$pad0=0ul } ({ { 00000000000000000000000000000101, 00000000000000000000000000000000 }, { 00000000000000000000000000000001, 00000000000000000000000000000000 }, { 00000000000000000000000000000010, 00000000000000000000000000000000 }, { 00000000000000000000000000000010, 00000000000000000000000000000000 }, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000001, 00000000000000000000000000000001, 00000000000000000000000000000000, 00000000000000000000000000000001, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, { 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000 }, 00000000000000000000000000000000 })

State 311 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3106 function DiskPerfAddCounters thread 0
----------------------------------------------------
  TotalCounters$object={ .BytesRead={ .__annonCompField1={ .LowPart=5ul, .HighPart=0 } }, .BytesWritten={ .__annonCompField1={ .LowPart=1ul, .HighPart=0 } },
    .ReadTime={ .__annonCompField1={ .LowPart=2ul, .HighPart=0 } },
    .WriteTime={ .__annonCompField1={ .LowPart=2ul, .HighPart=0 } },
    .IdleTime={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } },
    .ReadCount=1ul,
    .WriteCount=1ul, .QueueDepth=0ul, .SplitCount=1ul,
    .QueryTime={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } }, .StorageDeviceNumber=0ul,
    .StorageManagerName={ 0, 0, 0, 0, 0, 0, 0, 0 }, .$pad0=0ul } ({ { 00000000000000000000000000000101, 00000000000000000000000000000000 }, { 00000000000000000000000000000001, 00000000000000000000000000000000 }, { 00000000000000000000000000000010, 00000000000000000000000000000000 }, { 00000000000000000000000000000010, 00000000000000000000000000000000 }, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000001, 00000000000000000000000000000001, 00000000000000000000000000000000, 00000000000000000000000000000001, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, { 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000 }, 00000000000000000000000000000000 })

State 312 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3107 function DiskPerfAddCounters thread 0
----------------------------------------------------
  TotalCounters$object.ReadCount=1ul (00000000000000000000000000000001)

State 313 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3108 function DiskPerfAddCounters thread 0
----------------------------------------------------
  TotalCounters$object.WriteCount=1ul (00000000000000000000000000000001)

State 314 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3109 function DiskPerfAddCounters thread 0
----------------------------------------------------
  TotalCounters$object.SplitCount=1ul (00000000000000000000000000000001)

State 316 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3115 function DiskPerfAddCounters thread 0
----------------------------------------------------
  TotalCounters$object={ .BytesRead={ .__annonCompField1={ .LowPart=5ul, .HighPart=0 } }, .BytesWritten={ .__annonCompField1={ .LowPart=1ul, .HighPart=0 } },
    .ReadTime={ .__annonCompField1={ .LowPart=1562021196ul, .HighPart=411887 } },
    .WriteTime={ .__annonCompField1={ .LowPart=2ul, .HighPart=0 } },
    .IdleTime={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } },
    .ReadCount=1ul,
    .WriteCount=1ul, .QueueDepth=0ul, .SplitCount=1ul,
    .QueryTime={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } }, .StorageDeviceNumber=0ul,
    .StorageManagerName={ 0, 0, 0, 0, 0, 0, 0, 0 }, .$pad0=0ul } ({ { 00000000000000000000000000000101, 00000000000000000000000000000000 }, { 00000000000000000000000000000001, 00000000000000000000000000000000 }, { 01011101000110101000110101001100, 00000000000001100100100011101111 }, { 00000000000000000000000000000010, 00000000000000000000000000000000 }, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000001, 00000000000000000000000000000001, 00000000000000000000000000000000, 00000000000000000000000000000001, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, { 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000 }, 00000000000000000000000000000000 })

State 317 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3116 function DiskPerfAddCounters thread 0
----------------------------------------------------
  TotalCounters$object={ .BytesRead={ .__annonCompField1={ .LowPart=5ul, .HighPart=0 } }, .BytesWritten={ .__annonCompField1={ .LowPart=1ul, .HighPart=0 } },
    .ReadTime={ .__annonCompField1={ .LowPart=1562021196ul, .HighPart=411887 } },
    .WriteTime={ .__annonCompField1={ .LowPart=2928494247ul, .HighPart=16983159 } },
    .IdleTime={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } },
    .ReadCount=1ul,
    .WriteCount=1ul, .QueueDepth=0ul, .SplitCount=1ul,
    .QueryTime={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } }, .StorageDeviceNumber=0ul,
    .StorageManagerName={ 0, 0, 0, 0, 0, 0, 0, 0 }, .$pad0=0ul } ({ { 00000000000000000000000000000101, 00000000000000000000000000000000 }, { 00000000000000000000000000000001, 00000000000000000000000000000000 }, { 01011101000110101000110101001100, 00000000000001100100100011101111 }, { 10101110100011010100011010100111, 00000001000000110010010001110111 }, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000001, 00000000000000000000000000000001, 00000000000000000000000000000000, 00000000000000000000000000000001, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, { 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000 }, 00000000000000000000000000000000 })

State 318 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 3117 function DiskPerfAddCounters thread 0
----------------------------------------------------
  TotalCounters$object={ .BytesRead={ .__annonCompField1={ .LowPart=5ul, .HighPart=0 } }, .BytesWritten={ .__annonCompField1={ .LowPart=1ul, .HighPart=0 } },
    .ReadTime={ .__annonCompField1={ .LowPart=1562021196ul, .HighPart=411887 } },
    .WriteTime={ .__annonCompField1={ .LowPart=2928494247ul, .HighPart=16983159 } },
    .IdleTime={ .__annonCompField1={ .LowPart=4127195136ul, .HighPart=26073296 } },
    .ReadCount=1ul,
    .WriteCount=1ul, .QueueDepth=0ul, .SplitCount=1ul,
    .QueryTime={ .__annonCompField1={ .LowPart=0ul, .HighPart=0 } }, .StorageDeviceNumber=0ul,
    .StorageManagerName={ 0, 0, 0, 0, 0, 0, 0, 0 }, .$pad0=0ul } ({ { 00000000000000000000000000000101, 00000000000000000000000000000000 }, { 00000000000000000000000000000001, 00000000000000000000000000000000 }, { 01011101000110101000110101001100, 00000000000001100100100011101111 }, { 10101110100011010100011010100111, 00000001000000110010010001110111 }, { 11110110000000000000000000000000, 00000001100011011101100011010000 }, 00000000000000000000000000000001, 00000000000000000000000000000001, 00000000000000000000000000000000, 00000000000000000000000000000001, { 00000000000000000000000000000000, 00000000000000000000000000000000 }, 00000000000000000000000000000000, { 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000, 0000000000000000 }, 00000000000000000000000000000000 })

State 320 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2580 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  diskCounters=((PDISK_PERFORMANCE)NULL) + 58 (00000000000000000000000000111010)

State 321 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2581 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  i=1ul (00000000000000000000000000000001)

State 327 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2586 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  totalCounters$object.QueueDepth=32ul (00000000000000000000000000100000)

State 329 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2598 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  totalCounters$object.StorageDeviceNumber=0ul (00000000000000000000000000000000)

State 332 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  dst=NULL + -7733310 (00000000100010011111111111000010)

State 333 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  src=NULL + -7733295 (00000000100010011111111111010001)

State 334 file ../sv-benchmarks/c/ntdrivers/diskperf_true-unreach-call.i.cil.c line 2599 function DiskPerfDeviceControl thread 0
----------------------------------------------------
  n=16ul (00000000000000000000000000010000)

Violated property:
  file <builtin-library-memcpy> line 26 function memcpy
  memcpy src/dst overlap
  POINTER_OBJECT(dst) != POINTER_OBJECT(src) || (unsigned int)POINTER_OFFSET(src) + n <= (unsigned int)POINTER_OFFSET(dst) || (unsigned int)POINTER_OFFSET(dst) + n <= (unsigned int)POINTER_OFFSET(src)


VERIFICATION FAILED
EC=10
FALSE

@marek-trtik
Copy link
Owner Author

The cause is the assert violation in
https://github.com/marek-trtik/cbmc/blob/sv-comp-2018-patches/src/ansi-c/library/string.c#L532

@marek-trtik marek-trtik mentioned this issue Nov 10, 2017
Closed
@lucasccordeiro
Copy link
Collaborator

@marek-trtik: Are we enabling the pointer-check here? In this category, we're supposed to check the reachability of the error label only.

It seems that there are some benchmarks with memory related errors, which are marked as safe. @tautschnig and @peterschrammel: do you remember whether we have discussed it in previous editions of SV-COMP?

@marek-trtik
Copy link
Owner Author

Here is description how to set NONDET and uninitialised variables in order to reach and violate the assumption of memcpy shown in the log above:

line 3161:
    status = 1
line 3163:
    irp.AssociatedIrp.SystemBuffer = &d.MajorFunction[20] - OFFSET(_DISK_PERFORMANCE, StorageManagerName)
    Irp.Tail.Overlay.__annonCompField17.__annonCompField16.CurrentStackLocation = &d.MajorFunction[10]
   Irp.Tail.Overlay.__annonCompField17.__annonCompField16.CurrentStackLocation->Parameters.DeviceIoControl.IoControlCode =  (ULONG )((7 << 16) | (8 << 2)))
   Irp.Tail.Overlay.__annonCompField17.__annonCompField16.CurrentStackLocation->Parameters.DeviceIoControl.OutputBufferLength = (ULONG )sizeof(DISK_PERFORMANCE )
line 3164:
    __BLAST_NONDET___0 = 2
line 3166:
    devobj.DeviceExtension = &d.MajorFunction[20] - OFFSET(_DEVICE_EXTENSION, StorageManagerName)
    devobj.DeviceExtension->Processors = 0
    devobj.DeviceExtension->DiskCounters = 1
    devobj.DeviceExtension->QueueDepth = 1

@marek-trtik
Copy link
Owner Author

The benchmark also has undefined objects (declared only). So it does not compile.

@lucasccordeiro
Copy link
Collaborator

It looks like this benchmark should be removed from SV-COMP. For doing this, we would need to

(1) replace the nondet function calls by the concrete values;
(2) replace the __VERIFIER_error label by an assertion statement;
(3) then compile and run the benchmark to trigger the assertion violation.

However, since this benchmark contains undefined behaviour, anything can happen. Additionally, if the benchmark does not compile as it is, then we have to think on an alternative solution.

@marek-trtik
Copy link
Owner Author

marek-trtik commented Nov 13, 2017 •
edited
Loading

The alternative solution is to check the correctness of the proof/witness of reachability of the undefined behaviour in memcpy I posted above. I mean to do this manually, by looking into the benchmarks while taking assumptions about non-deterministicaly chosen values at lines in the proof.

@lucasccordeiro
Copy link
Collaborator

@marek-trtik: We should also report this issue in the sv-comp repository. These benchmarks with undefined behaviour clearly pose a big risk to the reputation of the SV-COMP.

@marek-trtik
Copy link
Owner Author

Here is the link to the PR:
sosy-lab/sv-benchmarks#498

@marek-trtik
Copy link
Owner Author

Dirk closed the PR without merge. However, the PR
sosy-lab/sv-benchmarks#512
fixes the benchmark so that we timeout on it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@marek-trtik marek-trtik

Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@lucasccordeiro @marek-trtik