Initial set of files.

1 files changed, 62 insertions, 0 deletions

diff --git a/Test/test0/WhereResolution.bpl b/Test/test0/WhereResolution.bpl
new file mode 100644
index 00000000..6b28a035
--- /dev/null
+++ b/Test/test0/WhereResolution.bpl
@@ -0,0 +1,62 @@
+type double;

+

+function R(int) returns (bool);

+function K(double, bool) returns (bool);

+

+var y: int where R(y);

+var g: int where h ==> g == 12;

+var h: bool where g < 100;

+var k: double where K(k, h);

+

+procedure P(x: int where x > 0) returns (y: int where y < 0);

+  requires x < 100;

+  modifies g;

+  ensures -100 < y;

+

+implementation P(xx: int) returns (yy: int)

+{

+  var a: int where a == 10;

+  var b: int where a == b && b < g;

+

+  start:

+    a := xx;

+    call b := P(a);

+    yy := b;

+    return;

+}

+

+procedure Q(w: int where x < w || x > alpha/*error: out-parameter alpha is not in scope*/, x: int where x + w > 0)

+    returns (v: bool where v,

+             y: int where x + y + z < 0,

+             z: int where g == 12,

+             alpha: ref where old(alpha) != null,  // error: cannot use old in where clause

+             beta: ref where (forall r: ref :: r == beta ==> beta == null))

+  requires x < 100;

+  modifies g;

+  ensures -100 < y;

+{

+  var a: int;

+  var b: int;

+

+  start:

+    a := x;

+    call b := P(a);

+    y := b;

+    return;

+}

+

+const SomeConstant: ref;

+

+procedure Cnst(n: ref where n != SomeConstant) returns (SomeConstant: int)

+{

+  var m: ref where m != SomeConstant;

+  var k: int where k != SomeConstant;

+  var r: ref where (forall abc: ref :: abc == SomeConstant);

+  var b: bool;

+  start:

+    b := (forall l: ref :: l == SomeConstant);

+    return;

+}

+

+type ref;

+const null : ref;