diff options
Diffstat (limited to 'Test/codeexpr/CodeExpr1.bpl')
-rw-r--r-- | Test/codeexpr/CodeExpr1.bpl | 138 |
1 files changed, 69 insertions, 69 deletions
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 +} |