./goblint --conf conf/svcomp23.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2216:5-2232:5 with factor 5
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2928:29-2946:29 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3592:7-3614:7 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:4469:3-4531:3 with factor 1
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:5333:9-5352:9 with factor 4
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:5437:3-5472:3 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:5556:5-5570:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:5794:5-5872:5 with factor 1
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:5892:7-5913:7 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6021:3-6113:3 with factor 1
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6171:3-6183:3 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6276:5-6294:5 with factor 4
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6299:5-6355:5 with factor 1
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:3-6446:3 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6880:3-6971:3 with factor 1
Collected factors:
functions: 127
functionCalls: 333
loops: 28
loopBreaks: 0
controlFlowStatements: 1895
expressions: 13386
instructions: 1733
integralVars: (20,279)
arrayVars: (7,5)
pointerVars: (5,272)

Complexity estimates:
File: 670914
function FlReadWriteTrack is recursive, disable interval context
malloc wrapper: FlFdcDeviceIo
no thread creation -> disabeling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn"
Total: 670914
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7028:3-7028:63)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7036:3-7036:15)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7036:3-7036:15)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7036:3-7036:15)
[Info][Unsound] Unknown address in {&d} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7038:3-7038:33)
[Info][Unsound] Unknown address in {&u} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7038:3-7038:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7038:3-7038:33)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2154:7-2154:63)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2165:7-2165:84)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2170:7-2170:84)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7084:17-7084:59)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7084:17-7084:59)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7084:17-7084:59)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7084:17-7084:59)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7084:17-7084:59)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7084:17-7084:59)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2668:3-2668:29)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2668:3-2668:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2668:3-2668:29)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7089:17-7089:59)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7089:17-7089:59)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7089:17-7089:59)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7089:17-7089:59)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7089:17-7089:59)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7089:17-7089:59)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7094:17-7094:61)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7094:17-7094:61)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7094:17-7094:61)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7094:17-7094:61)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7094:17-7094:61)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7094:17-7094:61)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2704:7-2704:41)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2707:7-2707:60)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2707:7-2707:60)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2707:7-2707:60)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2707:7-2707:60)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6777:3-6777:113)
[Info][Unsound] Unknown address in {&irp.CancelRoutine} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6777:3-6777:113)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6777:3-6777:113)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:1767:10-1767:28)
[Info][Unsound] Unknown address in {&irp.CancelRoutine} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6781:5-6781:93)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6781:5-6781:93)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6783:9-6783:89)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6788:7-6788:33)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6788:7-6788:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6788:7-6788:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6810:6-6810:192)
[Info][Unsound] Unknown address in {&irp.Tail.Overlay.__annonCompField17.ListEntry} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6819:5-6820:79)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6819:5-6820:79)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).NewRequestQueue} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6819:5-6820:79)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).NewRequestQueueSpinLock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6819:5-6820:79)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6819:5-6820:79)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2720:7-2720:35)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2725:5-2725:31)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2725:5-2725:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2725:5-2725:31)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2731:7-2731:37)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2740:5-2740:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2742:5-2742:62)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2742:5-2742:62)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2742:5-2742:62)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2742:5-2742:62)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2951:33-2951:110)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3061:33-3061:110)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3090:29-3090:91)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3092:29-3093:58)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3092:29-3093:58)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3092:29-3093:58)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3092:29-3093:58)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2797:29-2797:89)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2798:33-2798:152)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2798:33-2798:152)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2806:29-2807:58)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2809:29-2809:111)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2815:33-2815:76)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2827:29-2827:97)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2828:33-2828:155)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2828:33-2828:155)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2836:29-2837:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2839:29-2839:114)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2853:29-2853:143)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2853:29-2853:143)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6436:9-6436:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6437:11-6437:111)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6445:5-6445:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6449:7-6449:99)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6449:7-6449:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6453:9-6453:107)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6453:9-6453:107)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6456:11-6456:107)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6456:11-6456:107)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6459:13-6459:94)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6462:15-6462:94)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6465:17-6465:92)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6468:19-6468:96)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6469:21-6469:59)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6469:21-6469:59)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6472:23-6472:61)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6472:23-6472:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6475:25-6475:63)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6475:25-6475:63)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6478:27-6478:65)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6478:27-6478:65)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6481:29-6481:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6481:29-6481:68)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2871:31-2871:215)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2876:37-2876:85)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2880:39-2880:87)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2898:29-2898:82)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2898:29-2898:82)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2898:29-2898:82)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2898:29-2898:82)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2559:7-2559:49)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2579:3-2579:48)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2579:3-2579:48)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2581:7-2581:52)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2583:5-2583:50)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2583:5-2583:50)
[Info][Unsound] Unknown address in {&threadHandle} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2602:5-2603:80)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2602:5-2603:80)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2602:5-2603:80)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2607:7-2607:51)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2627:5-2628:50)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2627:5-2628:50)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).FloppyThread} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2627:5-2628:50)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2629:5-2629:26)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2642:4-2642:190)
[Info][Unsound] Unknown address in {&irp.Tail.Overlay.__annonCompField17.ListEntry} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2651:3-2652:66)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2651:3-2652:66)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).ListEntry} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2651:3-2652:66)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).ListSpinLock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2651:3-2652:66)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2651:3-2652:66)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2653:3-2653:70)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).RequestSemaphore} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2653:3-2653:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2917:33-2917:168)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2917:33-2917:168)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2917:33-2917:168)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2921:31-2921:176)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2921:31-2921:176)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2921:31-2921:176)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2921:31-2921:176)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2926:29-2926:69)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2930:35-2930:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2935:31-2935:93)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2936:31-2936:132)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2937:31-2937:85)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2938:31-2938:105)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2939:31-2939:105)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2940:31-2940:103)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2944:31-2944:94)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2945:31-2945:56)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2930:35-2930:91)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2944:31-2944:94)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2945:31-2945:56)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2930:35-2930:91)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2944:31-2944:94)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2945:31-2945:56)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2954:35-2954:74)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2979:31-2980:75)
[Info][Unsound] Unknown address in {&queryTable[def_exc:0; intervals:[0,0]; enums:{0}]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2988:31-2990:75)
[Info][Unsound] Unknown value in {&((alloc@sid:4557@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7221:3-7221:30)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2988:31-2990:75)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2988:31-2990:75)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3075:31-3075:84)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3075:31-3075:84)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3075:31-3075:84)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3075:31-3075:84)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3156:5-3156:31)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3156:5-3156:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3156:5-3156:31)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7099:17-7099:51)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7099:17-7099:51)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7099:17-7099:51)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7099:17-7099:51)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7099:17-7099:51)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7099:17-7099:51)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3194:7-3194:35)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3199:5-3199:31)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3199:5-3199:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3199:5-3199:31)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3243:23-3243:53)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3252:21-3252:83)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3254:21-3254:83)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3254:21-3254:83)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3254:21-3254:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3254:21-3254:83)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3231:19-3231:66)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3231:19-3231:66)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3231:19-3231:66)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3231:19-3231:66)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3231:19-3231:66)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3231:19-3231:66)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3547:3-3547:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3547:3-3547:35)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3550:3-3550:54)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3551:3-3551:53)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3552:3-3552:65)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3552:3-3552:65)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3552:3-3552:65)
[Info][Unsound] Unknown address in {&((alloc@sid:4463@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7029:3-7029:119)[def_exc:3; intervals:[3,3]; enums:{3}]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3552:3-3552:65)
[Info][Unsound] Unknown value in {&((alloc@sid:4463@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7029:3-7029:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3552:3-3552:65)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3552:3-3552:65)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3552:3-3552:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7660:5-7660:57)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7660:5-7660:57)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7660:5-7660:57)
[Info][Unsound] Unknown address in {&((alloc@sid:4463@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7029:3-7029:119)[def_exc:3; intervals:[3,3]; enums:{3}]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7660:5-7660:57)
[Info][Unsound] Unknown value in {&((alloc@sid:4463@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7029:3-7029:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7660:5-7660:57)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7660:5-7660:57)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7660:5-7660:57)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3556:5-3556:70)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3556:5-3556:70)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3565:3-3566:38)
[Info][Unsound] Unknown value in {&fdcInfo} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3565:3-3566:38)
[Info][Unsound] Unknown address in {&fdcInfo} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3565:3-3566:38)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3565:3-3566:38)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6569:3-6570:69)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6569:3-6570:69)
[Info][Unsound] Unknown value in {&ioStatus} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6569:3-6570:69)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6569:3-6570:69)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6572:7-6572:55)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6580:3-6580:116)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6582:3-6582:84)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6583:3-6583:94)
[Info][Unsound] Unknown value in {&fdcInfo} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6584:3-6584:63)
[Info][Unsound] Unknown address in {&fdcInfo} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6584:3-6584:63)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6584:3-6584:63)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6585:3-6585:46)
[Info][Unsound] Unknown value in {&fdcInfo} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6585:3-6585:46)
[Info][Unsound] Unknown address in {&fdcInfo} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6585:3-6585:46)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6585:3-6585:46)
[Info][Unsound] Unknown value in {&fdcInfo} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7660:5-7660:57)
[Info][Unsound] Unknown address in {&fdcInfo} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7660:5-7660:57)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6589:5-6589:59)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6589:5-6589:59)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3569:5-3569:65)
[Info][Unsound] Unknown value in {&fdcInfo} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3573:9-3573:71)
[Info][Unsound] Unknown address in {&fdcInfo} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3573:9-3573:71)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3573:9-3573:71)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3573:9-3573:71)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2485:7-2485:72)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2488:9-2488:74)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2491:11-2491:76)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2494:13-2494:78)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2497:15-2497:80)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2530:3-2530:43)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2531:3-2531:108)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2532:3-2532:112)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2532:3-2532:112)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2533:3-2533:92)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2533:3-2533:92)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2534:3-2534:92)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2534:3-2534:92)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2535:3-2535:100)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2535:3-2535:100)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2536:3-2536:97)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2536:3-2536:97)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2537:3-2537:104)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2537:3-2537:104)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2538:3-2538:98)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2538:3-2538:98)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2539:3-2539:106)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2539:3-2539:106)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2540:3-2540:96)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2540:3-2540:96)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2541:3-2541:123)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2541:3-2541:123)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2542:3-2542:125)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2542:3-2542:125)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2543:3-2543:97)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2543:3-2543:97)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2544:3-2544:96)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2544:3-2544:96)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3575:13-3575:52)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3576:11-3576:126)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3576:11-3576:126)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3576:11-3576:126)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3585:11-3585:50)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3586:9-3586:124)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3586:9-3586:124)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3586:9-3586:124)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3601:9-3604:63)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3601:9-3604:63)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3601:9-3604:63)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3601:9-3604:63)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3601:9-3604:63)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3601:9-3604:63)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3601:9-3604:63)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3619:11-3619:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3620:9-3620:75)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3620:9-3620:75)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3621:9-3621:77)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3621:9-3621:77)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3623:9-3623:81)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3623:9-3623:81)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3624:9-3624:136)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3624:9-3624:136)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3624:9-3624:136)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3624:9-3624:136)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3627:7-3628:93)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3627:7-3628:93)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).InterfaceString} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3627:7-3628:93)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3632:9-3633:49)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).InterfaceString} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3632:9-3633:49)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3639:7-3639:39)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3641:7-3641:45)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3643:7-3643:53)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6883:5-6884:92)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).NewRequestQueue} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6883:5-6884:92)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).NewRequestQueueSpinLock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6883:5-6884:92)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3654:3-3654:29)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3654:3-3654:29)
[Info][Unsound] Unknown address in {&((alloc@sid:4463@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7029:3-7029:119)[def_exc:3; intervals:[3,3]; enums:{3}]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3654:3-3654:29)
[Info][Unsound] Unknown value in {&((alloc@sid:4463@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7029:3-7029:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3654:3-3654:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3654:3-3654:29)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3654:3-3654:29)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3262:19-3262:57)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3264:19-3264:72)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3264:19-3264:72)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3264:19-3264:72)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3264:19-3264:72)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3268:21-3269:53)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3278:21-3278:64)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3289:21-3289:83)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3291:21-3291:83)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3291:21-3291:83)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3291:21-3291:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3291:21-3291:83)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3299:21-3299:47)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3299:21-3299:47)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3299:21-3299:47)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3312:23-3312:53)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3323:21-3323:83)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3325:21-3325:83)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3325:21-3325:83)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3325:21-3325:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3325:21-3325:83)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3354:21-3354:53)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3354:21-3354:53)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3357:21-3357:72)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3358:21-3358:71)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3359:21-3359:83)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3359:21-3359:83)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3359:21-3359:83)
[Info][Unsound] Unknown address in {&((alloc@sid:4463@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7029:3-7029:119)[def_exc:3; intervals:[3,3]; enums:{3}]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3359:21-3359:83)
[Info][Unsound] Unknown value in {&((alloc@sid:4463@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7029:3-7029:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3359:21-3359:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3359:21-3359:83)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3359:21-3359:83)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3363:23-3363:77)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3363:23-3363:77)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3371:21-3371:59)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3373:21-3373:67)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3377:21-3377:47)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3377:21-3377:47)
[Info][Unsound] Unknown address in {&((alloc@sid:4463@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7029:3-7029:119)[def_exc:3; intervals:[3,3]; enums:{3}]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3377:21-3377:47)
[Info][Unsound] Unknown value in {&((alloc@sid:4463@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7029:3-7029:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3377:21-3377:47)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3377:21-3377:47)
[Info][Unsound] Unknown address in {&doneEvent} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3377:21-3377:47)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3384:19-3384:51)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3395:19-3395:81)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3397:19-3397:81)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3397:19-3397:81)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3397:19-3397:81)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3397:19-3397:81)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3405:19-3405:57)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3407:19-3407:51)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3408:19-3408:51)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3409:19-3409:65)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3419:19-3419:81)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3423:19-3423:81)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3423:19-3423:81)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3423:19-3423:81)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3423:19-3423:81)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3425:23-3425:109)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3427:21-3428:49)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).InterfaceString} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3427:21-3428:49)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3439:23-3439:67)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3441:21-3441:71)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65).ArcName} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3441:21-3441:71)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3452:19-3452:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3466:19-3466:81)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3468:19-3468:81)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3468:19-3468:81)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3468:19-3468:81)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3468:19-3468:81)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7104:17-7104:53)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7104:17-7104:53)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7104:17-7104:53)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7104:17-7104:53)
[Info][Unsound] Unknown value in {&((alloc@sid:4459@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7026:3-7026:65)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7104:17-7104:53)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7104:17-7104:53)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3698:13-3698:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3699:15-3699:42)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3711:13-3711:58)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3722:11-3722:37)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3722:11-3722:37)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3722:11-3722:37)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3734:13-3734:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3738:15-3738:43)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3741:13-3741:48)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3747:13-3747:48)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3752:15-3752:91)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3755:15-3755:89)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3789:3-3789:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3791:3-3791:64)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3791:3-3791:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3791:3-3791:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3791:3-3791:64)
[Info][Unsound] Unknown address in {&d} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7120:7-7120:24)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7120:7-7120:24)
[Warning][Deadcode] Function 'FloppyAddDevice' is uncalled: 57 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2190:1-2328:1)
[Warning][Deadcode] Function 'FlConfigCallBack' is uncalled: 69 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2329:1-2473:1)
[Warning][Deadcode] Function 'FloppyReadWrite' is uncalled: 34 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3796:1-3890:1)
[Warning][Deadcode] Function 'FlInterpretError' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3891:1-3967:1)
[Warning][Deadcode] Function 'FlFinishOperation' is uncalled: 34 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3968:1-4076:1)
[Warning][Deadcode] Function 'FlStartDrive' is uncalled: 113 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:4077:1-4388:1)
[Warning][Deadcode] Function 'FlDatarateSpecifyConfigure' is uncalled: 28 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:4389:1-4460:1)
[Warning][Deadcode] Function 'FlRecalibrateDrive' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:4461:1-4538:1)
[Warning][Deadcode] Function 'FlDetermineMediaType' is uncalled: 88 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:4539:1-4773:1)
[Warning][Deadcode] Function 'FlAllocateIoBuffer' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:4774:1-4851:1)
[Warning][Deadcode] Function 'FlFreeIoBuffer' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:4852:1-4884:1)
[Warning][Deadcode] Function 'FloppyThread' is uncalled: 174 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:4885:1-5390:1)
[Warning][Deadcode] Function 'FlConsolidateMediaTypeWithBootSector' is uncalled: 82 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:5391:1-5590:1)
[Warning][Deadcode] Function 'FlCheckBootSector' is uncalled: 19 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:5591:1-5645:1)
[Warning][Deadcode] Function 'FlReadWriteTrack' is uncalled: 108 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:5646:1-5924:1)
[Warning][Deadcode] Function 'FlReadWrite' is uncalled: 73 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:5925:1-6132:1)
[Warning][Deadcode] Function 'FlFormat' is uncalled: 116 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6133:1-6426:1)
[Warning][Deadcode] Function 'FlIssueCommand' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6502:1-6531:1)
[Warning][Deadcode] Function 'FlInitializeControllerHardware' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6532:1-6556:1)
[Warning][Deadcode] Function 'FlHdbit' is uncalled: 65 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6598:1-6757:1)
[Warning][Deadcode] Function 'FloppyCancelQueuedRequest' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6827:1-6868:1)
[Warning][Deadcode] Function 'ExAcquireFastMutex' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7196:1-7202:1)
[Warning][Deadcode] Function 'ExReleaseFastMutex' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7204:1-7210:1)
[Warning][Deadcode] Function 'ExFreePool' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7228:1-7234:1)
[Warning][Deadcode] Function 'ExfInterlockedInsertHeadList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7238:1-7246:1)
[Warning][Deadcode] Function 'IoAllocateMdl' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7272:1-7297:1)
[Warning][Deadcode] Function 'IoAttachDeviceToDeviceStack' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7300:1-7320:1)
[Warning][Deadcode] Function 'IoBuildAsynchronousFsdRequest' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7327:1-7354:1)
[Warning][Deadcode] Function 'IoCreateDevice' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7398:1-7425:1)
[Warning][Deadcode] Function 'IoCreateSymbolicLink' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7428:1-7448:1)
[Warning][Deadcode] Function 'IoDeleteDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7450:1-7456:1)
[Warning][Deadcode] Function 'IoDetachDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7480:1-7486:1)
[Warning][Deadcode] Function 'IoFreeIrp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7488:1-7494:1)
[Warning][Deadcode] Function 'IoFreeMdl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7496:1-7502:1)
[Warning][Deadcode] Function 'IoReleaseCancelSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7595:1-7601:1)
[Warning][Deadcode] Function 'IoSetHardErrorOrVerifyDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7626:1-7632:1)
[Warning][Deadcode] Function 'KeAcquireSpinLockRaiseToDpc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7740:1-7746:1)
[Warning][Deadcode] Function 'KeDelayExecutionThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7750:1-7770:1)
[Warning][Deadcode] Function 'KeInitializeEvent' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7773:1-7779:1)
[Warning][Deadcode] Function 'KeInitializeSemaphore' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7782:1-7788:1)
[Warning][Deadcode] Function 'KeInitializeSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7790:1-7796:1)
[Warning][Deadcode] Function 'MmAllocateContiguousMemory' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7867:1-7893:1)
[Warning][Deadcode] Function 'MmFreeContiguousMemory' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7895:1-7901:1)
[Warning][Deadcode] Function 'MmMapLockedPagesSpecifyCache' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7908:1-7916:1)
[Warning][Deadcode] Function 'MmPageEntireDriver' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7918:1-7924:1)
[Warning][Deadcode] Function 'MmResetDriverPaging' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7926:1-7932:1)
[Warning][Deadcode] Function 'MmUnlockPages' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7934:1-7940:1)
[Warning][Deadcode] Function 'ObfDereferenceObject' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7970:1-7976:1)
[Warning][Deadcode] Function 'PoStartNextPowerIrp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8053:1-8059:1)
[Warning][Deadcode] Function 'PsTerminateSystemThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8091:1-8111:1)
[Warning][Deadcode] Function 'RtlAnsiStringToUnicodeString' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8115:1-8137:1)
[Warning][Deadcode] Function 'RtlCompareMemory' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8141:1-8148:1)
[Warning][Deadcode] Function 'RtlCopyUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8151:1-8158:1)
[Warning][Deadcode] Function 'RtlDeleteRegistryValue' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8162:1-8183:1)
[Warning][Deadcode] Function 'RtlFreeUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8185:1-8191:1)
[Warning][Deadcode] Function 'RtlInitString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8194:1-8200:1)
[Warning][Deadcode] Function 'RtlInitUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8203:1-8210:1)
[Warning][Deadcode] Function 'FlAcpiConfigureFloppy' has dead code:
  on line 2481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2481-2481)
  on line 2502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2502-2502)
