./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/kbfiltr.i.cil-2.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
Collected factors:
functions: 108
functionCalls: 127
loops: 6
loopBreaks: 0
controlFlowStatements: 493
expressions: 2291
instructions: 494
integralVars: (20,163)
arrayVars: (2,1)
pointerVars: (2,188)

Complexity estimates:
File: 3
no thread creation -> disabeling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn"
Total: 33446
Congruence: 8138
Enabled congruence domain.
Widening: 18305
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2427:3-2427:15)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2427:3-2427:15)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2427:3-2427:15)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2427:3-2427:15)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2427:3-2427:15)
[Info][Unsound] Unknown address in {&d} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2429:3-2429:33)
[Info][Unsound] Unknown address in {&u} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2429:3-2429:33)
[Info][Unsound] Unknown address in {&ext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2429:3-2429:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2429:3-2429:33)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1698:9-1698:38)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1702:3-1702:66)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1703:3-1703:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1704:3-1704:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1705:3-1705:51)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1706:3-1706:53)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1707:3-1707:59)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1708:3-1708:49)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1709:4-1709:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1710:3-1710:14)
[Info][Unsound] Unknown address in {&d} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2448:5-2448:47)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2448:5-2448:47)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2448:5-2448:47)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2448:5-2448:47)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2448:5-2448:47)
[Info][Unsound] Unknown address in {&ext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2448:5-2448:47)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2448:5-2448:47)
[Info][Unsound] Unknown address in {&device} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1721:3-1722:36)
[Info][Unsound] Unknown address in {&d} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1721:3-1722:36)
[Info][Unsound] Unknown address in {&ext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1721:3-1722:36)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1721:3-1722:36)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1730:3-1730:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1731:3-1731:63)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1732:3-1732:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1732:3-1732:64)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1732:3-1732:64)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1732:3-1732:64)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1732:3-1732:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1732:3-1732:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1732:3-1732:64)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1732:3-1732:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1733:3-1733:24)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1733:3-1733:24)
[Info][Unsound] Unknown value in {&((alloc@sid:931@tid:Top Threads(#top)), /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2819:7-2819:18)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1733:3-1733:24)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1734:3-1734:20)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1734:3-1734:20)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1734:3-1734:20)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1734:3-1734:20)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1734:3-1734:20)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1734:3-1734:20)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1734:3-1734:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1735:3-1735:26)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1735:3-1735:26)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1736:3-1736:30)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1736:3-1736:30)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1737:3-1737:22)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1737:3-1737:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1738:3-1738:22)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1738:3-1738:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1739:3-1739:26)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1740:3-1740:32)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2479:19-2479:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2479:19-2479:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2479:19-2479:64)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2479:19-2479:64)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2479:19-2479:64)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2479:19-2479:64)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2479:19-2479:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2479:19-2479:64)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2479:19-2479:64)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1777:13-1777:95)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1468:5-1468:23)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1471:5-1471:23)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1808:3-1808:60)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1808:3-1808:60)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1808:3-1808:60)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1808:3-1808:60)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1808:3-1808:60)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1808:3-1808:60)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1808:3-1808:60)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1808:3-1808:60)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1808:3-1808:60)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1827:3-1827:65)
[Info][Unsound] Unknown address in {&stack[def_exc:2; intervals:[2,2]; enums:{2}; congruences:2]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1828:3-1828:84)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1828:3-1828:84)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1828:3-1828:84)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1829:3-1830:27)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1829:3-1830:27)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1829:3-1830:27)
[Info][Unsound] Unknown address in {&stack[def_exc:2; intervals:[2,2]; enums:{2}; congruences:2]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1829:3-1830:27)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1829:3-1830:27)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1829:3-1830:27)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2484:19-2484:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2484:19-2484:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2484:19-2484:64)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2484:19-2484:64)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2484:19-2484:64)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2484:19-2484:64)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2484:19-2484:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2484:19-2484:64)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2484:19-2484:64)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2489:19-2489:58)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2489:19-2489:58)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2489:19-2489:58)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2489:19-2489:58)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2489:19-2489:58)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2489:19-2489:58)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2489:19-2489:58)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2489:19-2489:58)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2489:19-2489:58)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2494:19-2494:56)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2494:19-2494:56)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2494:19-2494:56)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2494:19-2494:56)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2494:19-2494:56)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2494:19-2494:56)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2494:19-2494:56)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2494:19-2494:56)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2494:19-2494:56)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TVoid( const  ),
                                ), Lval(Var(irpSp, NoOffset))), CastE(TNamed(size_t___0, TInt(unsigned int, ), ), CastE(TInt(long, ), AddrOf(Mem(CastE(TPtr(TNamed(IO_STACK_LOCATION, TCompLoop(struct _IO_STACK_LOCATION, _, ), ), ), Const(Int(0,int,0))), Field(CompletionRoutine:TPtr(TFun(TNamed(NTSTATUS, TNamed(LONG, TInt(long, ), ), ), DeviceObject: TNamed(PDEVICE_OBJECT, TPtr(TCompLoop(struct _DEVICE_OBJECT, _, ), ), ), Irp: TNamed(PIRP, TPtr(TCompLoop(struct _IRP, _, ), ), ), Context: TNamed(PVOID, TPtr(TVoid(), ), ), ), ), NoOffset))))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2053:47-2053:128)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2053:47-2053:128)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2053:47-2053:128)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2053:47-2053:128)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2074:47-2074:75)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2074:47-2074:75)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2077:47-2077:98)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2078:47-2078:97)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2079:47-2080:74)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2079:47-2080:74)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2079:47-2080:74)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2079:47-2080:74)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2079:47-2080:74)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2079:47-2080:74)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2079:47-2080:74)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3063:5-3063:57)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3063:5-3063:57)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3063:5-3063:57)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3063:5-3063:57)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3063:5-3063:57)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3063:5-3063:57)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3063:5-3063:57)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2084:49-2085:87)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2084:49-2085:87)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2105:47-2105:73)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2105:47-2105:73)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2105:47-2105:73)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2105:47-2105:73)
