summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl12
-rw-r--r--Source/Core/AbsyExpr.cs4
-rw-r--r--Source/Core/BoogiePL.atg4
-rw-r--r--Source/Core/Parser.cs4
-rw-r--r--Source/Core/Scanner.cs82
-rw-r--r--Source/Core/Util.cs4
-rw-r--r--Test/livevars/bla1.bpl2
-rw-r--r--Test/livevars/daytona_bug2_ioctl_example_1.bpl2
-rw-r--r--Test/livevars/daytona_bug2_ioctl_example_2.bpl2
-rw-r--r--Test/livevars/stack_overflow.bpl2
-rw-r--r--Test/prover/EQ_v2.Eval__v4.Eval_out.bpl4
-rw-r--r--Test/test0/Answer8
-rw-r--r--Test/test0/BadLabels1.bpl2
-rw-r--r--Test/test0/PrettyPrint.bpl7
-rw-r--r--Test/test2/strings-no-where.bpl20
-rw-r--r--Test/test2/strings-where.bpl20
-rw-r--r--Util/Emacs/boogie-mode.el2
-rw-r--r--Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs7
-rw-r--r--Util/latex/boogie.sty2
-rw-r--r--Util/vim/syntax/boogie.vim2
20 files changed, 98 insertions, 94 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index ca526173..53e8e86a 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -613,15 +613,15 @@ var $Tick: TickType;
// -- Arithmetic -------------------------------------------------
// ---------------------------------------------------------------
-// the connection between % and /
-axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y);
+// the connection between mod and div
+axiom (forall x:int, y:int :: {x mod y} {x div y} x mod y == x - x div y * y);
// remainder is always Euclidean Modulus.
-axiom (forall x:int, y:int :: {x % y} 0 < y ==> 0 <= x % y && x % y < y);
-axiom (forall x:int, y:int :: {x % y} y < 0 ==> 0 <= x % y && x % y < -y);
+axiom (forall x:int, y:int :: {x mod y} 0 < y ==> 0 <= x mod y && x mod y < y);
+axiom (forall x:int, y:int :: {x mod y} y < 0 ==> 0 <= x mod y && x mod y < -y);
-// the following axiom has some unfortunate matching, but it does state a property about % that
+// the following axiom has some unfortunate matching, but it does state a property about mod that
// is sometimes useful
-axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
+axiom (forall a: int, b: int, d: int :: { a mod d, b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b);
// ---------------------------------------------------------------
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index f2ed5790..d2b8506a 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1214,9 +1214,9 @@ namespace Microsoft.Boogie {
case Opcode.Mul:
return "*";
case Opcode.Div:
- return "/";
+ return "div";
case Opcode.Mod:
- return "%";
+ return "mod";
case Opcode.Eq:
return "==";
case Opcode.Neq:
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index a2ad40f6..26b70bd3 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -1171,8 +1171,8 @@ Factor<out Expr/*!*/ e0>
MulOp<out IToken/*!*/ x, out BinaryOperator.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)
( "*" (. x = t; op=BinaryOperator.Opcode.Mul; .)
- | "/" (. x = t; op=BinaryOperator.Opcode.Div; .)
- | "%" (. x = t; op=BinaryOperator.Opcode.Mod; .)
+ | "div" (. x = t; op=BinaryOperator.Opcode.Div; .)
+ | "mod" (. x = t; op=BinaryOperator.Opcode.Mod; .)
)
.
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index e95bccda..8638d9c3 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -2157,8 +2157,8 @@ public class Errors {
case 68: s = "\"++\" expected"; break;
case 69: s = "\"+\" expected"; break;
case 70: s = "\"-\" expected"; break;
- case 71: s = "\"/\" expected"; break;
- case 72: s = "\"%\" expected"; break;
+ case 71: s = "\"div\" expected"; break;
+ case 72: s = "\"mod\" expected"; break;
case 73: s = "\"!\" expected"; break;
case 74: s = "\"\\u00ac\" expected"; break;
case 75: s = "\"false\" expected"; break;
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index cfef86c7..b9f4ec42 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -262,36 +262,34 @@ public class Scanner {
start[59] = 12;
start[40] = 13;
start[41] = 14;
- start[58] = 49;
+ start[58] = 47;
start[44] = 15;
start[91] = 16;
start[93] = 17;
- start[60] = 50;
- start[62] = 51;
+ start[60] = 48;
+ start[62] = 49;
start[123] = 18;
- start[125] = 52;
- start[61] = 53;
+ start[125] = 50;
+ start[61] = 51;
start[42] = 19;
start[8660] = 22;
start[8658] = 24;
start[8656] = 25;
start[38] = 26;
start[8743] = 28;
- start[124] = 54;
+ start[124] = 52;
start[8744] = 30;
- start[33] = 55;
+ start[33] = 53;
start[8800] = 34;
start[8804] = 35;
start[8805] = 36;
- start[43] = 56;
+ start[43] = 54;
start[45] = 38;
- start[47] = 39;
- start[37] = 40;
- start[172] = 41;
- start[8704] = 44;
- start[8707] = 45;
- start[955] = 46;
- start[8226] = 48;
+ start[172] = 39;
+ start[8704] = 42;
+ start[8707] = 43;
+ start[955] = 44;
+ start[8226] = 46;
start[Buffer.EOF] = -1;
}
@@ -519,6 +517,8 @@ public class Scanner {
case "havoc": t.kind = 46; break;
case "call": t.kind = 48; break;
case "forall": t.kind = 49; break;
+ case "div": t.kind = 71; break;
+ case "mod": t.kind = 72; break;
case "false": t.kind = 75; break;
case "true": t.kind = 76; break;
case "old": t.kind = 77; break;
@@ -658,68 +658,64 @@ public class Scanner {
case 38:
{t.kind = 70; break;}
case 39:
- {t.kind = 71; break;}
- case 40:
- {t.kind = 72; break;}
- case 41:
{t.kind = 74; break;}
- case 42:
+ case 40:
{t.kind = 78; break;}
- case 43:
+ case 41:
{t.kind = 79; break;}
- case 44:
+ case 42:
{t.kind = 81; break;}
- case 45:
+ case 43:
{t.kind = 83; break;}
- case 46:
+ case 44:
{t.kind = 85; break;}
- case 47:
+ case 45:
{t.kind = 86; break;}
- case 48:
+ case 46:
{t.kind = 87; break;}
- case 49:
+ case 47:
recEnd = pos; recKind = 10;
if (ch == '=') {AddCh(); goto case 20;}
- else if (ch == ':') {AddCh(); goto case 47;}
+ else if (ch == ':') {AddCh(); goto case 45;}
else {t.kind = 10; break;}
- case 50:
+ case 48:
recEnd = pos; recKind = 17;
- if (ch == '=') {AddCh(); goto case 57;}
+ if (ch == '=') {AddCh(); goto case 55;}
else if (ch == ':') {AddCh(); goto case 33;}
else {t.kind = 17; break;}
- case 51:
+ case 49:
recEnd = pos; recKind = 18;
if (ch == '=') {AddCh(); goto case 31;}
else {t.kind = 18; break;}
- case 52:
+ case 50:
recEnd = pos; recKind = 26;
- if (ch == '|') {AddCh(); goto case 43;}
+ if (ch == '|') {AddCh(); goto case 41;}
else {t.kind = 26; break;}
- case 53:
+ case 51:
recEnd = pos; recKind = 29;
- if (ch == '=') {AddCh(); goto case 58;}
+ if (ch == '=') {AddCh(); goto case 56;}
else {t.kind = 29; break;}
- case 54:
+ case 52:
if (ch == '|') {AddCh(); goto case 29;}
- else if (ch == '{') {AddCh(); goto case 42;}
+ else if (ch == '{') {AddCh(); goto case 40;}
else {goto case 0;}
- case 55:
+ case 53:
recEnd = pos; recKind = 73;
if (ch == '=') {AddCh(); goto case 32;}
else {t.kind = 73; break;}
- case 56:
+ case 54:
recEnd = pos; recKind = 69;
if (ch == '+') {AddCh(); goto case 37;}
else {t.kind = 69; break;}
- case 57:
+ case 55:
recEnd = pos; recKind = 61;
- if (ch == '=') {AddCh(); goto case 59;}
+ if (ch == '=') {AddCh(); goto case 57;}
else {t.kind = 61; break;}
- case 58:
+ case 56:
recEnd = pos; recKind = 60;
if (ch == '>') {AddCh(); goto case 23;}
else {t.kind = 60; break;}
- case 59:
+ case 57:
recEnd = pos; recKind = 54;
if (ch == '>') {AddCh(); goto case 21;}
else {t.kind = 54; break;}
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index a8e12f63..f8b8b82b 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -451,7 +451,7 @@ namespace Microsoft.Boogie {
op = " && ";
break;
case Microsoft.Boogie.BinaryOperator.Opcode.Div:
- op = " / ";
+ op = " div ";
break;
case Microsoft.Boogie.BinaryOperator.Opcode.Eq:
op = " == ";
@@ -475,7 +475,7 @@ namespace Microsoft.Boogie {
op = " < ";
break;
case Microsoft.Boogie.BinaryOperator.Opcode.Mod:
- op = " % ";
+ op = " mod ";
break;
case Microsoft.Boogie.BinaryOperator.Opcode.Mul:
op = " * ";
diff --git a/Test/livevars/bla1.bpl b/Test/livevars/bla1.bpl
index 2854e5df..12ccc44a 100644
--- a/Test/livevars/bla1.bpl
+++ b/Test/livevars/bla1.bpl
@@ -471,7 +471,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y}
function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y}
function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y}
function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y}
-function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y}
+function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y}
function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y}
diff --git a/Test/livevars/daytona_bug2_ioctl_example_1.bpl b/Test/livevars/daytona_bug2_ioctl_example_1.bpl
index 1decba12..ae8ff08c 100644
--- a/Test/livevars/daytona_bug2_ioctl_example_1.bpl
+++ b/Test/livevars/daytona_bug2_ioctl_example_1.bpl
@@ -510,7 +510,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y}
function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y}
function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y}
function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y}
-function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y}
+function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y}
function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y}
diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl b/Test/livevars/daytona_bug2_ioctl_example_2.bpl
index 0b49364b..44e51827 100644
--- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl
+++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl
@@ -521,7 +521,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y}
function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y}
function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y}
function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y}
-function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y}
+function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y}
function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y}
diff --git a/Test/livevars/stack_overflow.bpl b/Test/livevars/stack_overflow.bpl
index 242acd65..fae3e863 100644
--- a/Test/livevars/stack_overflow.bpl
+++ b/Test/livevars/stack_overflow.bpl
@@ -831,7 +831,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y}
function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y}
function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y}
function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y}
-function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y}
+function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y}
function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y}
diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
index e4da94f4..e53e00b4 100644
--- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
+++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
@@ -382,7 +382,7 @@ axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int
axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y);
-axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x / y);
+axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y);
axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y);
@@ -1173,7 +1173,7 @@ axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int
axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y);
-axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x / y);
+axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y);
axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y);
diff --git a/Test/test0/Answer b/Test/test0/Answer
index 51a139b7..d57e7647 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -48,9 +48,13 @@ axiom x * y * z == x * y * z;
axiom x * y * z * x == x * y * z;
-axiom x / y / z == x / (y / z);
+axiom x div y div z == x div (y div z);
-axiom x / y / (z / x) == x / y / z;
+axiom x div y div (z div x) == x div y div z;
+
+axiom x + y mod z == y mod z + x;
+
+axiom (x + y) mod z == x mod z + y mod z;
axiom x - y - z == x - (y - z);
diff --git a/Test/test0/BadLabels1.bpl b/Test/test0/BadLabels1.bpl
index 28fb47b8..c040ce26 100644
--- a/Test/test0/BadLabels1.bpl
+++ b/Test/test0/BadLabels1.bpl
@@ -28,7 +28,7 @@ procedure P1(y: int)
{
K:
goto A;
- if (y % 2 == 0) {
+ if (y mod 2 == 0) {
goto L;
M:
}
diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl
index a1f941d8..955faad8 100644
--- a/Test/test0/PrettyPrint.bpl
+++ b/Test/test0/PrettyPrint.bpl
@@ -11,8 +11,11 @@ axiom (x * y) + z == (x + y) * z;
axiom x * y * z == (x * (y * z));
axiom (x * y) * (z * x) == (x * y) * z;
-axiom x / y / z == (x / (y / z));
-axiom (x / y) / (z / x) == (x / y) / z;
+axiom x div y div z == (x div (y div z));
+axiom (x div y) div (z div x) == (x div y) div z;
+
+axiom x + y mod z == ((y mod z) + x);
+axiom (x + y) mod z == (x mod z) + (y mod z);
axiom x - y - z == (x - (y - z));
axiom (x - y) - (z - x) == (x - y) - z;
diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl
index ff723db2..c8ef88c8 100644
--- a/Test/test2/strings-no-where.bpl
+++ b/Test/test2/strings-no-where.bpl
@@ -330,23 +330,23 @@ function #shl(int, int) returns (int);
function #shr(int, int) returns (int);
-axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y);
+axiom (forall x: int, y: int :: { x mod y } { x div y } x mod y == x - x div y * y);
-axiom (forall x: int, y: int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y);
+axiom (forall x: int, y: int :: { x mod y } 0 <= x && 0 < y ==> 0 <= x mod y && x mod y < y);
-axiom (forall x: int, y: int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y);
+axiom (forall x: int, y: int :: { x mod y } 0 <= x && y < 0 ==> 0 <= x mod y && x mod y < 0 - y);
-axiom (forall x: int, y: int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0);
+axiom (forall x: int, y: int :: { x mod y } x <= 0 && 0 < y ==> 0 - y < x mod y && x mod y <= 0);
-axiom (forall x: int, y: int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0);
+axiom (forall x: int, y: int :: { x mod y } x <= 0 && y < 0 ==> y < x mod y && x mod y <= 0);
-axiom (forall x: int, y: int :: { (x + y) % y } 0 <= x && 0 <= y ==> (x + y) % y == x % y);
+axiom (forall x: int, y: int :: { (x + y) mod y } 0 <= x && 0 <= y ==> (x + y) mod y == x mod y);
-axiom (forall x: int, y: int :: { (y + x) % y } 0 <= x && 0 <= y ==> (y + x) % y == x % y);
+axiom (forall x: int, y: int :: { (y + x) mod y } 0 <= x && 0 <= y ==> (y + x) mod y == x mod y);
-axiom (forall x: int, y: int :: { (x - y) % y } 0 <= x - y && 0 <= y ==> (x - y) % y == x % y);
+axiom (forall x: int, y: int :: { (x - y) mod y } 0 <= x - y && 0 <= y ==> (x - y) mod y == x mod y);
-axiom (forall a: int, b: int, d: int :: { a % d,b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
+axiom (forall a: int, b: int, d: int :: { a mod d,b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b);
axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i);
@@ -354,7 +354,7 @@ axiom (forall i: int, j: int :: 0 <= j ==> #shl(i, j + 1) == #shl(i, j) * 2);
axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i);
-axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) / 2);
+axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) div 2);
const unique $UnknownRef: ref;
diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl
index da529b84..05e392cb 100644
--- a/Test/test2/strings-where.bpl
+++ b/Test/test2/strings-where.bpl
@@ -330,23 +330,23 @@ function #shl(int, int) returns (int);
function #shr(int, int) returns (int);
-axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y);
+axiom (forall x: int, y: int :: { x mod y } { x div y } x mod y == x - x div y * y);
-axiom (forall x: int, y: int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y);
+axiom (forall x: int, y: int :: { x mod y } 0 <= x && 0 < y ==> 0 <= x mod y && x mod y < y);
-axiom (forall x: int, y: int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y);
+axiom (forall x: int, y: int :: { x mod y } 0 <= x && y < 0 ==> 0 <= x mod y && x mod y < 0 - y);
-axiom (forall x: int, y: int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0);
+axiom (forall x: int, y: int :: { x mod y } x <= 0 && 0 < y ==> 0 - y < x mod y && x mod y <= 0);
-axiom (forall x: int, y: int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0);
+axiom (forall x: int, y: int :: { x mod y } x <= 0 && y < 0 ==> y < x mod y && x mod y <= 0);
-axiom (forall x: int, y: int :: { (x + y) % y } 0 <= x && 0 <= y ==> (x + y) % y == x % y);
+axiom (forall x: int, y: int :: { (x + y) mod y } 0 <= x && 0 <= y ==> (x + y) mod y == x mod y);
-axiom (forall x: int, y: int :: { (y + x) % y } 0 <= x && 0 <= y ==> (y + x) % y == x % y);
+axiom (forall x: int, y: int :: { (y + x) mod y } 0 <= x && 0 <= y ==> (y + x) mod y == x mod y);
-axiom (forall x: int, y: int :: { (x - y) % y } 0 <= x - y && 0 <= y ==> (x - y) % y == x % y);
+axiom (forall x: int, y: int :: { (x - y) mod y } 0 <= x - y && 0 <= y ==> (x - y) mod y == x mod y);
-axiom (forall a: int, b: int, d: int :: { a % d,b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
+axiom (forall a: int, b: int, d: int :: { a mod d,b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b);
axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i);
@@ -354,7 +354,7 @@ axiom (forall i: int, j: int :: 0 <= j ==> #shl(i, j + 1) == #shl(i, j) * 2);
axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i);
-axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) / 2);
+axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) div 2);
const unique $UnknownRef: ref;
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 05:11:37 +0000