From 5f90de32e39ee691492048c08cb46215d2e9a062 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 7 Oct 2015 17:01:21 -0700
Subject: Renamed ExistentialGuards... to BindingGuards...

---
 Test/dafny0/BindingGuardsResolution.dfy | 154 ++++++++++++++++++++++++++++++++
 1 file changed, 154 insertions(+)
 create mode 100644 Test/dafny0/BindingGuardsResolution.dfy

(limited to 'Test/dafny0/BindingGuardsResolution.dfy')

diff --git a/Test/dafny0/BindingGuardsResolution.dfy b/Test/dafny0/BindingGuardsResolution.dfy
new file mode 100644
index 00000000..e2b55a99
--- /dev/null
+++ b/Test/dafny0/BindingGuardsResolution.dfy
@@ -0,0 +1,154 @@
+// RUN: %dafny /dprint:- /env:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate P(n: int)
+
+predicate R(r: real)
+
+method M0()
+{
+  if x :| P(x) {
+    var y := x + 3;
+    var x := true;  // error: 'x' is already declared in this scope
+  }
+}
+
+method M1()
+{
+  if x: int :| P(x) {
+    x := x + 1;  // error: 'x' is an immutable variable
+  }
+}
+
+method M2()
+{
+  var x := true;
+  if x, y :| P(x) && R(y) {  // this declares a new 'x'
+    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;  // error: 'x' is already declared in this scope
+}
+
+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;  // error: 'y' is an immutable variable
+    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 =>
+  }
+}
+
+module TypesNotFullyDetermined {
+  method T0()
+  {
+    if x :| true {  // error: type not entirely resolved
+    }
+  }
+  method T1()
+  {
+    if x :| true {
+      var y := x + 3;
+    }
+  }
+}
+
+module Ghost {
+  predicate P(x: int)  // note, P is ghost
+  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;  // error: not allowed, because the P in the guard makes this a ghost context
+    } else if y :| 0 <= y < 100 && R(y) {
+      z := y;  // error: this is also in a ghost context, because it depends on the P above
+    }
+
+    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;  // error: not allowed, because the P in the guard makes this a ghost context
+    } else if exists y :: 0 <= y < 100 && R(y) {
+      z := 0;  // error: this is also in a ghost context, because it depends on the P above
+    }
+
+    if P(z) {
+      z := 20;  // error: blatant ghost context
+    }
+
+    b := exists y :: 0 <= y < 100 && P(y);  // error: assignment to non-ghost of something that depends on ghost
+    ghost var c;
+    c := exists y :: 0 <= y < 100 && P(y);
+    b := exists y {:myattribute P(y)} :: 0 <= y < 100;
+  }
+}
-- 
cgit v1.2.3