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 | c7324d3b97252a60aba60cf77bdb64ebb206c6c3 (patch) | |
| tree | 170a2140a88794e28609e20c2b904615c42ad3ac /Test/dafny0 | |
| parent | 8ea7e9e82fef906f1a4727c48a292b8f93e51760 (diff) | |
Dafny: don't allow ghost expressions in print statements
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 3 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 8 |
2 files changed, 10 insertions, 1 deletions
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
+}
|