From 1064110ffe772441d3a438451c5b47c7c4bfaf4b Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 3 Jan 2012 17:49:32 -0800
Subject: Dafny: don't allow ghost expressions in print statements

---
 Test/dafny0/Answer               | 3 ++-
 Test/dafny0/ResolutionErrors.dfy | 8 ++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index da1055c8..adc49908 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -493,7 +493,8 @@ ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int
 ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)
 ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
 ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts
-45 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
+46 resolution/type errors detected in ResolutionErrors.dfy
 
 -------------------- ParseErrors.dfy --------------------
 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index e5e56d03..34cfc762 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -309,3 +309,11 @@ method DatatypeDestructors(d: DTD_List) {
       var g1 := d.g;  // error: cannot use ghost member in non-ghost code
   }
 }
+
+// ------------------- print statements ---------------------------------------
+
+method PrintOnlyNonGhosts(a: int, ghost b: int)
+{
+  print "a: ", a, "\n";
+  print "b: ", b, "\n";  // error: print statement cannot take ghosts
+}
-- 
cgit v1.2.3