Dafny:

* Effectively make all in- and out-parameters of ghost methods ghosts.
* Added DafnyRuntime.cs back in, which is needed to run Dafny programs, but which, unfortunately, is currently not being used in the test suite (something we should address)

1 files changed, 16 insertions, 0 deletions

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index 0e0d3ab3..3e8d1e25 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -104,3 +104,19 @@ method ProcG(g: ClassG) {
   call g.T();  // allowed: intra-module call

   var t := g.TFunc();  // allowed: intra-module call

 }

+

+// ---------------------- some ghost stuff ------------------------

+

+class Ghosty {

+  method Caller() {

+    var x := 3;

+    ghost var y := 3;

+    call Callee(x, y);  // fine

+    call Callee(x, x);  // fine

+    call Callee(y, x);  // error: cannot pass in ghost to a physical formal

+    call Theorem(x);  // fine

+    call Theorem(y);  // fine, because it's a ghost method

+  }

+  method Callee(a: int, ghost b: int) { }

+  ghost method Theorem(a: int) { }

+}