diff options
| author |  Rustan Leino <unknown> | 2014-01-11 20:23:52 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-11 20:23:52 -0800 |
| commit | ea4e1ee9b80fd41e1e023391b8d07949fb00b039 (patch) | |
| tree | e5a9ad50ca955435b63e75928602075c3f5a03c8 /Test/dafny0/TypeTests.dfy | |
| parent | 59f0250f9b4cb78b65f48cfcbddfd22f5271e96d (diff) | |
Fixed spurious complaint about assignment to non-ghost variable
Diffstat (limited to 'Test/dafny0/TypeTests.dfy')
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 42457918..ca89b08a 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -116,3 +116,8 @@ method M() k, m :| 0 <= k < m; // error: not allowed in ghost context
}
}
+
+ghost method GhostM() returns (x: int)
+{
+ x :| true; // no problem (but there once was a problem with this case, where an error was generated for no reason)
+}
|