diff options
Diffstat (limited to 'Test/test2/Call.bpl')
-rw-r--r-- | Test/test2/Call.bpl | 124 |
1 files changed, 62 insertions, 62 deletions
diff --git a/Test/test2/Call.bpl b/Test/test2/Call.bpl index bf2690cc..bb67c3dc 100644 --- a/Test/test2/Call.bpl +++ b/Test/test2/Call.bpl @@ -1,62 +1,62 @@ -// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure Bar() returns (barresult: ref);
-
-procedure Foo();
-
-implementation Foo()
-{
- var x: ref;
-
- entry:
- call x := Bar();
- assume x == null;
- call x := Bar();
- assert x == null;
- return;
-
-}
-
-procedure DifferentFormalNames(x: int, y: int) returns (z: int);
- requires x < y;
- ensures z == x;
-
-implementation DifferentFormalNames(x: int, y: int) returns (z: int)
-{
- start:
- assert x < y;
- z := x;
- return;
-}
-
-implementation DifferentFormalNames(y: int, x: int) returns (w: int)
-{
- start:
- goto A, B;
- A:
- assert y < x;
- assume false;
- return;
- B:
- w := y;
- return;
-}
-
-implementation DifferentFormalNames(y: int, x: int) returns (w: int)
-{
- start:
- assert x < y; // error
- w := y;
- return;
-}
-
-implementation DifferentFormalNames(y: int, x: int) returns (w: int)
-{
- start:
- w := x;
- return; // error: postcondition violation
-}
-
-type ref;
-
-const null : ref;
+// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure Bar() returns (barresult: ref); + +procedure Foo(); + +implementation Foo() +{ + var x: ref; + + entry: + call x := Bar(); + assume x == null; + call x := Bar(); + assert x == null; + return; + +} + +procedure DifferentFormalNames(x: int, y: int) returns (z: int); + requires x < y; + ensures z == x; + +implementation DifferentFormalNames(x: int, y: int) returns (z: int) +{ + start: + assert x < y; + z := x; + return; +} + +implementation DifferentFormalNames(y: int, x: int) returns (w: int) +{ + start: + goto A, B; + A: + assert y < x; + assume false; + return; + B: + w := y; + return; +} + +implementation DifferentFormalNames(y: int, x: int) returns (w: int) +{ + start: + assert x < y; // error + w := y; + return; +} + +implementation DifferentFormalNames(y: int, x: int) returns (w: int) +{ + start: + w := x; + return; // error: postcondition violation +} + +type ref; + +const null : ref; |