From 9fcb57c00fd690da3a86dbc890bc32f6fc352079 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Sun, 5 Jan 2014 15:28:15 -0800
Subject: Added ghost let expressions.

---
 Test/dafny0/Answer               |  8 ++++++--
 Test/dafny0/Compilation.dfy      | 37 ++++++++++++++++++++++++++++++++++++
 Test/dafny0/ResolutionErrors.dfy | 41 ++++++++++++++++++++++++++++++++++++++++
 3 files changed, 84 insertions(+), 2 deletions(-)

(limited to 'Test/dafny0')

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)
+  }
+}
-- 
cgit v1.2.3