diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-03 17:49:32 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-03 17:49:32 -0800 |
| commit | 1064110ffe772441d3a438451c5b47c7c4bfaf4b (patch) | |
| tree | a3190fd677b64ebc1c48b10071e3f817539f5f8b /Test/dafny0/ResolutionErrors.dfy | |
| parent | 83ce7ab9e1fe758b9c52b7d11c0050cfe626d6a9 (diff) | |
Dafny: don't allow ghost expressions in print statements
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 8 |
1 files changed, 8 insertions, 0 deletions
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
+}
|