1 files changed, 183 insertions, 0 deletions
diff --git a/Test/dafny0/BindingGuards.dfy.expect b/Test/dafny0/BindingGuards.dfy.expect
new file mode 100644
index 00000000..b7da7b9e
--- /dev/null
+++ b/Test/dafny0/BindingGuards.dfy.expect
@@ -0,0 +1,183 @@
+// BindingGuards.dfy
+
+predicate P(n: int)
+{
+  n % 2 == 0
+}
+
+predicate R(r: real)
+{
+  0.0 <= r
+}
+
+method M0()
+{
+  if x :| P(x) {
+    var y := x + 3;
+  }
+}
+
+method M1()
+{
+  if x: int :| P(x) {
+  }
+}
+
+method M2()
+{
+  var x := true;
+  if x, y :| P(x) && R(y) {
+    var z := x + 12;
+  }
+  x := x && false;
+}
+
+method M3()
+{
+  var x := true;
+  if x: int, y :| P(x) && R(y) {
+    var z := x + y.Trunc;
+    var w := real(x) + y;
+  }
+}
+
+method M4()
+{
+  if x, y: real :| P(x) && R(y) {
+  }
+}
+
+method M5()
+{
+  if x: int, y: real :| P(x) && R(y) {
+  }
+}
+
+method M6()
+{
+  if x {:myattribute x, "hello"} :| P(x) {
+  }
+  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
+  }
+  if x: int {:myattribute x, "chello"} :| P(x) {
+  }
+  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
+  }
+}
+
+ghost method M7() returns (z: real, w: real)
+  ensures -2.0 <= z
+  ensures z == w
+{
+  var k;
+  if x :| P(x) {
+    k, z := 4, 18.0;
+  } else if * {
+    z := z + -z;
+  } else if y :| R(y) {
+    z := y;
+  } else if y :| P(y) {
+    k := y;
+  } else {
+    z :| R(z);
+  }
+  if P(k) {
+    z := 18.0;
+  }
+}
+
+ghost method M8(m: int, n: int)
+  requires forall y :: m <= y < n ==> P(y)
+{
+  var t := -1;
+  var u;
+  if y :| m <= y < n && P(y) {
+    u := y;
+    if * {
+      t := n - y;
+    } else if * {
+      t := y - m;
+    } else if P(y) {
+      t := 8;
+    } else {
+      t := -100;
+    }
+  }
+  if t < 0 && m < n {
+    assert P(m) && !P(m);
+    assert false;
+  }
+  assert t < 0 ==> n <= m;
+}
+
+method P0(m: int, n: int)
+  requires m < n
+{
+  ghost var even, alsoEven := 4, 8;
+  if {
+    case x :| P(x) =>
+      even := x;
+    case x: int :| P(x) =>
+      even := x;
+    case x, y :| P(x) && R(y) =>
+      even, alsoEven := x, y.Trunc;
+    case x: int, y :| P(x) && R(y) =>
+      even := x;
+    case m < n =>
+    case x, y: real :| P(x) && R(y) =>
+      even := x;
+    case x: int, y: real :| P(x) && R(y) =>
+      even := x;
+  }
+  assert P(even);
+  assert P(alsoEven);
+}
+
+method P1(m: int, n: int)
+{
+  if {
+    case x :| m <= x < n && P(x) =>
+  }
+}
+
+method P2(m: int, n: int)
+  requires forall y :: m <= y < n ==> P(y)
+{
+  if {
+    case x :| m <= x < n && P(x) =>
+  }
+}
+
+method P3(m: int, n: int)
+  requires m < n && forall y :: m <= y < n ==> P(y)
+{
+  assert P(m);
+  if {
+    case x :| m <= x < n && P(x) =>
+  }
+}
+BindingGuards.dfy(85,10): Error BP5003: A postcondition might not hold on this return path.
+BindingGuards.dfy(71,12): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+    (0,0): anon12_Then
+    (0,0): anon9
+    (0,0): anon16_Then
+BindingGuards.dfy(134,9): Error: assertion violation
+BindingGuards.dfy(6,8): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon20_Then
+    (0,0): anon21_Then
+    (0,0): anon5
+    (0,0): anon17
+BindingGuards.dfy(139,2): Error: alternative cases fail to cover all possibilties
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+BindingGuards.dfy(147,2): Error: alternative cases fail to cover all possibilties
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+
+Dafny program verifier finished with 24 verified, 4 errors