Initial set of files.

1 files changed, 15 insertions, 0 deletions

diff --git a/Test/test0/WhereParsing1.bpl b/Test/test0/WhereParsing1.bpl
new file mode 100644
index 00000000..402071bf
--- /dev/null
+++ b/Test/test0/WhereParsing1.bpl
@@ -0,0 +1,15 @@
+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;

+

+function f(a: int, b: int where b < 0)  // error: where not allowed among function parameters

+    returns (bool);