./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3228:5-3250:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:4169:31-4185:31 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:4646:29-4681:29 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:4738:29-4762:29 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:4771:31-4796:31 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:4819:29-4843:29 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:4912:29-4937:29 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:4974:29-4995:29 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:5252:31-5268:31 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:5840:31-5856:31 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:5901:31-5922:31 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6481:25-6497:25 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6883:29-6899:29 with factor 2
[Info] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7570:3-7570:15)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7570:3-7570:15)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7570:3-7570:15)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7611:13-7611:58)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7611:13-7611:58)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7611:13-7611:58)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7611:13-7611:58)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7611:13-7611:58)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3808:13-3808:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3808:13-3808:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:6694:25-6694:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7724:5-7724:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3891:4-3891:64)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3918:7-3918:52)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:6698:25-6698:77)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:6698:25-6698:77)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3856:3-3856:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3858:3-3858:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3858:3-3858:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:6339:25-6339:64)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6348:29-6348:153)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:6370:25-6370:54)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:6372:25-6373:81)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6407:29-6407:153)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:6415:25-6415:68)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.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-2.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-2.c:6440:25-6440:81)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:6443:25-6443:101)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.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-2.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-2.c:6567:25-6567:94)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:6568:25-6569: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-2.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-2.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-2.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-2.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-2.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-2.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-2.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-2.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-2.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-2.c:6635:25-6636:55)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:6662:25-6662:107)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:6663:25-6663:107)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:6664:25-6664:106)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:6664:25-6664:106)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:6666:25-6667:55)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:6682:25-6683:55)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:6728:3-6728:29)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3813:13-3813:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3813:13-3813:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:7232:29-7232:72)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7242:31-7242:83)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:7242:31-7242:83)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7249:29-7249:81)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:7249:29-7249:81)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6807:33-6807:157)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:6815:29-6815:68)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.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-2.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-2.c:6841:29-6841:90)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.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-2.c:6935:29-6936:59)
[Warning][Imprecise] Trying to update a field, but the union is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.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-2.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-2.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-2.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-2.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-2.c:6971:29-6972: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-2.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-2.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-2.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-2.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-2.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-2.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-2.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-2.c:7003:29-7004: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-2.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-2.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-2.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-2.c:7050:29-7050:94)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7051:29-7052: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-2.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-2.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-2.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-2.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-2.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-2.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-2.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-2.c:7108:29-7109: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-2.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-2.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-2.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-2.c:7166:29-7166:94)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.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-2.c:7213:29-7214:59)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:7281:3-7281:29)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3818:13-3818:66)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3818:13-3818:66)
[Warning][Imprecise] Trying to update a field, but was not given a union (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7306:5-7306:70)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:7312:7-7312:33)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7320:5-7320:53)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:7320:5-7320:53)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3823:13-3823:66)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3823:13-3823:66)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7418:5-7418:55)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7419:5-7419:66)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7419:5-7419:66)
[Info][Unsound] Unknown address in {&(alloc@sid:3512(#0))[3]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7419:5-7419:66)
[Info][Unsound] Unknown value in {&(alloc@sid:3512(#0))[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7419:5-7419:66)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8197:7-8197:57)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8197:7-8197:57)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8197:7-8197:57)
[Info][Unsound] Unknown address in {&(alloc@sid:3512(#0))[3]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8197:7-8197:57)
[Info][Unsound] Unknown value in {&(alloc@sid:3512(#0))[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8197:7-8197:57)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8197:7-8197:57)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7338:5-7338:17)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7340:5-7340:52)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7341:5-7341:46)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7424:5-7424:57)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:7424:5-7424:57)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3829:13-3829:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3829:13-3829:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7616:13-7616:48)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7616:13-7616:48)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7616:13-7616:48)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7616:13-7616:48)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7616:13-7616:48)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3632:9-3632:55)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3632:9-3632:55)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3198:3-3198:59)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3198:3-3198:59)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7466:3-7466:31)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7470:3-7470:53)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7471:3-7471:67)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7471:3-7471:67)
[Info][Unsound] Unknown address in {&(alloc@sid:3512(#0))[3]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7471:3-7471:67)
[Info][Unsound] Unknown value in {&(alloc@sid:3512(#0))[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7471:3-7471:67)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7471:3-7471:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8203:9-8203:71)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8203:9-8203:71)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8203:9-8203:71)
[Info][Unsound] Unknown address in {&(alloc@sid:3512(#0))[3]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8203:9-8203:71)
[Info][Unsound] Unknown value in {&(alloc@sid:3512(#0))[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8203:9-8203:71)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8203:9-8203:71)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8203:9-8203:71)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7476:5-7476:55)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3243:7-3243: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-2.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-2.c:3245:7-3245:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3248:7-3248:78)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3243:7-3243: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-2.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-2.c:3245:7-3245:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3248:7-3248:78)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3232:9-3232:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3243:7-3243: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-2.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-2.c:3245:7-3245:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3248:7-3248:78)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3588:3-3588:100)
[Info][Unsound] Unknown address in {&deviceParameterHandle} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3588:3-3588:100)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3596:3-3597:66)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3605:3-3605:33)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3635:9-3635:35)
[Info][Unsound] Unknown address in {&(alloc@sid:3512(#0))[3]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3635:9-3635:35)
[Info][Unsound] Unknown value in {&(alloc@sid:3512(#0))[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3635:9-3635:35)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3639:13-3639:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3641:11-3641:59)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3641:11-3641:59)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCountEvent points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:136-22:139)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCountEvent points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8383:7-8383:52)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCountEvent points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8383:7-8383:52)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCountEvent points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8415:15-8415:18)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCountEvent points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8417:15-8417:28)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3668:9-3668:65)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3668:9-3668:65)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2686:12-2686:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2686:12-2686:23)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCount points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2686:12-2686:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2686:12-2686:23)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCount points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2686:12-2686:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2689:12-2689:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2689:12-2689:23)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCount points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2689:12-2689:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2689:12-2689:23)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCount points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2689:12-2689:23)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCountEvent points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:26:141-26:144)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCountEvent points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8370:8-8370:37)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCountEvent points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8370:8-8370:37)
[Warning][Unknown] lval (& deviceExtension)->PagingPathCountEvent points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8374:11-8374:13)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3699:9-3699:35)
[Info][Unsound] Unknown address in {&(alloc@sid:3512(#0))[3]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3699:9-3699:35)
[Info][Unsound] Unknown value in {&(alloc@sid:3512(#0))[3]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3699:9-3699:35)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3705:9-3705:61)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:3705:9-3705:61)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7621:13-7621:50)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7621:13-7621:50)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7621:13-7621:50)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7621:13-7621:50)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7621:13-7621:50)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7509:3-7509:65)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7512:3-7512:63)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.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-2.c:7512:3-7512:63)
[Warning][Deadcode] Function 'MmLockPagableDataSection' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2743:1-2743:59)
[Warning][Deadcode] Function 'CdAudioAddDevice' is uncalled: 80 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2967:1-3157:1)
[Warning][Deadcode] Function 'DriverEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3717:1-3731:1)
[Warning][Deadcode] Function 'NecSupportNeeded' is uncalled: 18 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3732:1-3762:1)
[Warning][Deadcode] Function 'CdAudioReadWrite' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3763:1-3784:1)
[Warning][Deadcode] Function 'CdAudioNECDeviceControl' is uncalled: 294 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3930:1-4477:1)
[Warning][Deadcode] Function 'CdAudioPioneerDeviceControl' is uncalled: 318 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:4478:1-5095:1)
[Warning][Deadcode] Function 'CdAudioDenonDeviceControl' is uncalled: 297 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:5096:1-5643:1)
[Warning][Deadcode] Function 'CdAudioHitachiSendPauseCommand' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:5644:1-5675:1)
[Warning][Deadcode] Function 'CdAudioHitachiDeviceControl' is uncalled: 339 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:5676:1-6269:1)
[Warning][Deadcode] Function 'CdAudioUnload' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7486:1-7492:1)
[Warning][Deadcode] Function 'ExAcquireFastMutex' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7731:1-7737:1)
[Warning][Deadcode] Function 'ExReleaseFastMutex' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7739:1-7745:1)
[Warning][Deadcode] Function 'ExFreePool' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7763:1-7769:1)
[Warning][Deadcode] Function 'ExfInterlockedInsertHeadList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7773:1-7781:1)
[Warning][Deadcode] Function 'ExfInterlockedInsertTailList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7785:1-7793:1)
[Warning][Deadcode] Function 'ExfInterlockedRemoveHeadList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7796:1-7803:1)
[Warning][Deadcode] Function 'IoAllocateMdl' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7807:1-7832:1)
[Warning][Deadcode] Function 'IoAttachDeviceToDeviceStack' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7835:1-7855:1)
[Warning][Deadcode] Function 'IoBuildAsynchronousFsdRequest' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7862:1-7889:1)
[Warning][Deadcode] Function 'IoBuildDeviceIoControlRequest' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7899:1-7927:1)
[Warning][Deadcode] Function 'IoCreateDevice' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7933:1-7960:1)
[Warning][Deadcode] Function 'IoCreateSymbolicLink' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7963:1-7983:1)
[Warning][Deadcode] Function 'IoDeleteDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7985:1-7991:1)
[Warning][Deadcode] Function 'IoDeleteSymbolicLink' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7993:1-8013:1)
[Warning][Deadcode] Function 'IoDetachDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8015:1-8021:1)
[Warning][Deadcode] Function 'IoFreeIrp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8023:1-8029:1)
[Warning][Deadcode] Function 'IoFreeMdl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8031:1-8037:1)
[Warning][Deadcode] Function 'IoGetConfigurationInformation' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8039:1-8048:1)
[Warning][Deadcode] Function 'IoQueryDeviceDescription' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8067:1-8100:1)
[Warning][Deadcode] Function 'IoRegisterDeviceInterface' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8105:1-8128:1)
[Warning][Deadcode] Function 'IoReleaseCancelSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8130:1-8136:1)
[Warning][Deadcode] Function 'IoSetDeviceInterfaceState' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8139:1-8159:1)
[Warning][Deadcode] Function 'IoSetHardErrorOrVerifyDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8161:1-8167:1)
[Warning][Deadcode] Function 'KeAcquireSpinLockRaiseToDpc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8291:1-8297:1)
[Warning][Deadcode] Function 'KeDelayExecutionThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8301:1-8321:1)
[Warning][Deadcode] Function 'KeInitializeEvent' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8324:1-8330:1)
[Warning][Deadcode] Function 'KeInitializeSemaphore' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8333:1-8339:1)
[Warning][Deadcode] Function 'KeInitializeSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8341:1-8347:1)
[Warning][Deadcode] Function 'KeReleaseSemaphore' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8350:1-8357:1)
[Warning][Deadcode] Function 'KfReleaseSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8360:1-8366:1)
[Warning][Deadcode] Function 'MmAllocateContiguousMemory' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8427:1-8453:1)
[Warning][Deadcode] Function 'MmFreeContiguousMemory' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8455:1-8461:1)
[Warning][Deadcode] Function 'MmMapLockedPagesSpecifyCache' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8468:1-8476:1)
[Warning][Deadcode] Function 'MmPageEntireDriver' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8478:1-8484:1)
[Warning][Deadcode] Function 'MmResetDriverPaging' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8486:1-8492:1)
[Warning][Deadcode] Function 'MmUnlockPages' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8494:1-8500:1)
[Warning][Deadcode] Function 'ObReferenceObjectByHandle' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8507:1-8528:1)
[Warning][Deadcode] Function 'ObfDereferenceObject' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8530:1-8536:1)
[Warning][Deadcode] Function 'PoStartNextPowerIrp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8625:1-8631:1)
[Warning][Deadcode] Function 'PsCreateSystemThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8639:1-8661:1)
[Warning][Deadcode] Function 'PsTerminateSystemThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8663:1-8683:1)
[Warning][Deadcode] Function 'RtlAnsiStringToUnicodeString' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8687:1-8709:1)
[Warning][Deadcode] Function 'RtlCompareMemory' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8713:1-8720:1)
[Warning][Deadcode] Function 'RtlCopyUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8723:1-8730:1)
[Warning][Deadcode] Function 'RtlDeleteRegistryValue' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8734:1-8755:1)
[Warning][Deadcode] Function 'RtlFreeUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8757:1-8763:1)
[Warning][Deadcode] Function 'RtlInitString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8766:1-8772:1)
[Warning][Deadcode] Function 'RtlInitUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8775:1-8782:1)
[Warning][Deadcode] Function 'RtlQueryRegistryValues' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8788:1-8810:1)
[Warning][Deadcode] Function 'CdAudio435DeviceControl' has dead code:
  on line 6805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6805-6805)
  on line 6859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6859-6859)
  on line 6862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6862-6862)
  on lines 6864..6865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6864-6865)
  on line 6867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6867-6867)
  on lines 6869..6877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6869-6877)
  on line 6879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6879-6879)
  on line 6881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6881-6881)
  on line 6883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6883-6883)
  on line 6885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6885-6885)
  on lines 6890..6898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6890-6898)
  on lines 6902..6911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6902-6911)
  on lines 6916..6923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6916-6923)
  on lines 6939..6946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6939-6946)
  on lines 6975..6979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6975-6979)
  on lines 7007..7013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7007-7013)
  on line 7016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7016-7016)
  on lines 7063..7070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7063-7070)
  on line 7073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7073-7073)
  on lines 7082..7086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7082-7086)
  on lines 7112..7113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7112-7113)
  on lines 7171..7174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7171-7174)
  on lines 7176..7178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7176-7178)
  on lines 7180..7181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7180-7181)
  on lines 7184..7199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7184-7199)
  on line 7273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7273-7273)
