Added ghost let expressions.

3 files changed, 84 insertions, 2 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5ef39185..0ce33b47 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -434,6 +434,10 @@ ResolutionErrors.dfy(735,19): Error: a while statement used inside a hint is not
 ResolutionErrors.dfy(760,4): Error: calls to methods with side-effects are not allowed inside a statement expression

 ResolutionErrors.dfy(761,4): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(762,4): Error: wrong number of method result arguments (got 0, expected 1)

+ResolutionErrors.dfy(773,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

+ResolutionErrors.dfy(783,4): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(794,36): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(803,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

 ResolutionErrors.dfy(427,2): Error: More than one default constructor

 ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

@@ -507,7 +511,7 @@ ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts

 ResolutionErrors.dfy(544,18): Error: unresolved identifier: w

 ResolutionErrors.dfy(651,11): Error: lemmas are not allowed to have modifies clauses

-110 resolution/type errors detected in ResolutionErrors.dfy

+114 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -2320,7 +2324,7 @@ Dafny program verifier finished with 9 verified, 6 errors
 

 Dafny program verifier finished with 0 verified, 0 errors

 

-Dafny program verifier finished with 37 verified, 0 errors

+Dafny program verifier finished with 44 verified, 0 errors

 Compiled assembly into Compilation.exe

 

 Dafny program verifier finished with 9 verified, 0 errors

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 734cc3e6..27691178 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -170,3 +170,40 @@ method hidden_test()
   reveal_hidden();

   assert hidden() == 7;

 }

+

+// ----- LetExpr with ghosts and in ghost contexts -----

+

+module GhostLetExpr {

+  method M() {

+    ghost var y;

+    var x;

+    var g := G(x, y);

+    ghost var h := var ta := F(); 5;

+    var j := ghost var tb := F(); 5;

+    assert h == j;

+  }

+

+  function F(): int

+  { 5 }

+

+  function method G(x: int, ghost y: int): int

+  { assert y == y; x }

+

+  datatype Dt = MyRecord(a: int, ghost b: int)

+

+  method P(dt: Dt) {

+    match dt {

+      case MyRecord(aa, bb) =>

+        ghost var z := bb + F();

+        ghost var t0 := var y := z; z + 3;

+        ghost var t1 := ghost var y := z; z + 3;

+        var t2 := ghost var y := z; aa + 3;

+    }

+  }

+

+  function method FM(): int

+  {

+    ghost var xyz := F();

+    G(5, xyz)

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 926f08ae..40963e36 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -763,3 +763,44 @@ module StatementsInExpressions {
     10

   }

 }

+

+module GhostLetExpr {

+  method M() {

+    ghost var y;

+    var x;

+    var g := G(x, y);

+    ghost var h := ghost var ta := F(); 5;

+    var j := var tb := F(); 5;  // error: allowed only if 'tb' were ghost

+    assert h == j;

+  }

+

+  function F(): int

+  { 5 }

+

+  function method G(x: int, ghost y: int): int

+  {

+    assert y == x;

+    y  // error: not allowed in non-ghost context

+  }

+

+  datatype Dt = MyRecord(a: int, ghost b: int)

+

+  method P(dt: Dt) {

+    match dt {

+      case MyRecord(aa, bb) =>

+        ghost var z := aa + F();

+        ghost var t0 := var y := z; z + 3;

+        ghost var t1 := ghost var y := z + bb; y + z + 3;

+        var t2 := ghost var y := z; y + 3;  // error: 'y' can only be used in ghost contexts

+    }

+  }

+

+  function method FM(e: bool): int

+  {

+    if e then

+      G(5, F())

+    else

+      var xyz := F();  // error: 'xyz' needs to be declared ghost to allow this

+      G(5, xyz)

+  }

+}