Boogie: new syntax for integer division and modulus: use div and mod instead of / and %

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