summaryrefslogtreecommitdiff
path: root/Source/Dafny/DafnyAst.cs
diff options
context:
space:
mode:
authorGravatar leino <unknown>2015-07-01 13:33:38 -0700
committerGravatar leino <unknown>2015-07-01 13:33:38 -0700
commit7dcc8c64e6fbcbf2fa40702619795144f9681f24 (patch)
tree0c7e8dfe613a29ef4dd41eaf58378e7bb7921218 /Source/Dafny/DafnyAst.cs
parente46ecaaca54ae619741abeb88e8a153d3a2fe66e (diff)
Made code contracts compliant
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r--Source/Dafny/DafnyAst.cs1
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c9c9ccc8..712cb00a 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2987,6 +2987,7 @@ namespace Microsoft.Dafny {
ModuleDefinition ICodeContext.EnclosingModule { get { return this.EnclosingClass.Module; } }
bool ICodeContext.MustReverify { get { return false; } }
+ [Pure]
public bool IsFuelAware() { return IsRecursive || IsFueled; }
}