./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/cdaudio.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/cdaudio.i.cil-1.c:3228:5-3250:5 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:4169:31-4185:31 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:4646:29-4681:29 with factor 1
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:4738:29-4762:29 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:4771:31-4796:31 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:4819:29-4843:29 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:4912:29-4937:29 with factor 3
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:4974:29-4995:29 with factor 3
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:5252:31-5268:31 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:5840:31-5856:31 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:5901:31-5922:31 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6481:25-6497:25 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6883:29-6899:29 with factor 2
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:3-7570:66 with factor 8
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7571:3-7572:119 with factor 8
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7573:3-7574:74 with factor 8
Collected factors:
functions: 123
functionCalls: 385
loops: 22
loopBreaks: 0
controlFlowStatements: 1352
expressions: 14085
instructions: 2365
integralVars: (23,287)
arrayVars: (2,2)
pointerVars: (2,297)

Complexity estimates:
File: 576982
no thread creation -> disabeling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn"
Total: 576982
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7571:7-7571:49)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7573:7-7573:41)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7578:3-7578:15)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7578:3-7578:15)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7578:3-7578:15)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7619:13-7619:58)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7619:13-7619:58)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7619:13-7619:58)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7619:13-7619:58)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7619:13-7619:58)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3791:7-3791:35)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3808:13-3808:64)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3808:13-3808:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3808:13-3808:64)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3808:13-3808:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3808:13-3808:64)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6304:7-6304:105)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6304:7-6304:105)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6307:9-6307:93)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6307:9-6307:93)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6310:11-6310:109)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6310:11-6310:109)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6313:13-6313:110)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6313:13-6313:110)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6316:15-6316:112)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6316:15-6316:112)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6319:17-6319:116)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6319:17-6319:116)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6322:19-6322:117)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6322:19-6322:117)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6325:21-6325:118)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6325:21-6325:118)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6328:23-6328:121)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6328:23-6328:121)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6331:25-6331:124)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6331:25-6331:124)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6694:25-6694:58)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6694:25-6694:58)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6694:25-6694:58)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3875:7-3875:36)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7728:5-7728:20)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3884:7-3884:65)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3890:4-3890:65)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3891:4-3891:64)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3894:7-3894:75)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3904:5-3904:55)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3904:5-3904:55)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3918:7-3918:52)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3922:5-3922:36)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6698:25-6698:77)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6698:25-6698:77)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6698:25-6698:77)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6698:25-6698:77)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6698:25-6698:77)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6698:25-6698:77)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3856:3-3856:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3858:3-3858:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3858:3-3858:64)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3858:3-3858:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3858:3-3858:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6339:25-6339:64)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6339:25-6339:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6339:25-6339:64)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6348:29-6348:153)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6348:29-6348:153)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6348:29-6348:153)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6360:29-6360:85)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6368:25-6368:76)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6370:25-6370:54)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6372:25-6373:81)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6372:25-6373:81)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6372:25-6373:81)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6407:29-6407:153)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6407:29-6407:153)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6407:29-6407:153)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6415:25-6415:68)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6415:25-6415:68)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6415:25-6415:68)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6428:29-6428:77)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6436:25-6436:59)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6437:25-6437:54)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6438:25-6438:49)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6439:25-6439:79)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6440:25-6440:81)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6443:25-6443:101)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6443:25-6443:101)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6443:25-6443:101)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6525:29-6525:133)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6525:29-6525:133)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6539:29-6539:81)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6549:29-6549:92)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6563:25-6563:59)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6564:25-6564:48)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6565:25-6565:49)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6566:25-6566:51)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6567:25-6567:94)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6568:25-6569:85)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6568:25-6569:85)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6605:29-6605:130)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6605:29-6605:130)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6611:29-6611:87)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6612:31-6612:89)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6613:33-6613:91)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6614:31-6614:67)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6615:31-6615:59)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6624:27-6624:65)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6625:27-6625:81)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6626:27-6626:81)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6627:27-6627:81)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6628:27-6628:77)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6629:27-6629:77)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6630:27-6630:77)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6635:25-6636:55)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6651:29-6651:130)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6651:29-6651:130)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6658:25-6658:171)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6661:25-6661:53)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6662:25-6662:107)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6662:25-6662:107)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6662:25-6662:107)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6663:25-6663:107)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6663:25-6663:107)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6663:25-6663:107)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6664:25-6664:106)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6664:25-6664:106)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6664:25-6664:106)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6665:25-6665:95)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6665:25-6665:95)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6666:25-6667:55)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6678:25-6678:56)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6681:25-6681:55)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6682:25-6683:55)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6682:25-6683:55)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6728:3-6728:29)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6728:3-6728:29)
[Info][Unsound] Unknown value in {&((alloc@sid:3897@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6728:3-6728:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6728:3-6728:29)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3794:9-3794:37)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3813:13-3813:64)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3813:13-3813:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3813:13-3813:64)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3813:13-3813:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3813:13-3813:64)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6767:7-6767:91)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6767:7-6767:91)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6770:9-6770:106)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6770:9-6770:106)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6773:11-6773:108)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6773:11-6773:108)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6776:13-6776:110)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6776:13-6776:110)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6779:15-6779:112)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6779:15-6779:112)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6782:17-6782:114)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6782:17-6782:114)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6785:19-6785:117)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6785:19-6785:117)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6788:21-6788:120)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6788:21-6788:120)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6791:23-6791:121)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6791:23-6791:121)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6794:25-6794:122)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6794:25-6794:122)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6797:27-6797:125)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6797:27-6797:125)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6800:29-6800:128)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6800:29-6800:128)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7232:29-7232:72)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7232:29-7232:72)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7232:29-7232:72)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7241:31-7241:62)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7242:31-7242:83)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7242:31-7242:83)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7242:31-7242:83)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7242:31-7242:83)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7242:31-7242:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7242:31-7242:83)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7249:29-7249:81)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7249:29-7249:81)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7249:29-7249:81)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7249:29-7249:81)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7249:29-7249:81)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6807:33-6807:157)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6807:33-6807:157)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6807:33-6807:157)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6815:29-6815:68)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6815:29-6815:68)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6815:29-6815:68)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6829:33-6829:81)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6837:29-6837:63)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6838:29-6838:61)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6839:29-6839:50)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6840:29-6840:88)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6841:29-6841:90)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6844:29-6845:76)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6844:29-6845:76)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6844:29-6845:76)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6934:29-6934:59)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6935:29-6936:59)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6950:33-6950:138)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6950:33-6950:138)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6955:33-6955:134)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6955:33-6955:134)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6964:29-6964:67)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6965:29-6965:83)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6966:29-6966:83)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6967:29-6967:83)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6968:29-6968:79)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6969:29-6969:79)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6970:29-6970:79)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6971:29-6972:59)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6987:33-6987:134)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6987:33-6987:134)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6996:29-6996:58)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6997:29-6997:79)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6998:29-6998:79)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6999:29-6999:79)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7000:29-7000:77)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7001:29-7001:77)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7002:29-7002:77)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7003:29-7004:59)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7029:33-7029:85)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7035:33-7035:67)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7047:29-7047:63)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7048:29-7048:52)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7049:29-7049:53)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7050:29-7050:94)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7051:29-7052:85)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7051:29-7052:85)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7092:33-7092:67)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7101:29-7101:67)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7102:29-7102:85)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7103:29-7103:85)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7104:29-7104:85)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7105:29-7105:84)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7106:29-7106:84)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7107:29-7107:84)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7108:29-7109:59)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7125:33-7125:137)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7125:33-7125:137)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7139:33-7139:89)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7149:33-7149:96)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7163:29-7163:63)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7164:29-7164:52)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7165:29-7165:53)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7166:29-7166:94)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7167:29-7168:85)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7167:29-7168:85)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7212:29-7212:59)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7213:29-7214:59)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7215:29-7215:56)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7216:29-7216:57)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7217:29-7217:57)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7218:29-7218:57)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7219:29-7219:58)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7220:29-7220:58)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7221:29-7221:58)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7235:31-7235:62)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7281:3-7281:29)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7281:3-7281:29)
[Info][Unsound] Unknown value in {&((alloc@sid:3897@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7281:3-7281:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7281:3-7281:29)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3797:11-3797:39)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3818:13-3818:66)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3818:13-3818:66)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3818:13-3818:66)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3818:13-3818:66)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3818:13-3818:66)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7298:7-7298:112)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7298:7-7298:112)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7301:5-7301:36)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7303:5-7303:38)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7306:5-7306:70)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7306:5-7306:70)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7312:7-7312:33)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7312:7-7312:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7312:7-7312:33)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7320:5-7320:53)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7320:5-7320:53)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7320:5-7320:53)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7320:5-7320:53)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7320:5-7320:53)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3800:13-3800:41)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3823:13-3823:66)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3823:13-3823:66)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3823:13-3823:66)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3823:13-3823:66)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3823:13-3823:66)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7389:7-7389:113)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7389:7-7389:113)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7394:5-7394:27)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7413:5-7413:53)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7414:5-7414:41)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7415:5-7415:27)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7416:5-7416:28)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7417:5-7417:56)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7417:5-7417:56)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7418:5-7418:55)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7418:5-7418:55)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7419:5-7419:66)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7419:5-7419:66)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7419:5-7419:66)
[Info][Unsound] Unknown value in {&((alloc@sid:3894@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7419:5-7419:66)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7419:5-7419:66)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8201:7-8201:57)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8201:7-8201:57)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8201:7-8201:57)
[Info][Unsound] Unknown value in {&((alloc@sid:3894@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8201:7-8201:57)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8201:7-8201:57)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7338:5-7338:17)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7339:5-7339:49)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7340:5-7340:52)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7340:5-7340:52)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7341:5-7341:46)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7341:5-7341:46)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7343:5-7343:23)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7344:5-7344:37)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7424:5-7424:57)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7424:5-7424:57)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7424:5-7424:57)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7424:5-7424:57)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7424:5-7424:57)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3828:13-3828:40)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3829:13-3829:64)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3829:13-3829:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3829:13-3829:64)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3829:13-3829:64)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3829:13-3829:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3829:13-3829:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7624:13-7624:48)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7624:13-7624:48)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7624:13-7624:48)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7624:13-7624:48)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7624:13-7624:48)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3621:7-3621:32)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3632:9-3632:55)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3632:9-3632:55)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3632:9-3632:55)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3632:9-3632:55)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3632:9-3632:55)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3198:3-3198:59)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3198:3-3198:59)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3198:3-3198:59)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3198:3-3198:59)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3198:3-3198:59)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7446:3-7446:25)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7465:3-7465:59)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7466:3-7466:31)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7466:3-7466:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7466:3-7466:31)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7467:3-7467:25)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7468:3-7468:26)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7469:3-7469:54)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7469:3-7469:54)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7470:3-7470:53)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7470:3-7470:53)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7471:3-7471:67)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7471:3-7471:67)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7471:3-7471:67)
[Info][Unsound] Unknown value in {&((alloc@sid:3894@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7471:3-7471:67)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7471:3-7471:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8207:9-8207:71)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8207:9-8207:71)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8207:9-8207:71)
[Info][Unsound] Unknown value in {&((alloc@sid:3894@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8207:9-8207:71)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8207:9-8207:71)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7476:5-7476:55)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7476:5-7476:55)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3205:3-3205:30)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3206:3-3206:31)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3207:3-3207:31)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3208:3-3208:31)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3209:3-3209:32)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3210:3-3210:32)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3211:3-3211:32)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3212:7-3212:43)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3221:7-3221:34)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3244:7-3244:42)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3245:7-3245:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3248:7-3248:78)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3248:7-3248:78)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3248:7-3248:78)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3244:7-3244:42)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3245:7-3245:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3248:7-3248:78)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3248:7-3248:78)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3248:7-3248:78)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3232:9-3232:46)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3244:7-3244:42)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3245:7-3245:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3248:7-3248:78)
[Info][Unsound] Unknown value in {&srb} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3248:7-3248:78)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3248:7-3248:78)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3256:7-3256:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3588:3-3588:100)
[Info][Unsound] Unknown address in {&deviceParameterHandle} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3588:3-3588:100)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3588:3-3588:100)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3596:3-3597:66)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3605:3-3605:33)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3635:9-3635:35)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3635:9-3635:35)
[Info][Unsound] Unknown value in {&((alloc@sid:3894@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3635:9-3635:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3635:9-3635:35)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3624:9-3624:35)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3639:13-3639:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3641:11-3641:59)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3641:11-3641:59)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3641:11-3641:59)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3641:11-3641:59)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3641:11-3641:59)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3649:9-3650:56)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119).PagingPathCountEvent} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3649:9-3650:56)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3653:13-3653:57)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3654:15-3654:54)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3668:9-3668:65)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3668:9-3668:65)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3668:9-3668:65)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3668:9-3668:65)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3668:9-3668:65)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3671:15-3671:57)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3673:13-3673:69)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119).PagingPathCount} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3673:13-3673:69)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2685:5-2685:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2685:5-2685:23)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2685:5-2685:23)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2685:5-2685:23)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3677:13-3677:69)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119).PagingPathCount} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3677:13-3677:69)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2688:5-2688:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2688:5-2688:23)
[Warning][Imprecise] Trying to update a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2688:5-2688:23)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2688:5-2688:23)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3680:15-3680:57)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3681:17-3681:56)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3698:9-3698:66)
[Info][Unsound] Unknown value in {&((alloc@sid:3893@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119).PagingPathCountEvent} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3698:9-3698:66)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3699:9-3699:35)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3699:9-3699:35)
[Info][Unsound] Unknown value in {&((alloc@sid:3894@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7563:3-7563:119)[def_exc:3; intervals:[3,3]; enums:{3}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3699:9-3699:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3699:9-3699:35)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3705:9-3705:61)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3705:9-3705:61)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3705:9-3705:61)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3705:9-3705:61)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3705:9-3705:61)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7629:13-7629:50)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7629:13-7629:50)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7629:13-7629:50)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7629:13-7629:50)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7629:13-7629:50)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7509:3-7509:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7512:3-7512:63)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7512:3-7512:63)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7512:3-7512:63)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7512:3-7512:63)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7715:3-7715:18)
[Warning][Deadcode] Function 'MmLockPagableDataSection' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2742:1-2742:59)
[Warning][Deadcode] Function 'CdAudioAddDevice' is uncalled: 80 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2967:1-3157:1)
[Warning][Deadcode] Function 'DriverEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3717:1-3731:1)
[Warning][Deadcode] Function 'NecSupportNeeded' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3732:1-3762:1)
[Warning][Deadcode] Function 'CdAudioReadWrite' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3763:1-3784:1)
[Warning][Deadcode] Function 'CdAudioNECDeviceControl' is uncalled: 293 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3930:1-4477:1)
[Warning][Deadcode] Function 'CdAudioPioneerDeviceControl' is uncalled: 317 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:4478:1-5095:1)
[Warning][Deadcode] Function 'CdAudioDenonDeviceControl' is uncalled: 296 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:5096:1-5643:1)
[Warning][Deadcode] Function 'CdAudioHitachiSendPauseCommand' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:5644:1-5675:1)
[Warning][Deadcode] Function 'CdAudioHitachiDeviceControl' is uncalled: 338 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:5676:1-6269:1)
[Warning][Deadcode] Function 'CdAudioUnload' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7486:1-7492:1)
[Warning][Deadcode] Function 'ExAcquireFastMutex' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7735:1-7741:1)
[Warning][Deadcode] Function 'ExReleaseFastMutex' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7743:1-7749:1)
[Warning][Deadcode] Function 'ExFreePool' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7767:1-7773:1)
[Warning][Deadcode] Function 'ExfInterlockedInsertHeadList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7777:1-7785:1)
[Warning][Deadcode] Function 'ExfInterlockedInsertTailList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7789:1-7797:1)
[Warning][Deadcode] Function 'ExfInterlockedRemoveHeadList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7800:1-7807:1)
[Warning][Deadcode] Function 'IoAllocateMdl' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7811:1-7836:1)
[Warning][Deadcode] Function 'IoAttachDeviceToDeviceStack' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7839:1-7859:1)
[Warning][Deadcode] Function 'IoBuildAsynchronousFsdRequest' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7866:1-7893:1)
[Warning][Deadcode] Function 'IoBuildDeviceIoControlRequest' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7903:1-7931:1)
[Warning][Deadcode] Function 'IoCreateDevice' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7937:1-7964:1)
[Warning][Deadcode] Function 'IoCreateSymbolicLink' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7967:1-7987:1)
[Warning][Deadcode] Function 'IoDeleteDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7989:1-7995:1)
[Warning][Deadcode] Function 'IoDeleteSymbolicLink' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7997:1-8017:1)
[Warning][Deadcode] Function 'IoDetachDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8019:1-8025:1)
[Warning][Deadcode] Function 'IoFreeIrp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8027:1-8033:1)
[Warning][Deadcode] Function 'IoFreeMdl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8035:1-8041:1)
[Warning][Deadcode] Function 'IoGetConfigurationInformation' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8043:1-8052:1)
[Warning][Deadcode] Function 'IoQueryDeviceDescription' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8071:1-8104:1)
[Warning][Deadcode] Function 'IoRegisterDeviceInterface' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8109:1-8132:1)
[Warning][Deadcode] Function 'IoReleaseCancelSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8134:1-8140:1)
[Warning][Deadcode] Function 'IoSetDeviceInterfaceState' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8143:1-8163:1)
[Warning][Deadcode] Function 'IoSetHardErrorOrVerifyDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8165:1-8171:1)
[Warning][Deadcode] Function 'KeAcquireSpinLockRaiseToDpc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8295:1-8301:1)
[Warning][Deadcode] Function 'KeDelayExecutionThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8305:1-8325:1)
[Warning][Deadcode] Function 'KeInitializeEvent' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8328:1-8334:1)
[Warning][Deadcode] Function 'KeInitializeSemaphore' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8337:1-8343:1)
[Warning][Deadcode] Function 'KeInitializeSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8345:1-8351:1)
[Warning][Deadcode] Function 'KeReleaseSemaphore' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8354:1-8361:1)
[Warning][Deadcode] Function 'KfReleaseSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8364:1-8370:1)
[Warning][Deadcode] Function 'MmAllocateContiguousMemory' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8431:1-8457:1)
[Warning][Deadcode] Function 'MmFreeContiguousMemory' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8459:1-8465:1)
[Warning][Deadcode] Function 'MmMapLockedPagesSpecifyCache' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8472:1-8480:1)
[Warning][Deadcode] Function 'MmPageEntireDriver' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8482:1-8488:1)
[Warning][Deadcode] Function 'MmResetDriverPaging' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8490:1-8496:1)
[Warning][Deadcode] Function 'MmUnlockPages' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8498:1-8504:1)
[Warning][Deadcode] Function 'ObReferenceObjectByHandle' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8511:1-8532:1)
[Warning][Deadcode] Function 'ObfDereferenceObject' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8534:1-8540:1)
[Warning][Deadcode] Function 'PoStartNextPowerIrp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8629:1-8635:1)
[Warning][Deadcode] Function 'PsCreateSystemThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8643:1-8665:1)
[Warning][Deadcode] Function 'PsTerminateSystemThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8667:1-8687:1)
[Warning][Deadcode] Function 'RtlAnsiStringToUnicodeString' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8691:1-8713:1)
[Warning][Deadcode] Function 'RtlCompareMemory' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8717:1-8724:1)
[Warning][Deadcode] Function 'RtlCopyUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8727:1-8734:1)
[Warning][Deadcode] Function 'RtlDeleteRegistryValue' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8738:1-8759:1)
[Warning][Deadcode] Function 'RtlFreeUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8761:1-8767:1)
[Warning][Deadcode] Function 'RtlInitString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8770:1-8776:1)
[Warning][Deadcode] Function 'RtlInitUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8779:1-8786:1)
[Warning][Deadcode] Function 'RtlQueryRegistryValues' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8792:1-8814:1)
[Warning][Deadcode] Function 'CdAudio435DeviceControl' has dead code:
  on line 6805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6805-6805)
  on line 6859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6859-6859)
  on line 6862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6862-6862)
  on lines 6864..6865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6864-6865)
  on line 6867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6867-6867)
  on lines 6869..6877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6869-6877)
  on line 6879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6879-6879)
  on line 6881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6881-6881)
  on line 6883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6883-6883)
  on line 6885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6885-6885)
  on lines 6890..6898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6890-6898)
  on lines 6902..6911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6902-6911)
  on lines 6916..6923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6916-6923)
  on lines 6939..6946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6939-6946)
  on lines 6975..6979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6975-6979)
  on lines 7007..7013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7007-7013)
  on line 7016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7016-7016)
  on lines 7063..7070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7063-7070)
  on line 7073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7073-7073)
  on lines 7082..7086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7082-7086)
  on lines 7112..7113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7112-7113)
  on lines 7171..7174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7171-7174)
  on lines 7176..7178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7176-7178)
  on lines 7180..7181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7180-7181)
  on lines 7184..7199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7184-7199)
  on line 7273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7273-7273)
