diff options
| author |  Rustan Leino <unknown> | 2013-04-19 17:26:14 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-04-19 17:26:14 -0700 |
| commit | 9aaa0798bac4672064b75d311d23f7dc7e61bca7 (patch) | |
| tree | de675245ff23fa5ec1d8598bf1b96becb2f0dbcd /Source/Dafny | |
| parent | 7555f1e7dc8556b8ff1d2cab3c637b0556d1a946 (diff) | |
Fixed (completeness) bug in translation of automatic induction--previously, the induction-inserted 'forall' statement had caused the heap to be advanced).
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Translator.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 3d07a729..ff29df39 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2012,6 +2012,7 @@ namespace Microsoft.Dafny { }
var recursiveCall = new CallStmt(m.tok, new List<Expression>(), recursiveCallReceiver, m.Name, recursiveCallArgs);
recursiveCall.Method = m; // resolve here
+ recursiveCall.IsGhost = m.IsGhost; // resolve here
Expression parRange = new LiteralExpr(m.tok, true);
parRange.Type = Type.Bool; // resolve here
|