Remove incorrect one-past-end distinction in memOutOfBounds

[sim642]

This addresses the finding from #2017 (comment).

The memOutOfBounds analysis warns about invalid dereferences. Dereferencing one past end is never valid.

While adding the test I discovered so much more wrong about memOutOfBounds which in some cases completely ignores the offset altogether. I found this because initially I had hard time constructing a test where the off-by-one aspect even made a difference.

There's also a whole other rabbit hole that comes up with this test: %p prints the pointer itself (not what it points to), so there's never a need to warn about out of bounds for that because it's not even dereferenced. Thus, the added tests use %s which actually dereferences. However, we don't have an analysis for the format strings, so we won't be able to not warn for %p. Currently the analysis did warn there but for three wrong reasons combined.

This is orthogonal to #2027: the point here is to simplify the existing thing (and make it correct!) such that the refactoring there doesn't need to preserve an artificial and incorrect distinction.

[Copilot]

Pull request overview

This pull request fixes memOutOfBounds’s offset-vs-size comparison so that dereferences at exactly one-past-end are no longer treated as safe, and extends the regression suite to cover one-past-end and beyond-end pointer cases (including implicit dereference contexts like printf arguments).

Changes:

• Remove the special-case distinction between dereference-offset and pointer-offset comparisons by using a single size <= offset out-of-bounds check.
• Update memOutOfBounds call sites to use the unified offset-bounds helper.
• Expand the 36-one-past-pointer.c regression test with multiple buf + k scenarios and expected WARN/NOWARN annotations.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.

File	Description
src/analyses/memOutOfBounds.ml	Unifies offset bound checking to flag one-past-end as out-of-bounds for invalid dereference detection.
tests/regression/74-invalid_deref/36-one-past-pointer.c	Adds regression coverage for one-past-end and beyond-end pointer cases using printf calls.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[sim642]

According to an sv-benchmarks run with level01, 60s and 1GB, this (surprisingly) makes no difference to verdicts. This probably explains why this unnecessary distinction flew under the radar.