[Info][Unsound] Unknown address in {&event} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2105:47-2105:73)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2105:47-2105:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2118:47-2118:109)
[Info][Unsound] Unknown address in {&stack[def_exc:2; intervals:[2,2]; enums:{2}; congruences:2]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2119:47-2119:128)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2119:47-2119:128)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2119:47-2119:128)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2120:47-2121:74)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2120:47-2121:74)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2120:47-2121:74)
[Info][Unsound] Unknown address in {&stack[def_exc:2; intervals:[2,2]; enums:{2}; congruences:2]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2120:47-2121:74)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2120:47-2121:74)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2120:47-2121:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2134:47-2134:109)
[Info][Unsound] Unknown address in {&stack[def_exc:2; intervals:[2,2]; enums:{2}; congruences:2]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2135:47-2135:128)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2135:47-2135:128)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2135:47-2135:128)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2136:47-2136:85)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2136:47-2136:85)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2136:47-2136:85)
[Info][Unsound] Unknown address in {&stack[def_exc:2; intervals:[2,2]; enums:{2}; congruences:2]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2136:47-2136:85)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2136:47-2136:85)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2136:47-2136:85)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2169:47-2169:109)
[Info][Unsound] Unknown address in {&stack[def_exc:2; intervals:[2,2]; enums:{2}; congruences:2]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2170:47-2170:128)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2170:47-2170:128)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2170:47-2170:128)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2171:47-2172:74)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2171:47-2172:74)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2171:47-2172:74)
[Info][Unsound] Unknown address in {&stack[def_exc:2; intervals:[2,2]; enums:{2}; congruences:2]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2171:47-2172:74)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2171:47-2172:74)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2171:47-2172:74)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2499:19-2499:58)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2499:19-2499:58)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2499:19-2499:58)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2499:19-2499:58)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2499:19-2499:58)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2499:19-2499:58)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2499:19-2499:58)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2499:19-2499:58)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2499:19-2499:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2231:17-2231:37)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2260:3-2260:65)
[Info][Unsound] Unknown address in {&stack[def_exc:2; intervals:[2,2]; enums:{2}; congruences:2]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2261:3-2261:84)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2261:3-2261:84)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2261:3-2261:84)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2262:3-2262:46)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2262:3-2262:46)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2262:3-2262:46)
[Info][Unsound] Unknown address in {&stack[def_exc:2; intervals:[2,2]; enums:{2}; congruences:2]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2262:3-2262:46)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2262:3-2262:46)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2262:3-2262:46)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2504:19-2504:64)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2504:19-2504:64)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2504:19-2504:64)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2504:19-2504:64)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2504:19-2504:64)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2504:19-2504:64)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2504:19-2504:64)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2504:19-2504:64)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2504:19-2504:64)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1877:27-1877:109)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1905:23-1905:67)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1905:23-1905:67)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1905:23-1905:67)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1905:23-1905:67)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1905:23-1905:67)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1958:5-1958:31)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1958:5-1958:31)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1958:5-1958:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1958:5-1958:31)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1958:5-1958:31)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1958:5-1958:31)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1958:5-1958:31)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1958:5-1958:31)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1958:5-1958:31)
[Info][Unsound] Unknown value in {&irp} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1965:3-1965:56)
[Info][Unsound] Unknown address in {&irp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1965:3-1965:56)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1965:3-1965:56)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1965:3-1965:56)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1965:3-1965:56)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1965:3-1965:56)
[Info][Unsound] Unknown address in {&stack[def_exc:1; intervals:[1,1]; enums:{1}; congruences:1]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1965:3-1965:56)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1965:3-1965:56)
[Info][Unsound] Unknown address in {&hookkb} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1965:3-1965:56)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1828:3-1828:84)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1828:3-1828:84)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1828:3-1828:84)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1828:3-1828:84)
[Info][Unsound] Unknown address in {&devobj} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1829:3-1830:27)
[Info][Unsound] Unknown value in {&devobj} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1829:3-1830:27)
[Info][Unsound] Unknown address in {&devext} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1829:3-1830:27)
[Info][Unsound] Unknown value in {&devext} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1829:3-1830:27)
[Warning][Deadcode] Function 'KbFilter_InitializationRoutine' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2267:1-2295:1)
[Warning][Deadcode] Function 'KbFilter_IsrHook' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2296:1-2325:1)
[Warning][Deadcode] Function 'KbFilter_ServiceCallback' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2326:1-2341:1)
[Warning][Deadcode] Function 'KbFilter_Unload' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2342:1-2348:1)
[Warning][Deadcode] Function 'ExAcquireFastMutex' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2598:1-2604:1)
[Warning][Deadcode] Function 'ExReleaseFastMutex' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2606:1-2612:1)
[Warning][Deadcode] Function 'ExAllocatePoolWithTag' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2616:1-2628:1)
[Warning][Deadcode] Function 'ExFreePool' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2630:1-2636:1)
[Warning][Deadcode] Function 'ExfInterlockedInsertHeadList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2640:1-2648:1)
[Warning][Deadcode] Function 'ExfInterlockedInsertTailList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2652:1-2660:1)
[Warning][Deadcode] Function 'ExfInterlockedRemoveHeadList' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2663:1-2670:1)
[Warning][Deadcode] Function 'IoAllocateMdl' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2674:1-2699:1)
[Warning][Deadcode] Function 'IoBuildAsynchronousFsdRequest' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2729:1-2756:1)
[Warning][Deadcode] Function 'IoBuildDeviceIoControlRequest' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2766:1-2794:1)
[Warning][Deadcode] Function 'IoCreateSymbolicLink' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2831:1-2851:1)
[Warning][Deadcode] Function 'IoDeleteDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2853:1-2859:1)
[Warning][Deadcode] Function 'IoDeleteSymbolicLink' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2861:1-2881:1)
[Warning][Deadcode] Function 'IoDetachDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2883:1-2889:1)
[Warning][Deadcode] Function 'IoFreeIrp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2891:1-2897:1)
[Warning][Deadcode] Function 'IoFreeMdl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2899:1-2905:1)
[Warning][Deadcode] Function 'IoGetConfigurationInformation' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2907:1-2916:1)
[Warning][Deadcode] Function 'IoQueryDeviceDescription' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2935:1-2968:1)
[Warning][Deadcode] Function 'IoRegisterDeviceInterface' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2973:1-2996:1)
[Warning][Deadcode] Function 'IoReleaseCancelSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2998:1-3004:1)
[Warning][Deadcode] Function 'IoSetDeviceInterfaceState' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3007:1-3027:1)
[Warning][Deadcode] Function 'IoSetHardErrorOrVerifyDevice' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3029:1-3035:1)
[Warning][Deadcode] Function 'KeAcquireSpinLockRaiseToDpc' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3143:1-3149:1)
[Warning][Deadcode] Function 'KeDelayExecutionThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3153:1-3173:1)
[Warning][Deadcode] Function 'KeInitializeEvent' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3176:1-3182:1)
[Warning][Deadcode] Function 'KeInitializeSemaphore' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3185:1-3191:1)
[Warning][Deadcode] Function 'KeInitializeSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3193:1-3199:1)
[Warning][Deadcode] Function 'KeReleaseSemaphore' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3202:1-3209:1)
[Warning][Deadcode] Function 'KfReleaseSpinLock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3212:1-3218:1)
[Warning][Deadcode] Function 'MmAllocateContiguousMemory' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3279:1-3305:1)
[Warning][Deadcode] Function 'MmFreeContiguousMemory' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3307:1-3313:1)
[Warning][Deadcode] Function 'MmMapLockedPagesSpecifyCache' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3320:1-3328:1)
[Warning][Deadcode] Function 'MmPageEntireDriver' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3330:1-3336:1)
[Warning][Deadcode] Function 'MmResetDriverPaging' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3338:1-3344:1)
[Warning][Deadcode] Function 'MmUnlockPages' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3346:1-3352:1)
[Warning][Deadcode] Function 'ObReferenceObjectByHandle' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3359:1-3380:1)
[Warning][Deadcode] Function 'ObfDereferenceObject' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3382:1-3388:1)
[Warning][Deadcode] Function 'PoStartNextPowerIrp' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3465:1-3471:1)
[Warning][Deadcode] Function 'PsCreateSystemThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3479:1-3501:1)
[Warning][Deadcode] Function 'PsTerminateSystemThread' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3503:1-3523:1)
[Warning][Deadcode] Function 'RtlAnsiStringToUnicodeString' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3527:1-3549:1)
[Warning][Deadcode] Function 'RtlCompareMemory' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3553:1-3560:1)
[Warning][Deadcode] Function 'RtlCopyUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3563:1-3570:1)
[Warning][Deadcode] Function 'RtlDeleteRegistryValue' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3574:1-3595:1)
[Warning][Deadcode] Function 'RtlFreeUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3597:1-3603:1)
[Warning][Deadcode] Function 'RtlInitString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3606:1-3612:1)
[Warning][Deadcode] Function 'RtlInitUnicodeString' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3615:1-3622:1)
[Warning][Deadcode] Function 'RtlQueryRegistryValues' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3628:1-3650:1)
[Warning][Deadcode] Function 'ZwClose' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3652:1-3672:1)
[Warning][Deadcode] Function 'IoAttachDeviceToDeviceStack' has dead code:
  on line 2711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2711-2711)