[Warning][Deadcode] Function 'FlQueueIrpToThread' has dead code:
  on line 2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2647-2647)
[Warning][Deadcode] Function 'FloppyDeviceControl' has dead code:
  on line 2736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2736-2736)
  on line 2786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2786-2786)
  on line 2972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2972-2972)
  on line 3007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3007-3007)
  on line 3009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3009-3009)
  on line 3014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3014-3014)
  on line 3016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3016-3016)
  on line 3021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3021-3021)
  on line 3023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3023-3023)
  on lines 3033..3037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3033-3037)
  on lines 3039..3040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3039-3040)
  on line 3048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3048-3048)
  on line 3051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3051-3051)
  on lines 3053..3054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3053-3054)
  on line 3086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3086-3086)
  on line 3117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3117-3117)
  on line 3120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3120-3120)
  on line 3123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3123-3123)
  on line 3126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3126-3126)
  on line 3129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3129-3129)
  on line 3132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3132-3132)
  on line 3135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3135-3135)
[Warning][Deadcode] Function 'FloppyPnp' has dead code:
  on line 3228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3228-3228)
  on line 3248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3248-3248)
  on line 3285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3285-3285)
  on line 3319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3319-3319)
  on line 3339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3339-3339)
  on line 3344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3344-3344)
  on line 3391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3391-3391)
  on line 3415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3415-3415)
  on line 3462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3462-3462)
