diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/test2/Old.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test2/Old.bpl')
| -rw-r--r-- | Test/test2/Old.bpl | 132 |
1 files changed, 132 insertions, 0 deletions
diff --git a/Test/test2/Old.bpl b/Test/test2/Old.bpl new file mode 100644 index 00000000..00f798bc --- /dev/null +++ b/Test/test2/Old.bpl @@ -0,0 +1,132 @@ +var x: int;
+var y: int;
+
+procedure P()
+ modifies x;
+ ensures x == old(x) + 1;
+{
+ start:
+ x := 1 + x;
+ return;
+}
+
+procedure Q();
+ modifies x;
+ ensures x == old(x) + 1;
+
+implementation Q()
+{
+ start:
+ x := 1 + x;
+ return;
+}
+
+procedure R()
+ modifies x;
+ ensures x == old(x) + 1;
+{
+ start:
+ return;
+} // error: does not establish postcondition
+
+procedure Swap()
+ modifies x, y;
+ ensures x == old(y) && y == old(x);
+{
+ var t: int;
+
+ start:
+ goto A, B;
+ A:
+ t := x;
+ x := y;
+ y := t;
+ goto end;
+ B:
+ x := x - y; // x == old(x) - old(y)
+ y := y + x; // y == old(y) + (old(x) - old(y)) == old(x)
+ x := y - x; // x == old(x) - (old(x) - old(y)) == old(y)
+ goto end;
+ end:
+ return;
+}
+
+procedure OutParam0(x: int) returns (y: int)
+ ensures y == x + 1;
+{
+ start:
+ y := x + 1;
+ return;
+}
+
+// OutParam1 is like OutParam0, except that there's now a separate
+// implementation declaration, which means that the specification
+// and body use different AST nodes for the formal parameters. This
+// may make a difference in the various substitutions going on.
+// (Indeed, a previous bug caused OutParam0 to verify but not OutParam1.)
+procedure OutParam1(x: int) returns (y: int);
+ ensures y == x + 1;
+implementation OutParam1(x: int) returns (y: int)
+{
+ start:
+ y := x + 1;
+ return;
+}
+
+var a: [ref]int;
+var b: [ref]int;
+
+procedure SwapElems(o: ref) returns (p: ref)
+ modifies a, b;
+ ensures a[o] == old(b[p]) && b[o] == old(a[p]);
+{
+ var ta: int, tb: int;
+
+ start:
+ goto A, B, C;
+ A:
+ havoc p;
+ goto B, C;
+ B:
+ ta := a[p];
+ tb := b[p];
+ a[o] := tb;
+ b[o] := ta;
+ return;
+ C:
+ assume a[o] == b[o];assume false;
+
+ p := o;
+ return;
+}
+
+
+
+//-------------------------------------------------------------------------
+// Test old in Boogie PL code
+//-------------------------------------------------------------------------
+
+var Global0: int;
+
+// Good
+procedure OldInCode0()
+ requires Global0 >= 0;
+ ensures Global0 <= old(Global0) + 1;
+ modifies Global0;
+{
+ var local0: int;
+
+ start:
+ goto A,B;
+ A:
+ assert Global0 == old(Global0);
+ return;
+
+ B:
+ local0 := Global0 + 1;
+ local0 := local0 - 1;
+ Global0 := old(local0 + 1);
+ return;
+}
+
+type ref;
|