1 files changed, 165 insertions, 0 deletions
diff --git a/Test/dafny0/BindingGuardsResolution.dfy.expect b/Test/dafny0/BindingGuardsResolution.dfy.expect
new file mode 100644
index 00000000..b6f23805
--- /dev/null
+++ b/Test/dafny0/BindingGuardsResolution.dfy.expect
@@ -0,0 +1,165 @@
+// BindingGuardsResolution.dfy
+
+
+module TypesNotFullyDetermined {
+  method T0()
+  {
+    if x :| true {
+    }
+  }
+
+  method T1()
+  {
+    if x :| true {
+      var y := x + 3;
+    }
+  }
+}
+
+module Ghost {
+  predicate P(x: int)
+
+  predicate method R(x: int)
+
+  method M7() returns (z: int, b: bool)
+  {
+    if * {
+      z := z + -z;
+    } else if y :| 1000 <= y < 2000 && R(y) {
+      z := y;
+    } else if y :| 0 <= y < 100 && P(y) {
+      z := y;
+    } else if y :| 0 <= y < 100 && R(y) {
+      z := y;
+    }
+    if * {
+      z := z + -z;
+    } else if exists y :: 1000 <= y < 2000 && R(y) {
+      z := 0;
+    } else if exists y :: 0 <= y < 100 && P(y) {
+      z := 0;
+    } else if exists y :: 0 <= y < 100 && R(y) {
+      z := 0;
+    }
+    if P(z) {
+      z := 20;
+    }
+    b := exists y :: 0 <= y < 100 && P(y);
+    ghost var c;
+    c := exists y :: 0 <= y < 100 && P(y);
+    b := exists y {:myattribute P(y)} :: 0 <= y < 100;
+  }
+}
+predicate P(n: int)
+
+predicate R(r: real)
+
+method M0()
+{
+  if x :| P(x) {
+    var y := x + 3;
+    var x := true;
+  }
+}
+
+method M1()
+{
+  if x: int :| P(x) {
+    x := x + 1;
+  }
+}
+
+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 + int(y);
+    var w := real(x) + y;
+  }
+  var x := 0.0;
+}
+
+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) {
+  }
+}
+
+method M7()
+{
+  if x :| P(x) {
+  } else if * {
+  } else if y :| R(y) {
+  } else if y :| P(y) {
+  }
+}
+
+method P0(m: int, n: int)
+  requires m < n
+{
+  var x := true;
+  if {
+    case x :| P(x) =>
+      var t := 3 * x;
+    case x: int :| P(x) =>
+    case x, y :| P(x) && R(y) =>
+      y := y + 1.0;
+    case x: int, y :| P(x) && R(y) =>
+    case m < n =>
+      x := x || m + 5 == n;
+    case x, y: real :| P(x) && R(y) =>
+    case x: int, y: real :| P(x) && R(y) =>
+  }
+  assert x;
+}
+
+method P1(m: int, n: int)
+  requires m < n
+{
+  if {
+    case x {:myattribute x, "hello"} :| P(x) =>
+    case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>
+    case x: int {:myattribute x, "chello"} :| P(x) =>
+    case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>
+    case m < n =>
+  }
+}
+BindingGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly
+BindingGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+BindingGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x
+BindingGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable
+BindingGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x
+BindingGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable
+11 resolution/type errors detected in BindingGuardsResolution.dfy