Closed ArquintL closed 4 months ago
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 (https://github.com/viperproject/VerifiedSCION/pull/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.
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
)