Skip to content

Sai/acc syntax addition#94

Open
TheDeveloper101 wants to merge 9 commits intomainfrom
sai/acc-syntax-addition
Open

Sai/acc syntax addition#94
TheDeveloper101 wants to merge 9 commits intomainfrom
sai/acc-syntax-addition

Conversation

@TheDeveloper101
Copy link
Copy Markdown
Collaborator

This PR adds the syntax for acc statements in preconditions, therefore allowing for explicit permissions management as mentioned in #34.

@TheDeveloper101 TheDeveloper101 requested review from The-Ray-Man and jesyspa and removed request for jesyspa April 2, 2026 16:44
Copy link
Copy Markdown
Collaborator

@The-Ray-Man The-Ray-Man left a comment

Choose a reason for hiding this comment

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

I think that goes into a good direction. Made some remarks about error handling.

…ed implementing default full permission for acc statements
@TheDeveloper101
Copy link
Copy Markdown
Collaborator Author

I was able to add in the error handling pretty easily. However, when I am trying to add the default value of acc(x.f) to be full permissions, I am getting a no value for parameter exception even when im able to generate the correct viper. any help would be appreciated

@TheDeveloper101 TheDeveloper101 linked an issue Apr 8, 2026 that may be closed by this pull request
val read : Permission
get() = throw FormverFunctionCalledInRuntimeException("read.get")
val write : Permission
get() = throw FormverFunctionCalledInRuntimeException("write.get")
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

I did not yet work with the Builtins logic yet, but I do not understand why we have the read and write?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

that was because we wanted to be able to embed the read and write parameters, so we needed to add them to the builtins since they’re not functions

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.

Add support for explicit permissions in pre-/postconditions

2 participants