Open
Conversation
src/vcy/vcy_parser.mly
Outdated
| | ASSUME e=exp SEMI { loc $startpos $endpos @@ Assume e } | ||
| | HAVOC i=IDENT SEMI { loc $startpos $endpos @@ Havoc i } | ||
| | variant=commute_variant phi=commute_condition | ||
| LBRACE PRE COLON pre=exp blocks=nonempty_list(block) POST COLON post=exp RBRACE |
Collaborator
There was a problem hiding this comment.
Merge this rule with the above rule while making the parsing of the pre/post an Option.
src/vcy/ast.ml
Outdated
| | Assume of exp node | ||
| | Havoc of id | ||
| | Require of exp node | ||
| | GCommute of commute_variant * commute_condition * commute_pre_cond * block node list * commute_post_cond |
Collaborator
There was a problem hiding this comment.
| Commute of commute_variant * commute_condition * block node list * commute_pre_cond option * commute_post_cond option
| end | ||
| | Assume _ | Havoc _ -> | ||
| env, None (* We simply ignore 'assume's and 'havoc's at runtime *) | ||
| (* | GCommute (variant, phi, pre, blocks, post) -> |
Collaborator
There was a problem hiding this comment.
Does GCommute just error on runtime? (Should be fixed if we merge with the Commute case as noted before).
Semantics for pre/post conditions? Do we want those to behave like assumptions/assertions and error if they aren't satisfied?
| | (* empty *) { loc $startpos $endpos @@ [] } | ||
| | ELSE b=block { b } | ||
| | ELSE ifs=if_stmt { loc $startpos $endpos @@ [ ifs ] } | ||
| | ELSE ifs=if_stmt { loc $startpos $endpos @@ [ ifs ] } No newline at end of file |
Collaborator
There was a problem hiding this comment.
Add a trailing endline
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
add pre and post-condition in veracity parser and its translation to Servois spec