diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-30 17:13:13 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-30 17:13:13 -0700 |
| commit | b0c51b6fdf1960bbee547959eaf9b0985dee10a9 (patch) | |
| tree | 61223cc2bed18d7913cac860cd45d966056ff04b /Source/DafnyExtension/ResolverTagger.cs | |
| parent | d4472576ba4f4678f48313e69733254fb1e7017c (diff) | |
Rename _reverifyPost to $_reverifyPost, so that it doesn't show up in BVD
Remove some duplicated hover text in DafnyExtension
Enable Code Contracts in the build
Diffstat (limited to 'Source/DafnyExtension/ResolverTagger.cs')
| -rw-r--r-- | Source/DafnyExtension/ResolverTagger.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs index d1af6878..ca9ed169 100644 --- a/Source/DafnyExtension/ResolverTagger.cs +++ b/Source/DafnyExtension/ResolverTagger.cs @@ -311,7 +311,7 @@ namespace DafnyLanguage Snapshot = snapshot;
}
public SnapshotSpan Span() {
- Contract.Requires(Snapshot != null); // requires that Snapshot has been filled in
+ Contract.Assume(Snapshot != null); // requires that Snapshot has been filled in
var line = Snapshot.GetLineFromLineNumber(Line);
Contract.Assume(Column <= line.Length); // this is really a precondition of the constructor + FillInSnapshot
var length = Math.Min(line.Length - Column, 5);
|