Fixed resolution bug where "var x := x" was allowed.

1 files changed, 20 insertions, 0 deletions

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index ca89b08a..143fa579 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -62,6 +62,26 @@ method DuplicateVarName(x: int) returns (y: int)
                // treated like an outermost-scoped local in this regard)

 }

 

+method ScopeTests()

+{

+  var x := x;  // error: the 'x' in the RHS is not in scope

+  var y :| y == y;  // fine, 'y' is in scope in the RHS

+  var z := DuplicateVarName(z);  // error: the 'z' in the RHS is not in scope

+  var w0, w1 := IntTransform(w1), IntTransform(w0);  // errors two

+  var c := new MyClass.Init(null);  // fine

+  var d := new MyClass.Init(c);  // fine

+  var e := new MyClass.Init(e);  // error: the 'e' in the RHS is not in scope

+  e := new MyClass.Init(e);  // fine (no variable is being introduced here)

+  e.c := new MyClass.Init(e);  // also fine

+}

+

+function IntTransform(w: int): int

+

+class MyClass {

+  var c: MyClass;

+  constructor Init(c: MyClass)

+}

+

 // ---------------------

 

 method InitCalls() {