[Warning][Deadcode] Function 'FloppyPower' has dead code:
  on line 3694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3694-3694)
  on line 3785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3785-3785)
[Warning][Deadcode] Function 'FloppyProcessQueuedRequests' has dead code:
  on lines 6892..6893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6892-6893)
  on lines 6895..6896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6895-6896)
  on lines 6898..6899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6898-6899)
  on lines 6903..6904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6903-6904)
  on lines 6906..6908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6906-6908)
  on line 6911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6911-6911)
  on line 6914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6914-6914)
  on line 6917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6917-6917)
  on line 6922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6922-6922)
  on line 6926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6926-6926)
  on line 6931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6931-6931)
  on lines 6936..6938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6936-6938)
  on line 6951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6951-6951)
  on line 6954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6954-6954)
[Warning][Deadcode] Function 'FloppyQueueRequest' has dead code:
  on line 6815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6815-6815)
[Warning][Deadcode] Function 'FloppyStartDevice' has dead code:
  on line 3532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3532-3532)
  on line 3537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3537-3537)
[Warning][Deadcode] Function 'IoBuildDeviceIoControlRequest' has dead code:
  on line 7378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7378-7378)
[Warning][Deadcode] Function 'IoDeleteSymbolicLink' has dead code:
  on line 7467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7467-7467)
