diff options
Diffstat (limited to 'Test/codeexpr')
-rw-r--r-- | Test/codeexpr/CodeExpr0.bpl | 110 | ||||
-rw-r--r-- | Test/codeexpr/CodeExpr1.bpl | 138 | ||||
-rw-r--r-- | Test/codeexpr/CodeExpr2.bpl | 104 | ||||
-rw-r--r-- | Test/codeexpr/codeExprBug.bpl | 30 | ||||
-rw-r--r-- | Test/codeexpr/codeExprBug.bpl.expect | 4 |
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 |