-
Notifications
You must be signed in to change notification settings - Fork 28
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Support for Ghost Fields #766
Conversation
I will soon test this out in SCION to make sure that this works with the SCION idioms. I will report the results here. |
I just adapted the SCION code to be accepted by this new PR (viperproject/VerifiedSCION#337). As such, I do NOT have any objections against merging this 🚀. Note that this comment is not a review, I did not look at the code. |
src/main/scala/viper/gobra/frontend/info/implementation/property/Implements.scala
Outdated
Show resolved
Hide resolved
src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM! I would be happy to merge this when the tests go through
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think I found an issue. Please look at that. otherwise, it should be fine. I did not check all tests yet.
src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala
Outdated
Show resolved
Hide resolved
(underlyingType(typ(s.base)), isGhostField) match { | ||
case (_, true) => isGhost // ghost fields are always ghost memory | ||
val isGhostEmbedding = s.path.exists { | ||
case MemberPath.Next(decl) => decl.ghost |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am not super sure whether this is sufficient. Can the path not be longer?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't quite understand. I'm iterating here over the entire field selection's path
src/test/resources/regressions/features/ghost_field/ghost-field-comparison-simple01.gobra
Show resolved
Hide resolved
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
missed something
This PR depends on PRs #747 & #755 and, thus, targets
ghost-field-target-branch
, which corresponds to the branch used in #755.This PR adds ghost fields, i.e., allows the use of
ghost
in front of field declarations. Note that struct embeddings can (so far) not be ghost. While ghost fields work mostly analogously to actual, non-ghost, fields, there are a few restrictions / differences to point out:ghost-field-interface-simple01.gobra
andghost-field-interface-fail01.gobra
)==
) on structs considers only actual fields, i.e., structs are equal modulo ghost fields. To include ghost fields in the comparison, ghost equality (===
) can be used instead (seeghost-field-comparison-simple01.gobra
)ghost-field-map-fail01.gobra
)