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

10 files changed, 38 insertions, 31 deletions

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;