diff options
| author |  boehmes <unknown> | 2012-09-27 17:13:42 +0200 |
|---|---|---|
| committer | boehmes <unknown> | 2012-09-27 17:13:42 +0200 |
| commit | 623a87c132abec61b5c74a6a00a7b162073a6a8d (patch) | |
| tree | b95ba791592cf395ce99035715de98578a5519ee /Test/test0 | |
| parent | ed83becd12d7079e6ce2853fbebace20b1e7df5a (diff) | |
Boogie: new syntax for integer division and modulus: use div and mod instead of / and %
Diffstat (limited to 'Test/test0')
| -rw-r--r-- | Test/test0/Answer | 8 | ||||
| -rw-r--r-- | Test/test0/BadLabels1.bpl | 2 | ||||
| -rw-r--r-- | Test/test0/PrettyPrint.bpl | 7 |
3 files changed, 12 insertions, 5 deletions
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;
|