Fixed bug in resolution of illegal programs.

Fixed comments in some test cases.

1 files changed, 15 insertions, 3 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index bc9c4eee..78288b1e 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -541,11 +541,11 @@ module NoTypeArgs1 {
 method LetSuchThat(ghost z: int, n: nat)

 {

   var x: int;

-  x := var y :| y < 0; y;  // fine

+  x := var y :| y < 0; y;  // error: let-such-that not allowed in non-ghost context

 

-  x := var y :| y < z; y;  // error (x2): RHS depends on a ghost (both on the :| expression and on the z variable)

+  x := var y :| y < z; y;  // error (x2): contraint depend on ghost, and let-such-that not allowed in non-ghost context

 

-  x := var w :| w == 2*w; w;

+  x := var w :| w == 2*w; w;  // error: let-such-that not allowed in non-ghost context

   x := var w := 2*w; w;  // error: the 'w' in the RHS of the assignment is not in scope

   ghost var xg := var w :| w == 2*w; w;

 }

@@ -1330,3 +1330,15 @@ module AmbiguousModuleReference {
     }

   }

 }

+

+// --------------------------------------------------

+

+module GhostLet {

+  method M() {

+    var x: int;

+    x := ghost var tmp := 5; tmp;  // error: ghost -> non-ghost

+    x := ghost var tmp := 5; 10;  // fine

+    x := ghost var a0, a1 :| a0 == 0 && a1 == 1; a0 + a1;  // error: ghost -> non-ghost

+    x := ghost var a :| true; 10;  // error: (conservatively) considered ghost -> non-ghost

+  }

+}