diff options
Diffstat (limited to 'Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs')
| -rw-r--r-- | Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs index 02d14b93..fd7c561d 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs @@ -23,17 +23,17 @@ namespace Demo "bv30", "bv31", "bv32",
"bv64",
"call", "complete", "const",
+ "div",
"else", "ensures", "exists", "extends",
"false", "forall", "free", "function",
"goto",
"havoc",
"if", "implementation", "int", "invariant",
"lambda",
- "modifies",
+ "mod", "modifies",
"old",
"procedure",
- "requires",
- "return", "returns",
+ "real", "requires", "return", "returns",
"then", "true", "type",
"unique",
"var",
@@ -181,7 +181,7 @@ namespace Demo identList.Rule = MakePlusRule(identList, comma, ident);
NewStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LParen + expressionList.Q() + RParen;
NewArrStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LBracket + expressionList.Q() + RBracket;
- BinOp.Rule = ToTerm("+") | "-" | "*" | "/" | "%" | "^" | "&" | "|"
+ BinOp.Rule = ToTerm("+") | "-" | "*" | "div" | "mod" | "^" | "&" | "|"
| "&&" | "||" | "==" | "!=" | greater | less
| ">=" | "<=" | "is"
| "=" | "+=" | "-="
@@ -270,8 +270,7 @@ namespace Demo "modifies" |
"old" |
"procedure" |
- "requires" |
- "return" | "returns" |
+ "real" | "requires" | "return" | "returns" |
"then" | "true" | "type" |
"unique" |
"var" |
@@ -322,7 +321,7 @@ namespace Demo ;
typeDecl.Rule
- = (ToTerm("int") | "bool" | ident)
+ = (ToTerm("int") | "bool" | "real" | ident)
;
fieldDecl.Rule
@@ -376,7 +375,7 @@ namespace Demo #region 5. Operators precedence
RegisterOperators(1, "<==>");
RegisterOperators(2, "+", "-");
- RegisterOperators(3, "*", "/", "%", "!!");
+ RegisterOperators(3, "*", "div", "mod", "!!");
RegisterOperators(4, Associativity.Right, "^");
RegisterOperators(5, "||");
RegisterOperators(6, "&&");
|