summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Parser.cs12
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs8
2 files changed, 12 insertions, 8 deletions
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 01438f68..d50a4dd6 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -4429,8 +4429,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string errMsgFormat = "{0}({1},{2}): Error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): Warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
public void SynErr(string filename, int line, int col, int n) {
SynErr(filename, line, col, GetSyntaxErrorString(n));
@@ -4438,7 +4438,7 @@ public class Errors {
public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
Contract.Requires(msg != null);
- errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
+ errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg);
count++;
}
@@ -4701,7 +4701,7 @@ public class Errors {
public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
Contract.Requires(msg != null);
- errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
+ errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg);
count++;
}
@@ -4713,7 +4713,7 @@ public class Errors {
public virtual void Warning(string filename, int line, int col, string msg) {
Contract.Requires(msg != null);
- errorStream.WriteLine(warningMsgFormat, filename, line, col, msg);
+ errorStream.WriteLine(warningMsgFormat, filename, line, col - 1, msg);
}
} // Errors
@@ -4721,6 +4721,4 @@ public class Errors {
public class FatalError: Exception {
public FatalError(string m): base(m) {}
}
-
-
} \ No newline at end of file
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 9fdc9320..d22899ab 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -273,7 +273,13 @@ namespace Microsoft.Dafny
{
public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null)
{
- base.ReportBplError(tok, message, error, tw, category);
+ // Dafny has 0-indexed columns, but Boogie counts from 1
+ var realigned_tok = new Token(tok.line, tok.col - 1);
+ realigned_tok.kind = tok.kind;
+ realigned_tok.pos = tok.pos;
+ realigned_tok.val = tok.val;
+ realigned_tok.filename = tok.filename;
+ base.ReportBplError(realigned_tok, message, error, tw, category);
if (tok is Dafny.NestedToken)
{