From d86d8e6d41394166370bdaee4b02fa1ce6886f42 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 19:09:55 -0700 Subject: 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. --- Source/DafnyExtension/ResolverTagger.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Source/DafnyExtension') 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)); -- cgit v1.2.3