[Warning][Deadcode] Function 'IoCreateDevice' has dead code:
  on line 2812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2812-2812)
[Warning][Deadcode] Function 'IofCallDriver' has dead code:
  on line 3084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3084-3084)
  on lines 3101..3102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3101-3102)
  on line 3118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3118-3118)
[Warning][Deadcode] Function 'KbFilter_DispatchPassThrough' has dead code:
  on line 1823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1823-1823)
[Warning][Deadcode] Function 'KbFilter_PnP' has dead code:
  on line 2048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2048-2048)
  on line 2059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2059-2059)
  on line 2064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2064-2064)
  on line 2114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2114-2114)
  on line 2130 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2130-2130)
  on line 2165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2165-2165)
[Warning][Deadcode] Function 'KbFilter_Power' has dead code:
  on line 2229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2229-2229)
  on line 2256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2256-2256)
[Warning][Deadcode] Function 'KeWaitForSingleObject' has dead code:
  on lines 3248..3249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3248-3249)
  on line 3253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3253-3253)
  on line 3265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3265-3265)
[Warning][Deadcode] Function 'PoCallDriver' has dead code:
  on lines 3401..3402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3401-3402)
  on line 3404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3404-3404)
  on line 3406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3406-3406)
  on line 3422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3422-3422)
  on lines 3439..3440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3439-3440)
  on lines 3443..3445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3443-3445)
  on lines 3447..3448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3447-3448)
  on line 3456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3456-3456)