[Warning][Deadcode] Function 'IoQueryDeviceDescription' has dead code:
  on line 7554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7554-7554)
[Warning][Deadcode] Function 'IoRegisterDeviceInterface' has dead code:
  on line 7582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7582-7582)
[Warning][Deadcode] Function 'IoSetDeviceInterfaceState' has dead code:
  on line 7613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7613-7613)
[Warning][Deadcode] Function 'IofCallDriver' has dead code:
  on line 7681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7681-7681)
  on lines 7698..7699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7698-7699)
  on line 7715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7715-7715)
[Warning][Deadcode] Function 'KeWaitForSingleObject' has dead code:
  on line 7841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7841-7841)
  on line 7853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7853-7853)
[Warning][Deadcode] Function 'ObReferenceObjectByHandle' has dead code:
  on line 7957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7957-7957)
[Warning][Deadcode] Function 'PoCallDriver' has dead code:
  on lines 7989..7990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7989-7990)
  on line 7992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7992-7992)
  on line 7994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7994-7994)
  on line 8010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8010-8010)
  on lines 8027..8028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8027-8028)
  on lines 8031..8033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8031-8033)
  on lines 8035..8036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8035-8036)
  on line 8044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8044-8044)
[Warning][Deadcode] Function 'PsCreateSystemThread' has dead code:
  on line 8078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8078-8078)