[Warning][Deadcode] Function 'CdAudio535DeviceControl' has dead code:
  on line 6336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6336-6336)
  on line 6382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6382-6382)
  on lines 6385..6389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6385-6389)
  on line 6391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6391-6391)
  on lines 6400..6402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6400-6402)
  on line 6457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6457-6457)
  on line 6460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6460-6460)
  on lines 6462..6463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6462-6463)
  on line 6465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6465-6465)
  on lines 6467..6475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6467-6475)
  on line 6477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6477-6477)
  on line 6479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6479-6479)
  on line 6481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6481-6481)
  on line 6483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6483-6483)
  on lines 6488..6496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6488-6496)
  on lines 6500..6509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6500-6509)
  on line 6514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6514-6514)
  on lines 6572..6573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6572-6573)
  on line 6575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6575-6575)
  on lines 6577..6594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6577-6594)
  on lines 6639..6640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6639-6640)
  on line 6720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7325-7327)
  on line 7329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7329-7329)
[Warning][Deadcode] Function 'CdAudioDeviceControl' has dead code:
  on line 3805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3805-3805)
[Warning][Deadcode] Function 'CdAudioForwardIrpSynchronous' has dead code:
  on line 7450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7450-7450)
  on line 7455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7455-7455)
[Warning][Deadcode] Function 'CdAudioHPCdrDeviceControl' has dead code:
  on line 7398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7398-7398)
  on line 7403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7403-7403)
  on line 7428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7428-7428)
