Skip to content

Recognize malloc/calloc/realloc in local_bitvector_analysist#8980

Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:local_bitvector_analysis-libc-alloc
Open

Recognize malloc/calloc/realloc in local_bitvector_analysist#8980
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:local_bitvector_analysis-libc-alloc

Conversation

@tautschnig
Copy link
Copy Markdown
Collaborator

Teach local_bitvector_analysis to recognize malloc, calloc, and realloc as returning dynamic heap pointers. This lets goto_check_c generate more precise pointer checks (e.g., using dynamic object bounds instead of generic object bounds).

Impact on array_test_add: 312 -> 308 generated properties.

  • Each commit message has a non-empty body, explaining why the change was made.
  • 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).
  • 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.

Teach local_bitvector_analysis to recognize malloc, calloc, and
realloc as returning dynamic heap pointers. This lets goto_check_c
generate more precise pointer checks (e.g., using dynamic object
bounds instead of generic object bounds).

Impact on array_test_add: 312 -> 308 generated properties.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig tautschnig self-assigned this Apr 27, 2026
Copilot AI review requested due to automatic review settings April 27, 2026 10:51
Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants