Open
Conversation
…ing policies for function calls and assignments
jesyspa
requested changes
Apr 4, 2026
Collaborator
jesyspa
left a comment
There was a problem hiding this comment.
Not ready for review since PR it depends on hasn't been merged yet.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary:
This PR adds support for Kotlin objects to SnaKt and introduces new associated test cases. The translation is identical to the existing encoding of classes with an additional uniqueness constraint on object references.
Context:
SnaKt supports reasoning about classes, but not about objects. However, the reasoning about objects is very similar. Objects are singletons with global access, but the interactions with them are identical to the interactions with individual class instances. Thus, under the assumption that these interactions are correctly implemented for classes, we introduce additional uniqueness encoding for the reference of each objects and reuse the the shared access predicates from classes.
Changes:
Note: The current handling for objects mirrors the handling (non-unique) class references passed to a function, which require the shared-access predicate. We thus treat used object the same as classes which are passed to a function as an argument and for which we do not have any additional information. This allows read, but no write operations.
Tests:
A new test case objects.kt was added.
Note: This PR depends on #92.