Initial set of files.

1 files changed, 28 insertions, 0 deletions

diff --git a/Test/test0/WhereParsing0.bpl b/Test/test0/WhereParsing0.bpl
new file mode 100644
index 00000000..84f92741
--- /dev/null
+++ b/Test/test0/WhereParsing0.bpl
@@ -0,0 +1,28 @@
+const x: int;

+

+function R(int) returns (bool);

+function Even(int) returns (bool);

+

+var y: int where R(y);

+var g: int where g == 12;

+

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

+  requires x < 100;

+  modifies g;

+  ensures -100 < y;

+

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

+  requires x < 100;

+  modifies g;

+  ensures (forall t: int where Even(t) :: -100 < y + t) ||  // error: where not allowed in quant

+          (exists t: int where Even(t) :: -100 < y + t);    // error: where not allowed in quant

+{

+  var a: int;

+  var b: int;

+

+  start:

+    a := x;

+    call b := P(a);

+    y := b;

+    return;

+}