[Warning][Deadcode] Function 'errorFn' has dead code:
  on line 1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1658-1658)
[Warning][Deadcode] Function 'main' has dead code:
  on line 2476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2476-2476)
  on lines 2530..2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2530-2531)
  on lines 2538..2539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2538-2539)
  on line 2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2564-2564)
  on line 2566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2566-2566)
[Warning][Deadcode] Function 'stubMoreProcessingRequired' has dead code:
  on line 3044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3044-3044)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 380
  dead: 227 (186 in uncalled functions)
  total: 607
[Warning][Deadcode][CWE-571] condition 'status >= 0L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2431:7-2431:19)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3100:7-3100:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2161:51-2161:58)
[Warning][Deadcode][CWE-570] condition 's == NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3438:7-3438:14)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3113:11-3113:21)
[Warning][Deadcode][CWE-570] condition 's == MPR1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3442:9-3442:18)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1775:11-1775:12)
[Warning][Deadcode][CWE-571] condition 's == SKIP1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3451:11-3451:21)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1819:7-1819:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2252:7-2252:14)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2529:7-2529:18)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2537:9-2537:20)
[Warning][Deadcode][CWE-570] condition 's == UNLOADED' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2545:11-2545:24)
[Warning][Deadcode][CWE-570] condition 's != NP' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2057:51-2057:58)
[Warning][Deadcode][CWE-571] condition 'setEventCalled == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3239:9-3239:28)
[Warning][Deadcode][CWE-571] condition 's != IPC' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2552:17-2552:25)
[Warning][Deadcode][CWE-570] condition 'compRegistered != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2062:53-2062:72)
[Warning][Deadcode][CWE-570] condition 'customIrp == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3247:9-3247:23)
[Warning][Deadcode][CWE-570] condition 'pended == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2563:17-2563:28)
[Warning][Deadcode][CWE-570] condition 's == MPR3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3251:11-3251:20)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:1875:25-1875:26)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2110:51-2110:58)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3040:7-3040:14)
[Warning][Deadcode][CWE-571] condition 's == NP' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:2126:51-2126:58)
[Warning][Deadcode][CWE-571] condition '(long )compRetStatus == -1073741802L' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3066:9-3066:45)
[Warning][Deadcode][CWE-570] condition 'compRegistered' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ntdrivers/kbfiltr.i.cil-2.c:3399:7-3399:21)
SV-COMP result: unknown