[Warning][Deadcode] Function 'RtlQueryRegistryValues' has dead code:
  on line 8227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8227-8227)
[Warning][Deadcode] Function 'ZwClose' has dead code:
  on line 8249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8249-8249)
[Warning][Deadcode] Function 'errorFn' has dead code:
  on line 2091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2091-2091)
[Warning][Deadcode] Function 'main' has dead code:
  on line 7060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7060-7060)
  on line 7081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7081-7081)
  on line 7138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7138-7138)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 732
  dead: 1376 (1277 in uncalled functions)
  total: 2108
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-570] condition '! (status >= 0L)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7059:9-7059:25)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2928:36-2928:37)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7710:11-7710:21)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3387:23-3387:30)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3411:23-3411:30)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3781:7-3781:14)
[Warning][Deadcode][CWE-570] condition '! valueName' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2971:35-2971:46)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7137:11-7137:20)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3458:23-3458:30)
[Warning][Deadcode][CWE-571] condition 's != IPC' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7151:17-7151:25)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7827:9-7827:28)
[Warning][Deadcode][CWE-571] condition '(int )driveLetterName.Length != 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3000:35-3000:68)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition 'pended == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2643:7-2643:18)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7839:11-7839:20)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3530:7-3530:14)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3535:9-3535:28)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition 'pended == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6811:9-6811:20)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2732:9-2732:16)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3082:33-3082:40)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-570] condition 'compRegistered' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7987:7-7987:21)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3592:14-3592:15)
[Warning][Deadcode][CWE-570] condition 'ntStatus == -1073741661L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3116:11-3116:35)
[Warning][Deadcode][CWE-571] condition '(int )InterfaceType < 16' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3594:13-3594:37)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6880:10-6880:11)
[Warning][Deadcode][CWE-570] condition 'ntStatus == -1073741643L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3119:13-3119:37)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-570] condition 'ntStatus == -1073741662L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3122:15-3122:39)
[Warning][Deadcode][CWE-570] condition '(unsigned int )headOfList != (unsigned int )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6886:9-6886:64)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-570] condition 'ntStatus == -1073741805L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3125:17-3125:41)
[Warning][Deadcode][CWE-570] condition 'ntStatus == -2147483626L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3128:19-3128:43)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3592:14-3592:15)
[Warning][Deadcode][CWE-570] condition 'ntStatus == -1073741804L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3131:21-3131:45)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '(int )InterfaceType < 16' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3594:13-3594:37)
[Warning][Deadcode][CWE-570] condition 'ntStatus == -1073741806L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3134:23-3134:47)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8026:7-8026:14)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-570] condition 's == MPR1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8030:9-8030:18)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3592:14-3592:15)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:8039:11-8039:21)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '(int )InterfaceType < 16' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3594:13-3594:37)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3592:14-3592:15)
[Warning][Deadcode][CWE-571] condition '(int )InterfaceType < 16' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3594:13-3594:37)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3592:14-3592:15)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3244:25-3244:32)
[Warning][Deadcode][CWE-571] condition '(int )InterfaceType < 16' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3594:13-3594:37)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3592:14-3592:15)
[Warning][Deadcode][CWE-571] condition '(int )InterfaceType < 16' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3594:13-3594:37)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3281:25-3281:32)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3592:14-3592:15)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3315:25-3315:32)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2928:36-2928:37)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3337:25-3337:32)
[Warning][Deadcode][CWE-570] condition '! FdcInfo->AcpiFdiSupported' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2480:7-2480:34)
[Warning][Deadcode][CWE-571] condition '(long )compRetStatus1 == -1073741802L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7663:9-7663:46)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:3342:27-3342:46)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:6434:10-6434:11)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:2928:36-2928:37)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/floppy.i.cil-1.c:7697:7-7697:14)
SV-COMP result: unknown
