Skip to content

Propagate access dependencies for ternary expressions in pure functions#86

Open
AlexFalter wants to merge 7 commits intomainfrom
alex/heap-dependent-verification
Open

Propagate access dependencies for ternary expressions in pure functions#86
AlexFalter wants to merge 7 commits intomainfrom
alex/heap-dependent-verification

Conversation

@AlexFalter
Copy link
Copy Markdown
Collaborator

In this PR we introduce conditional heap-dependent expressions in pure functions. Namely, we extend the already existing model, which passed access dependencies unconditionally, and extend it by a condition. On field access or function usage, instead of encoding an expression as an unconditional access, we create a ternary expression unfolding predicates depending on the condition under which what predicates have to be unfolded. To validate our implementation we have created various test cases

@AlexFalter AlexFalter requested a review from jesyspa March 25, 2026 19:32
Copy link
Copy Markdown
Collaborator

@jesyspa jesyspa left a comment

Choose a reason for hiding this comment

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

I am still quite concerned about this case:

class Box(inner: Box?)
fun f(x: Box?, y: Box?): Box? = (x ?: y)?.inner?.inner

It seems to me like the current approach will not correctly unfold permissions, but maybe I'm missing something.

I'll test it out and get this merged if it's okay - no action needed on your part.

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