Add opaque/reveal to Gobra #715
Merged
Conversation
This file contains 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
dnezam
commented
Feb 5, 2024
src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala
Outdated
Show resolved
Hide resolved
src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala
Show resolved
Hide resolved
src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala
Outdated
Show resolved
Hide resolved
src/test/resources/regressions/features/opaque/opaque-interface-fail1.gobra
Outdated
Show resolved
Hide resolved
src/test/resources/regressions/features/opaque/reveal-closure-fail1.gobra
Outdated
Show resolved
Hide resolved
QUES in question was added as comment on PR.
jcp19
reviewed
Feb 6, 2024
src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala
Outdated
Show resolved
Hide resolved
src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala
Show resolved
Hide resolved
src/test/resources/regressions/features/opaque/opaque-interface-fail1.gobra
Outdated
Show resolved
Hide resolved
src/test/resources/regressions/features/opaque/reveal-closure-fail1.gobra
Outdated
Show resolved
Hide resolved
|
We currently do not have tests for the following errors:
Is that alright? |
That is fine. I think the only thing missing is disallowing marking interface methods with opaque. After this, we can merge the PR |
|
Disallowing marking interfaces with opaque should be line 38-40 in StmtTyping.scala, while the error should be exercised by opaque-interface-fail1.gobra. |
oops, I missed this; sorry! |
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.
Overview
This pull request implement
opaqueandrevealfor functions and methods in Gobra.Similar to the meaning of
opaqueandrevealin Dafny (Dafny's reference), anopaquefunction does not expose its body by default. The programmer can explicitly reveal the body of a function call usingreveal. Please refer to opaque-fac2.gobra and opaque-fac3.gobra for examples.Motivation
Not unnecessarily exposing the body of a pure function and hence reducing the context of the solver may increase proof stability and improve performance. This is something that @jcp19 and I plan to investigate in the context of my practical work.
Implementation
opaqueandrevealare implemented by automatically adding the corresponding annotations on the Viper level.Related pull requests/commits