Skip to content

Enable creating new objects#417

Open
keyboardDrummer wants to merge 58 commits intomainfrom
remy/allocate
Open

Enable creating new objects#417
keyboardDrummer wants to merge 58 commits intomainfrom
remy/allocate

Conversation

@keyboardDrummer
Copy link
Contributor

@keyboardDrummer keyboardDrummer commented Feb 13, 2026

Changes

  • Fix a bug in SMTEncoder that would cause it to sometimes not emit all used sorts
  • Fix a bug that prevented using impure expressions in opaque bodies
  • Generate a single postcondition for the modifies clauses, instead of one per field in the whole program
  • Simplify how we handle procedures without modifies clauses
  • Enable creating new objects, and make sure these don't count for the modifies clause

Testing

  • Using object creation in T1_MutableFields. Checking that two created objects are not equal.
  • Using object creation in T2_ModifiesClauses. Checking that newly allocated objects can be modified without being in the modifies clause.

@keyboardDrummer keyboardDrummer changed the title Enable creating new object Enable creating new objects Feb 13, 2026
@keyboardDrummer keyboardDrummer marked this pull request as ready for review February 14, 2026 10:55
@keyboardDrummer keyboardDrummer requested a review from a team as a code owner February 14, 2026 10:55
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.

1 participant