summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-07-31 19:09:55 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-07-31 19:09:55 -0700
commitd86d8e6d41394166370bdaee4b02fa1ce6886f42 (patch)
tree6cc41add8a653e655f2f2ecbc862d840a688f88b
parent744da7955a4468c411b5d01d313012edc7452dda (diff)
Fix an issue with column numbers in the VS extension
The error came from the fact that Dafny now consistently used 0-based indexing. Boogie gets its traces from text that's inserted by Dafny in the Boogie file, so there's no need to apply an extra offset in the VS extension.
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 4237041f..6eaec5a6 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -529,7 +529,7 @@ namespace DafnyLanguage
else
{
var line = Math.Max(0, int.Parse(match.Groups[1].Value) - 1);
- var column = Math.Max(0, int.Parse(match.Groups[2].Value) - 1);
+ var column = Math.Max(0, int.Parse(match.Groups[2].Value));
var sLine = Snapshot.GetLineFromLineNumber(line);
Contract.Assert(column <= sLine.Length);
var sLength = Math.Max(0, Math.Min(sLine.Length - column, 0));