vbpf / prevail / 28621240250

86%

push

github

Fix width argument in weak type-store havoc

ArrayDomain::store_type's weak (non-constant index) update called
num_bytes.havoc(lb, ub), but BitsetDomain::havoc's second parameter is a
width, not an upper bound. It therefore marked bytes [lb, lb+ub) non-numeric
instead of [lb, ub), over-clobbering numeric bytes (clamped to the stack
size). This is conservative and cannot accept an unsafe program, but it
loses precision and can cause spurious rejections.

Pass ub - lb as the width, matching the correct sibling calls.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

1 of 1 new or added line in 1 file covered. (100.0%)

9143 of 10573 relevant lines covered (86.47%)

6472055.5 hits per line