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 | |
| parent | 59f0250f9b4cb78b65f48cfcbddfd22f5271e96d (diff) | |
Fixed spurious complaint about assignment to non-ghost variable
| -rw-r--r-- | Source/Dafny/Resolver.cs | 2 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 5 |
2 files changed, 6 insertions, 1 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 0b63a635..b8c561b3 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4536,7 +4536,7 @@ namespace Microsoft.Dafny var ec = ErrorCount;
ResolveExpression(lhs, true, codeContext);
if (ec == ErrorCount) {
- if (update == null && specContextOnly && !AssignStmt.LhsIsToGhost(lhs)) {
+ if (update == null && specContextOnly && !AssignStmt.LhsIsToGhost(lhs) && !codeContext.IsGhost) {
Error(lhs, "cannot assign to non-ghost variable in a ghost context");
}
if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
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)
+}
|