[Warning][Deadcode] Function 'CdAudio535DeviceControl' has dead code:
  on line 6336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6336-6336)
  on line 6382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6382-6382)
  on lines 6385..6389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6385-6389)
  on line 6391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6391-6391)
  on lines 6400..6402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6400-6402)
  on line 6457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6457-6457)
  on line 6460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6460-6460)
  on lines 6462..6463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6462-6463)
  on line 6465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6465-6465)
  on lines 6467..6475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6467-6475)
  on line 6477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6477-6477)
  on line 6479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6479-6479)
  on line 6481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6481-6481)
  on line 6483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6483-6483)
  on lines 6488..6496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6488-6496)
  on lines 6500..6509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6500-6509)
  on line 6514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6514-6514)
  on lines 6572..6573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6572-6573)
  on line 6575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6575-6575)
  on lines 6577..6594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6577-6594)
  on lines 6639..6640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6639-6640)
  on line 6720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6720-6720)
[Warning][Deadcode] Function 'CdAudioAtapiDeviceControl' has dead code:
  on lines 7325..7327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7325-7327)
  on line 7329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7329-7329)
[Warning][Deadcode] Function 'CdAudioDeviceControl' has dead code:
  on line 3805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3805-3805)
[Warning][Deadcode] Function 'CdAudioForwardIrpSynchronous' has dead code:
  on line 7450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7450-7450)
  on line 7455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7455-7455)
