diff options
author | Rustan Leino <leino@microsoft.com> | 2011-11-16 22:15:41 -0800 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2011-11-16 22:15:41 -0800 |
commit | 44fadfb3db027ce727ecf1d209c3a4a10036d521 (patch) | |
tree | fd46795e086b6ea651fe20027ba6e994c520c9f3 /Source/Dafny | |
parent | 2c21674e24312f34cec0a99a72e6afd717abf94c (diff) |
Dafny: fixed bad Code Contracts
Diffstat (limited to 'Source/Dafny')
-rw-r--r-- | Source/Dafny/DafnyOptions.cs | 2 | ||||
-rw-r--r-- | Source/Dafny/Translator.cs | 4 |
2 files changed, 2 insertions, 4 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 8c604b8a..745d50ef 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -33,8 +33,6 @@ namespace Microsoft.Dafny public bool ForceCompile = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
- Contract.Requires(name != null);
- Contract.Requires(ps != null);
var args = ps.args; // convenient synonym
switch (name) {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 88f95f30..d1e41663 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5068,8 +5068,8 @@ namespace Microsoft.Dafny { Contract.Requires(predef != null);
Contract.Requires(heap != null);
Contract.Requires(thisVar != null);
- Contract.Invariant(layerOffset == 0 || layerOffset == 1);
- Contract.Invariant(modifiesFrame != null);
+ Contract.Requires(layerOffset == 0 || layerOffset == 1);
+ Contract.Requires(modifiesFrame != null);
this.translator = translator;
this.predef = predef;
|