[Warning][Deadcode] Function 'CdAudioPnp' has dead code:
  on line 3629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3629-3629)
  on line 3714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3714-3714)
[Warning][Deadcode] Function 'CdAudioPower' has dead code:
  on line 7505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7505-7505)
[Warning][Deadcode] Function 'CdAudioSendToNextDriver' has dead code:
  on line 3852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3263-3264)
  on line 3266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3266-3266)
  on line 3270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3270-3270)
  on line 3272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3272-3272)
  on lines 3274..3275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3274-3275)
  on line 3282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3282-3282)
  on line 3284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3284-3284)
  on line 3288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3288-3288)
  on line 3290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3290-3290)
  on lines 3294..3295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3294-3295)
  on lines 3299..3307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3299-3307)
  on lines 3309..3310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3309-3310)
  on line 3340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3340-3340)
  on line 3342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3342-3342)
  on lines 3345..3348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3345-3348)
  on lines 3350..3351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3350-3351)
  on lines 3365..3367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3365-3367)
  on line 3370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3370-3370)
  on line 3372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3372-3372)
  on lines 3374..3375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3374-3375)
  on line 3378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3378-3378)
  on lines 3380..3381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3380-3381)
  on line 3384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3384-3384)
  on lines 3386..3387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3386-3387)
  on line 3390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3390-3390)
  on lines 3392..3393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3392-3393)
  on line 3396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3396-3396)
  on lines 3398..3399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3398-3399)
  on line 3420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3420-3420)
  on line 3422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3422-3422)
  on line 3426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3426-3426)
  on line 3428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3428-3428)
  on line 3430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3430-3430)
  on line 3432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3432-3432)
  on lines 3436..3437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3436-3437)
  on lines 3442..3443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3442-3443)
  on line 3448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3448-3448)
  on line 3450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3450-3450)
  on line 3453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3453-3453)
  on line 3455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3455-3455)
  on line 3459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3459-3459)
  on line 3461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3461-3461)
  on lines 3465..3467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3465-3467)
  on line 3473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3473-3473)
  on line 3475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3475-3475)
  on lines 3479..3481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3479-3481)
  on line 3486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3486-3486)
  on line 3488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3488-3488)
  on lines 3491..3497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3491-3497)
  on lines 3499..3501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3499-3501)
  on lines 3523..3528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3523-3528)
  on lines 3530..3532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3530-3532)
  on line 3535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3535-3535)
  on lines 3537..3539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3537-3539)
  on line 3563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3563-3563)
  on line 3565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3565-3565)
  on line 3569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3569-3569)
  on line 3571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3571-3571)
  on lines 3575..3576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3575-3576)
