summaryrefslogtreecommitdiff
path: root/Test/codeexpr
diff options
context:
space:
mode:
Diffstat (limited to 'Test/codeexpr')
-rw-r--r--Test/codeexpr/CodeExpr0.bpl110
-rw-r--r--Test/codeexpr/CodeExpr1.bpl138
-rw-r--r--Test/codeexpr/CodeExpr2.bpl104
-rw-r--r--Test/codeexpr/codeExprBug.bpl30
-rw-r--r--Test/codeexpr/codeExprBug.bpl.expect4
5 files changed, 193 insertions, 193 deletions
diff --git a/Test/codeexpr/CodeExpr0.bpl b/Test/codeexpr/CodeExpr0.bpl
index 97dd60e7..e6bf584d 100644
--- a/Test/codeexpr/CodeExpr0.bpl
+++ b/Test/codeexpr/CodeExpr0.bpl
@@ -1,55 +1,55 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P()
-{
- assert |{ A: return true; }|;
-}
-
-// ------------
-
-procedure Q()
-{
- assert |{ var x: bool; A: x := true; return x; }|;
-}
-
-procedure R()
-{
- assert |{ var x: bool; A: x := false; return x; }|; // error
-}
-
-procedure S()
-{
- assert |{ var x: bool; A: return x; }|; // error
-}
-
-// ------------
-
-procedure T(x: int, y: int)
- requires |{ var z: bool;
- Start: goto A;
- A: z := false; goto B, C;
- B: assume 0 <= x; goto D;
- C: assume x < 0; goto R;
- D: goto E, F;
- E: assume 0 <= y; z := true; goto R;
- F: assume y < 0; goto R;
- R: return z;
- }|;
-{
- assert 0 <= x + y;
-}
-
-procedure U(x: int, y: int)
- requires |{ var z: bool;
- Start: goto A;
- A: z := false; goto B, C;
- B: assume 0 <= x; goto D;
- C: assume x < 0; goto R;
- D: goto E, F;
- E: assume 0 <= y; z := true; goto R;
- F: assume y < 0; goto R;
- R: return z;
- }|;
-{
- assert x <= y; // error
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure P()
+{
+ assert |{ A: return true; }|;
+}
+
+// ------------
+
+procedure Q()
+{
+ assert |{ var x: bool; A: x := true; return x; }|;
+}
+
+procedure R()
+{
+ assert |{ var x: bool; A: x := false; return x; }|; // error
+}
+
+procedure S()
+{
+ assert |{ var x: bool; A: return x; }|; // error
+}
+
+// ------------
+
+procedure T(x: int, y: int)
+ requires |{ var z: bool;
+ Start: goto A;
+ A: z := false; goto B, C;
+ B: assume 0 <= x; goto D;
+ C: assume x < 0; goto R;
+ D: goto E, F;
+ E: assume 0 <= y; z := true; goto R;
+ F: assume y < 0; goto R;
+ R: return z;
+ }|;
+{
+ assert 0 <= x + y;
+}
+
+procedure U(x: int, y: int)
+ requires |{ var z: bool;
+ Start: goto A;
+ A: z := false; goto B, C;
+ B: assume 0 <= x; goto D;
+ C: assume x < 0; goto R;
+ D: goto E, F;
+ E: assume 0 <= y; z := true; goto R;
+ F: assume y < 0; goto R;
+ R: return z;
+ }|;
+{
+ assert x <= y; // error
+}
diff --git a/Test/codeexpr/CodeExpr1.bpl b/Test/codeexpr/CodeExpr1.bpl
index 4e8faf3f..98e97cdb 100644
--- a/Test/codeexpr/CodeExpr1.bpl
+++ b/Test/codeexpr/CodeExpr1.bpl
@@ -1,69 +1,69 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// ------ the good ------
-
-procedure F(x: int, y: int) returns (z: bool)
- requires x < y;
- ensures z == (x < 3);
-{
- start:
- z := |{ var a : bool, b : bool; B: a := x < 3; return a; }|;
- return;
-}
-
-function r(int): bool;
-
-procedure F'(x: int, y: int) returns (z: bool)
-{
- start:
- assume x < y;
- assume (forall t: int :: x < 3 + t ==> r(t));
- assert r(y);
-}
-
-procedure F''(x: int, y: int) returns (z: bool)
-{
- start:
- assume x < y;
- assume (forall t: int :: |{ var a: bool;
- Start:
- a := x < 3 + t;
- goto X, Y;
- X: assume a; return r(t);
- Y: assume !a; return true;
- }|);
- assert r(y);
-}
-
-// ------ the bad ------
-
-procedure G(x: int, y: int) returns (z: bool)
- requires x < y;
- ensures z == (x < 3);
-{
- start:
- z := |{ var a : bool, b : bool; B: a := x < 3; return !a; }|;
- return; // error: postcondition violation
-}
-
-procedure G'(x: int, y: int) returns (z: bool)
-{
- start:
- assume x < y;
- assume (forall t: int :: x + 3 < t ==> r(t));
- assert r(y); // error
-}
-
-procedure G''(x: int, y: int) returns (z: bool)
-{
- start:
- assume x < y;
- assume (forall t: int :: |{ var a: bool;
- Start:
- a := x + 3 < t;
- goto X, Y;
- X: assume a; return r(t);
- Y: assume !a; return true;
- }|);
- assert r(y); // error
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// ------ the good ------
+
+procedure F(x: int, y: int) returns (z: bool)
+ requires x < y;
+ ensures z == (x < 3);
+{
+ start:
+ z := |{ var a : bool, b : bool; B: a := x < 3; return a; }|;
+ return;
+}
+
+function r(int): bool;
+
+procedure F'(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: x < 3 + t ==> r(t));
+ assert r(y);
+}
+
+procedure F''(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: |{ var a: bool;
+ Start:
+ a := x < 3 + t;
+ goto X, Y;
+ X: assume a; return r(t);
+ Y: assume !a; return true;
+ }|);
+ assert r(y);
+}
+
+// ------ the bad ------
+
+procedure G(x: int, y: int) returns (z: bool)
+ requires x < y;
+ ensures z == (x < 3);
+{
+ start:
+ z := |{ var a : bool, b : bool; B: a := x < 3; return !a; }|;
+ return; // error: postcondition violation
+}
+
+procedure G'(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: x + 3 < t ==> r(t));
+ assert r(y); // error
+}
+
+procedure G''(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: |{ var a: bool;
+ Start:
+ a := x + 3 < t;
+ goto X, Y;
+ X: assume a; return r(t);
+ Y: assume !a; return true;
+ }|);
+ assert r(y); // error
+}
diff --git a/Test/codeexpr/CodeExpr2.bpl b/Test/codeexpr/CodeExpr2.bpl
index 9d8beed7..0edaa8f4 100644
--- a/Test/codeexpr/CodeExpr2.bpl
+++ b/Test/codeexpr/CodeExpr2.bpl
@@ -1,52 +1,52 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type T;
-const zero: T;
-
-function IsProperIndex(i: int, size: int): bool;
-
-procedure P(a: [int]T, n: int)
- requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
-{
- call Q(a, n);
-}
-
-procedure Q(a: [int]T, n: int)
- requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
-{
- call P(a, n);
-}
-
-procedure A(a: [int]T, n: int)
-{
- assert
- (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)
- ==>
- (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
-}
-
-procedure B(a: [int]T, n: int)
-{
- assert
- (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)
- ==>
- (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
-}
-
-procedure C(a: [int]T, n: int)
-{
- Start:
- assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
- goto Next;
- Next:
- assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
-}
-
-procedure D(a: [int]T, n: int)
-{
- Start:
- assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
- goto Next;
- Next:
- assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type T;
+const zero: T;
+
+function IsProperIndex(i: int, size: int): bool;
+
+procedure P(a: [int]T, n: int)
+ requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+{
+ call Q(a, n);
+}
+
+procedure Q(a: [int]T, n: int)
+ requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+{
+ call P(a, n);
+}
+
+procedure A(a: [int]T, n: int)
+{
+ assert
+ (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)
+ ==>
+ (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure B(a: [int]T, n: int)
+{
+ assert
+ (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)
+ ==>
+ (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}
+
+procedure C(a: [int]T, n: int)
+{
+ Start:
+ assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+ goto Next;
+ Next:
+ assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure D(a: [int]T, n: int)
+{
+ Start:
+ assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+ goto Next;
+ Next:
+ assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}
diff --git a/Test/codeexpr/codeExprBug.bpl b/Test/codeexpr/codeExprBug.bpl
index 4eb86789..e1ae938c 100644
--- a/Test/codeexpr/codeExprBug.bpl
+++ b/Test/codeexpr/codeExprBug.bpl
@@ -1,15 +1,15 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure p() returns ($r: int);
- ensures |{ $bb0: return ($r == 1); }|;
-
-implementation p() returns ($x: int)
-{
- $x := 1;
- return;
-}
-
-procedure q()
- ensures |{ var $b: bool; $0: $b := true; goto $1; $1: return $b; }|;
-{
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure p() returns ($r: int);
+ ensures |{ $bb0: return ($r == 1); }|;
+
+implementation p() returns ($x: int)
+{
+ $x := 1;
+ return;
+}
+
+procedure q()
+ ensures |{ var $b: bool; $0: $b := true; goto $1; $1: return $b; }|;
+{
+}
diff --git a/Test/codeexpr/codeExprBug.bpl.expect b/Test/codeexpr/codeExprBug.bpl.expect
index 3de74d3e..41374b00 100644
--- a/Test/codeexpr/codeExprBug.bpl.expect
+++ b/Test/codeexpr/codeExprBug.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 2 verified, 0 errors
+
+Boogie program verifier finished with 2 verified, 0 errors
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 05:48:26 +0000