cprover: treat the __CPROVER_allocate side effect like malloc

[tautschnig]

The state encoder special-cases calls to malloc/posix_memalign/realloc by tying the allocation to the current state (update_state(state, lhs, allocate_exprt(state, size, type))), which makes the allocate axioms (live_object, writeable_object, object_size, pointer_offset) apply to the result. The generic __CPROVER_allocate side effect, however, was left as-is during expression evaluation, so an assignment p = __CPROVER_allocate(...) never connected the allocated object to the state. As a result, "pointer safe" properties over a freshly allocated object were spuriously refuted, even though cprover has axioms for ID_allocate. A function merely named malloc (even bodyless) was handled correctly while the same __CPROVER_allocate under any other name was not -- the behavior keyed on the C library name rather than the GOTO primitive.

Handle the __CPROVER_allocate side effect uniformly in evaluate_expr_rec by rewriting it to an allocate_exprt tied to the current state, mirroring the malloc special case. This makes cprover treat the GOTO allocation primitive directly, independent of any C-level allocator name.

Soundness is preserved: safe allocations verify (pointer safe), while out-of-bounds accesses and functional bugs over allocated objects are still refuted.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

This PR fixes a soundness/precision issue in the cprover state encoder where the generic __CPROVER_allocate side effect did not establish dynamic-object liveness, causing spurious failures of “pointer safe” properties on freshly allocated objects. It does so by rewriting ID_allocate side effects during expression evaluation into a state-tied allocate_exprt, matching the existing malloc-family special casing.

Changes:

• Rewrite ID_side_effect / ID_allocate expressions in state_encodingt::evaluate_expr_rec into allocate_exprt(state, size, ptr_type) so allocations are tied to the current state and become live dynamic objects.
• Add a regression test where __CPROVER_allocate should yield successful pointer-safety checks on in-bounds accesses.
• Add a companion regression test ensuring an out-of-bounds access on an allocated object is still refuted (i.e., the fix doesn’t mask safety violations).

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/cprover/state_encoding.cpp	Rewrite ID_allocate side effects into state-tied allocate_exprt to establish liveness uniformly.
regression/cprover/pointers/allocate1.c	New test: in-bounds access after __CPROVER_allocate should be pointer-safe and assertion should succeed.
regression/cprover/pointers/allocate1.desc	Expected output for the new “in-bounds allocation is safe” regression.
regression/cprover/pointers/allocate2.c	New test: out-of-bounds access after __CPROVER_allocate must still be refuted by pointer-safety checks.
regression/cprover/pointers/allocate2.desc	Expected output for the new “OOB still refuted” regression.

---

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

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.84%. Comparing base (7483d0d) to head (f510c0a).
⚠️ Report is 38 commits behind head on develop.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9079      +/-   ##
===========================================
+ Coverage    80.68%   80.84%   +0.15%     
===========================================
  Files         1714     1715       +1     
  Lines       189593   189957     +364     
  Branches        73       73              
===========================================
+ Hits        152979   153562     +583     
+ Misses       36614    36395     -219     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[kroening]

I would have avoided the term "liveness".