[Warning][Deadcode] Function 'HPCdrCompletion' has dead code:
  on lines 7354..7355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7354-7355)
  on line 7358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7358-7358)
  on line 7361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7361-7361)
[Warning][Deadcode] Function 'IofCallDriver' has dead code:
  on line 8221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8221-8221)
  on line 8231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8231-8231)
  on line 8266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8266-8266)
[Warning][Deadcode] Function 'IofCompleteRequest' has dead code:
  on line 8284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8284-8284)
[Warning][Deadcode] Function 'KeWaitForSingleObject' has dead code:
  on lines 8396..8397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8396-8397)
  on line 8401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8401-8401)
  on line 8413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8413-8413)
[Warning][Deadcode] Function 'PoCallDriver' has dead code:
  on line 8549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8549-8549)
  on lines 8551..8552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8551-8552)
  on line 8555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8555-8555)
  on lines 8557..8558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8557-8558)
  on line 8564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8564-8564)
  on line 8566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8566-8566)
  on line 8582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8582-8582)
  on lines 8599..8600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8599-8600)
  on lines 8603..8605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8603-8605)
  on lines 8607..8608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8607-8608)
  on line 8616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8616-8616)
[Warning][Deadcode] Function 'SendSrbSynchronous' has dead code:
  on line 2956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2956-2956)
  on lines 2958..2959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2958-2959)
  on line 2964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2964-2964)
