diff options
Diffstat (limited to 'Util')
| -rw-r--r-- | Util/Emacs/boogie-mode.el | 2 | ||||
| -rw-r--r-- | Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs | 7 | ||||
| -rw-r--r-- | Util/latex/boogie.sty | 2 | ||||
| -rw-r--r-- | Util/vim/syntax/boogie.vim | 2 |
4 files changed, 7 insertions, 6 deletions
diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el index 5b60dcab..86721a74 100644 --- a/Util/Emacs/boogie-mode.el +++ b/Util/Emacs/boogie-mode.el @@ -36,7 +36,7 @@ )) . font-lock-builtin-face)
`(,(boogie-regexp-opt '(
"assert" "assume" "break" "call" "then" "else" "havoc" "if" "goto" "return" "while"
- "old" "forall" "exists" "lambda" "cast"
+ "old" "forall" "exists" "lambda" "cast" "div" "mod"
"false" "true")) . font-lock-keyword-face)
`(,(boogie-regexp-opt '("bool" "int"
"bv0" "bv1" "bv2" "bv3" "bv4" "bv5" "bv6" "bv7" "bv8" "bv9"
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs index 02d14b93..4e38f654 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs @@ -23,13 +23,14 @@ 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",
@@ -181,7 +182,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"
| "=" | "+=" | "-="
@@ -376,7 +377,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, "&&");
diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty index 45eb050d..43336262 100644 --- a/Util/latex/boogie.sty +++ b/Util/latex/boogie.sty @@ -34,7 +34,7 @@ procedure,implementation,
requires,modifies,ensures,free,
% expressions
- false,true,null,old,then,
+ false,true,null,old,then,div,mod,
% statements
assert,assume,havoc,call,if,else,while,invariant,break,return,goto,
},
diff --git a/Util/vim/syntax/boogie.vim b/Util/vim/syntax/boogie.vim index 667a2b8c..673f967e 100644 --- a/Util/vim/syntax/boogie.vim +++ b/Util/vim/syntax/boogie.vim @@ -15,7 +15,7 @@ set cpo&vim " type syn keyword bplType bool int " repeat / condition / label -syn keyword bplExpr forall exists cast returns lambda +syn keyword bplExpr forall exists cast returns lambda div mod syn keyword bplStmt goto return while call else if assert assume havoc then syn keyword bplDecl axiom function procedure type requires ensures modifies unique const var free implementation invariant " user labels |