diff options
author | leino <unknown> | 2015-07-01 13:33:38 -0700 |
---|---|---|
committer | leino <unknown> | 2015-07-01 13:33:38 -0700 |
commit | 7dcc8c64e6fbcbf2fa40702619795144f9681f24 (patch) | |
tree | 0c7e8dfe613a29ef4dd41eaf58378e7bb7921218 | |
parent | e46ecaaca54ae619741abeb88e8a153d3a2fe66e (diff) |
Made code contracts compliant
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 1 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 1 |
2 files changed, 1 insertions, 1 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; }
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index e48a7932..29e36ccd 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2399,7 +2399,6 @@ namespace Microsoft.Dafny }
protected override bool VisitOneStmt(Statement stmt, ref FuelAdjustment_Context st) {
- Contract.Requires(stmt != null);
Resolver.CheckForFuelAdjustments(stmt.Tok, stmt.Attributes, st.currentModule, st.reporter);
return true;
}
|