[Warning][Deadcode] Function 'CdAudioHPCdrDeviceControl' has dead code:
  on line 7398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7398-7398)
  on line 7403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7403-7403)
  on line 7428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7428-7428)
[Warning][Deadcode] Function 'CdAudioPnp' has dead code:
  on line 3629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3629-3629)
  on line 3714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3714-3714)
[Warning][Deadcode] Function 'CdAudioPower' has dead code:
  on line 7505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7505-7505)
[Warning][Deadcode] Function 'CdAudioSendToNextDriver' has dead code:
  on line 3852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3852-3852)
[Warning][Deadcode] Function 'CdAudioStartDevice' has dead code:
  on lines 3263..3264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3263-3264)
  on line 3266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3266-3266)
  on line 3270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3270-3270)
  on line 3272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3272-3272)
  on lines 3274..3275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3274-3275)
  on line 3282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3282-3282)
  on line 3284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3284-3284)
  on line 3288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3288-3288)
  on line 3290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3290-3290)
  on lines 3294..3295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3294-3295)
  on lines 3299..3307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3299-3307)
  on lines 3309..3310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3309-3310)
  on line 3340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3340-3340)
  on line 3342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3342-3342)
  on lines 3345..3348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3345-3348)
  on lines 3350..3351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3350-3351)
  on lines 3365..3367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3365-3367)
  on line 3370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3370-3370)
  on line 3372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3372-3372)
  on lines 3374..3375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3374-3375)
  on line 3378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3378-3378)
  on lines 3380..3381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3380-3381)
  on line 3384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3384-3384)
  on lines 3386..3387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3386-3387)
  on line 3390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3390-3390)
  on lines 3392..3393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3392-3393)
  on line 3396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3396-3396)
  on lines 3398..3399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3398-3399)
  on line 3420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3420-3420)
  on line 3422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3422-3422)
  on line 3426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3426-3426)
  on line 3428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3428-3428)
  on line 3430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3430-3430)
  on line 3432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3432-3432)
  on lines 3436..3437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3436-3437)
  on lines 3442..3443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3442-3443)
  on line 3448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3448-3448)
  on line 3450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3450-3450)
  on line 3453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3453-3453)
  on line 3455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3455-3455)
  on line 3459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3459-3459)
  on line 3461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3461-3461)
  on lines 3465..3467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3465-3467)
  on line 3473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3473-3473)
  on line 3475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3475-3475)
  on lines 3479..3481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3479-3481)
  on line 3486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3486-3486)
  on line 3488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3488-3488)
  on lines 3491..3497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3491-3497)
  on lines 3499..3501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3499-3501)
  on lines 3523..3528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3523-3528)
  on lines 3530..3532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3530-3532)
  on line 3535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3535-3535)
  on lines 3537..3539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3537-3539)
  on line 3563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3563-3563)
  on line 3565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3565-3565)
  on line 3569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3569-3569)
  on line 3571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3571-3571)
  on lines 3575..3576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3575-3576)
  on line 3591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3591-3591)