[Warning][Deadcode] Function 'ZwClose' has dead code:
  on line 8821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8821-8821)
[Warning][Deadcode] Function 'errorFn' has dead code:
  on line 2849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2849-2849)
[Warning][Deadcode] Function 'main' has dead code:
  on line 7593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7593-7593)
  on line 7608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7608-7608)
  on lines 7644..7645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7644-7645)
  on lines 7652..7653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7652-7653)
  on line 7669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7669-7669)
  on line 7680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7680-7680)
  on line 7682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7682-7682)
[Warning][Deadcode] Function 'stubMoreProcessingRequired' has dead code:
  on line 8176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8176-8176)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 712
  dead: 1896 (1549 in uncalled functions)
  total lines: 2608
[Warning][Deadcode][CWE-570] condition 'myIrp_PendingReturned' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7353:7-7353:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3230:11-3230:27)
[Warning][Deadcode][CWE-570] condition '! (status >= 0L)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7592:9-7592:25)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:6638:29-6638:41)
[Warning][Deadcode][CWE-571] condition '(int )tmp___0 < 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7170:33-7170:45)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8261:11-8261:21)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8598:7-8598:14)
[Warning][Deadcode][CWE-570] condition 's == MPR1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8602:9-8602:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:8280:7-8280:14)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7396:9-7396:16)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3230:11-3230:27)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7401:11-7401:30)
[Warning][Deadcode][CWE-571] condition '(int )tmp___0 < 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3233:13-3233:24)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8611:11-8611:21)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7643:7-7643:18)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6669:29-6669:45)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6375:29-6375:45)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7651:9-7651:20)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7006:33-7006:45)
[Warning][Deadcode][CWE-570] condition 's != DC' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7667:19-7667:26)
[Warning][Deadcode][CWE-570] condition 'status == -1073741808L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7015:35-7015:57)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:3230:11-3230:27)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7679:17-7679:28)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7448:7-7448:14)
[Warning][Deadcode][CWE-570] condition 'status == -2147483626L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6717:7-6717:29)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7453:9-7453:28)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8387:9-8387:28)
[Warning][Deadcode][CWE-570] condition 'customIrp == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8395:9-8395:23)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3253:9-3253:25)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8399:11-8399:20)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7054:33-7054:49)
[Warning][Deadcode][CWE-571] condition 'status' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7474:7-7474:13)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7501:7-7501:14)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6445:29-6445:45)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6571:29-6571:41)
[Warning][Deadcode][CWE-571] condition 'status != -1073741764L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6446:31-6446:53)
[Warning][Deadcode][CWE-570] condition 'status == -2147483626L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:7270:7-7270:29)
[Warning][Deadcode][CWE-571] condition 'status != -1073741764L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6447:33-6447:55)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8172:7-8172:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:3848:7-3848:14)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:7111:33-7111:45)
[Warning][Deadcode][CWE-571] condition 'routine == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8201:11-8201:23)
[Warning][Deadcode][CWE-570] condition 'status >= 0L' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6938:33-6938:45)
[Warning][Deadcode][CWE-570] condition 'myIrp_PendingReturned' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8220:7-8220:28)
[Warning][Deadcode][CWE-571] condition '! irp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:2951:7-2951:12)
[Warning][Deadcode][CWE-570] condition 'compRegistered' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:8548:7-8548:21)
[Warning][Deadcode][CWE-571] condition '! (status >= 0L)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.c:6847:33-6847:49)
[Warning][Deadcode][CWE-571] condition 'status != -1073741764L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/cdaudio.i.cil-2.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-2.c:6849:37-6849:59)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
