diff options
| author |  chmaria <unknown> | 2014-11-04 06:51:56 +0100 |
|---|---|---|
| committer | chmaria <unknown> | 2014-11-04 06:51:56 +0100 |
| commit | cac5c7d4a8a387f757a7ac44a6bc9b6c340f01d6 (patch) | |
| tree | ae8ed555c90c72baaaa1799f4a303f6294b97344 | |
| parent | de76f8df4091e6f14a1a6ce8c82c9a50bff68a87 (diff) | |
Made dirty statements ghost.
| -rw-r--r-- | Source/Dafny/Resolver.cs | 4 | ||||
| -rw-r--r-- | Test/dafny0/DirtyLoops.dfy | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 757995f2..69acf9de 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4755,7 +4755,7 @@ namespace Microsoft.Dafny ResolveFrameExpression(fe, "modifies", bodyMustBeSpecOnly, codeContext);
}
}
- s.IsGhost = bodyMustBeSpecOnly;
+ s.IsGhost = s.Body == null || bodyMustBeSpecOnly;
if (s.Body != null) {
loopStack.Add(s); // push
if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map
@@ -4825,7 +4825,7 @@ namespace Microsoft.Dafny bodyMustBeSpecOnly = true;
}
}
- s.IsGhost = bodyMustBeSpecOnly;
+ s.IsGhost = s.Body == null || bodyMustBeSpecOnly;
if (s.Body != null) {
// clear the labels for the duration of checking the body, because break statements are not allowed to leave a forall statement
diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy index 5d356f0a..d3164fa9 100644 --- a/Test/dafny0/DirtyLoops.dfy +++ b/Test/dafny0/DirtyLoops.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:1 "%t.dprint.dfy" >> "%t"
// RUN: %diff "%s.expect" "%t"
method M0(S: set<int>) {
|