[Warning][Deadcode] Function 'HPCdrCompletion' has dead code:
  on lines 7354..7355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7354-7355)
  on line 7358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7358-7358)
  on line 7361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7361-7361)
[Warning][Deadcode] Function 'IofCallDriver' has dead code:
  on line 8225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8225-8225)
  on line 8235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8235-8235)
  on line 8270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8270-8270)
[Warning][Deadcode] Function 'IofCompleteRequest' has dead code:
  on line 8288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8288-8288)
[Warning][Deadcode] Function 'KeWaitForSingleObject' has dead code:
  on lines 8400..8401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8400-8401)
  on line 8405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8405-8405)
  on line 8417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8417-8417)
[Warning][Deadcode] Function 'PoCallDriver' has dead code:
  on line 8553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8553-8553)
  on lines 8555..8556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8555-8556)
  on line 8559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8559-8559)
  on lines 8561..8562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8561-8562)
  on line 8568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8568-8568)
  on line 8570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8570-8570)
  on line 8586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8586-8586)
  on lines 8603..8604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8603-8604)
  on lines 8607..8609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8607-8609)
  on lines 8611..8612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8611-8612)
  on line 8620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8620-8620)
[Warning][Deadcode] Function 'SendSrbSynchronous' has dead code:
  on line 2956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2956-2956)
  on lines 2958..2959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2958-2959)
  on line 2964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2964-2964)
[Warning][Deadcode] Function 'ZwClose' has dead code:
  on line 8825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8825-8825)
[Warning][Deadcode] Function 'errorFn' has dead code:
  on line 2849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2849-2849)
[Warning][Deadcode] Function 'main' has dead code:
  on line 7601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7601-7601)
  on line 7616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7616-7616)
  on lines 7652..7653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7652-7653)
  on lines 7660..7661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7660-7661)
  on line 7677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7677-7677)
  on line 7688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7688-7688)
  on line 7690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7690-7690)
[Warning][Deadcode] Function 'stubMoreProcessingRequired' has dead code:
  on line 8180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8180-8180)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 714
  dead: 1893 (1545 in uncalled functions)
  total: 2607
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8176:7-8176:14)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CDROM_TOC )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7573:7-7573:41)
[Warning][Deadcode][CWE-571] condition '! irp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:2951:7-2951:12)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(IO_STACK_LOCATION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7571:7-7571:49)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7054:33-7054:49)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CDROM_TOC )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7573:7-7573:41)
[Warning][Deadcode][CWE-571] condition 'status' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7474:7-7474:13)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(IO_STACK_LOCATION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7571:7-7571:49)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6445:29-6445:45)
[Warning][Deadcode][CWE-571] condition 'status != -1073741764L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6446:31-6446:53)
[Warning][Deadcode][CWE-571] condition 'status != -1073741764L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6447:33-6447:55)
[Warning][Deadcode][CWE-571] condition 'routine == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8205:11-8205:23)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6571:29-6571:41)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7501:7-7501:14)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3228:12-3228:13)
[Warning][Deadcode][CWE-570] condition 'status == -2147483626L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7270:7-7270:29)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(IO_STACK_LOCATION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7571:7-7571:49)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3230:11-3230:27)
[Warning][Deadcode][CWE-570] condition 'myIrp_PendingReturned' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8224:7-8224:28)
[Warning][Deadcode][CWE-571] condition '(int )tmp___0 < 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3233:13-3233:24)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(IO_STACK_LOCATION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7571:7-7571:49)
[Warning][Deadcode][CWE-570] condition 'compRegistered' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8552:7-8552:21)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(IO_STACK_LOCATION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7571:7-7571:49)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3228:12-3228:13)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7308:9-7308:25)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7111:33-7111:45)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3230:11-3230:27)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(IO_STACK_LOCATION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7571:7-7571:49)
[Warning][Deadcode][CWE-570] condition '! (status >= 0L)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7600:9-7600:25)
[Warning][Deadcode][CWE-571] condition '(int )tmp___0 < 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3233:13-3233:24)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6938:33-6938:45)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(IO_STACK_LOCATION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7571:7-7571:49)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8265:11-8265:21)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CD_DEVICE_EXTENSION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6847:33-6847:49)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8602:7-8602:14)
[Warning][Deadcode][CWE-571] condition 'status != -1073741764L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6848:35-6848:57)
[Warning][Deadcode][CWE-571] condition 'status != -1073741764L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6849:37-6849:59)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(IO_STACK_LOCATION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7571:7-7571:49)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3228:12-3228:13)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8284:7-8284:14)
[Warning][Deadcode][CWE-570] condition 's == MPR1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8606:9-8606:18)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CD_DEVICE_EXTENSION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3230:11-3230:27)
[Warning][Deadcode][CWE-570] condition 'myIrp_PendingReturned' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7353:7-7353:28)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7651:7-7651:18)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8615:11-8615:21)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CD_DEVICE_EXTENSION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6638:29-6638:41)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7659:9-7659:20)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6974:33-6974:45)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7170:33-7170:45)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CD_DEVICE_EXTENSION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)
[Warning][Deadcode][CWE-570] condition 's != DC' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7675:19-7675:26)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CDROM_TOC )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7573:7-7573:41)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3253:9-3253:25)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7687:17-7687:28)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CD_DEVICE_EXTENSION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7396:9-7396:16)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CDROM_TOC )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7573:7-7573:41)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7401:11-7401:30)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6375:29-6375:45)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CD_DEVICE_EXTENSION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8391:9-8391:28)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CDROM_TOC )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7573:7-7573:41)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7006:33-7006:45)
[Warning][Deadcode][CWE-570] condition 'customIrp == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8399:9-8399:23)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CD_DEVICE_EXTENSION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CDROM_TOC )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7573:7-7573:41)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:8403:11-8403:20)
[Warning][Deadcode][CWE-570] condition '! (status >= 0L)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3590:7-3590:23)
[Warning][Deadcode][CWE-570] condition 'status == -1073741808L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7015:35-7015:57)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CD_DEVICE_EXTENSION )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7569:7-7569:51)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CDROM_TOC )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7573:7-7573:41)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:3848:7-3848:14)
[Warning][Deadcode][CWE-570] condition 'status == -2147483626L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:6717:7-6717:29)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7448:7-7448:14)
[Warning][Deadcode][CWE-571] condition '(unsigned long )a < sizeof(CDROM_TOC )' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7573:7-7573:41)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-1.c:7453:9-7453:28)
SV-COMP result: unknown
