Boogie:

* Updated Parser.cs/Scanner.cs to use new .frame files from boogiepartners.
* It changes, for example, "syntax error:" to just "error:", so adjusted expected Test outputs.
Dafny:
* Ditto for its Parser.cs/Scanner.cs.
* Added ability to provide a custom Errors handler for scanner/parser.
* Added Test/dafny1/Cubes.dfy

5 files changed, 71 insertions, 69 deletions

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index a2887dcf..9b344a4f 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -2035,13 +2035,16 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 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 = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=text

-  public string/*!*/ errMsgFormat4 = "{0}({1},{2}): Error: {3}"; // 0=line, 1=column, 2=text

-  public string/*!*/ errMsgFormat = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=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) {

+	public virtual void SynErr (string filename, int line, int col, int n) {

+    string s = GetErrorString(n);

+		errorStream.WriteLine(errMsgFormat, filename, line, col, s);

+		count++;

+  }

+  public string GetErrorString(int n) {

 		string s;

-		Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);

 		switch (n) {

 			case 0: s = "EOF expected"; break;

 			case 1: s = "ident expected"; break;

@@ -2175,40 +2178,23 @@ public class Errors {
 

 			default: s = "error " + n; break;

 		}

-		//errorStream.WriteLine(errMsgFormat, line, col, s);

-		errorStream.WriteLine(s);

-		count++;

-	}

-

-	public void SemErr (int line, int col, string/*!*/ s) {

-	  Contract.Requires(s != null);

-		errorStream.WriteLine(errMsgFormat, line, col, s);

-		count++;

+    return s;

 	}

 

-	public void SemErr (string filename, int line, int col, string/*!*/ s) {

+	public virtual void SemErr (string filename, int line, int col, string/*!*/ s) {

 	  Contract.Requires(s != null);

-		errorStream.WriteLine(errMsgFormat4, filename, line, col, s);

+		errorStream.WriteLine(errMsgFormat, filename, line, col, s);

 		count++;

 	}

 	

-	public void SemErr (string s) {

-		errorStream.WriteLine(s);

-		count++;

+	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

+		Contract.Requires(tok != null);

+		Contract.Requires(msg != null);

+		SemErr(tok.filename, tok.line, tok.col, msg);

 	}

 

-    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

-      Contract.Requires(tok != null);

-      Contract.Requires(msg != null);

-      SemErr(tok.filename, tok.line, tok.col, msg);

-    }

-	

-	public void Warning (int line, int col, string s) {

-		errorStream.WriteLine(errMsgFormat, line, col, s);

-	}

-	

-	public void Warning(string s) {

-		errorStream.WriteLine(s);

+	public virtual void Warning (int line, int col, string s) {

+		errorStream.WriteLine(warningMsgFormat, line, col, s);

 	}

 } // Errors

 

diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index deb8b809..faab5837 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -375,7 +375,7 @@ void objectInvariant(){
 				// eol handling uniform across Windows, Unix and Mac

 				if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 				if (ch == EOL) {

-					line++; col = 0;
+					line++; col = 0;

 				} else if (ch == '#' && col == 1) {

 				  int prLine = line;

 				  int prColumn = 0;

@@ -536,7 +536,7 @@ void objectInvariant(){
 		int recKind = noSym;

 		int recEnd = pos;

 		t = new Token();

-		t.pos = pos; t.col = col; t.line = line;
+		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

 		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 560c0aea..cfb9be3e 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -96,13 +96,28 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   Contract.Requires(s != null);

   Contract.Requires(filename != null);

   Contract.Requires(cce.NonNullElements(modules));

+  Errors errors = new Errors();

+  return Parse(s, filename, modules, builtIns, errors);

+}

+

+///<summary>

+/// Parses top-level things (modules, classes, datatypes, class members)

+/// and appends them in appropriate form to "modules".

+/// Returns the number of parsing errors encountered.

+/// Note: first initialize the Scanner with the given Errors sink.

+///</summary>

+public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns,

+                         Errors/*!*/ errors) {

+  Contract.Requires(s != null);

+  Contract.Requires(filename != null);

+  Contract.Requires(cce.NonNullElements(modules));

+  Contract.Requires(errors != null);

   List<ModuleDecl/*!*/> oldModules = theModules;

   theModules = modules;

   BuiltIns oldBuiltIns = builtIns;

   theBuiltIns = builtIns;

   byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));

   MemoryStream ms = new MemoryStream(buffer,false);

-  Errors errors = new Errors();

   Scanner scanner = new Scanner(ms, errors, filename);

   Parser parser = new Parser(scanner, errors);

   parser.Parse();

@@ -743,7 +758,7 @@ AssignRhs<.out List<Expression> ee, out Type ty.>
       { "," Expression<out e>          (. ee.Add(e); .)

       }

       "]"                              (. // make sure an array class with this dimensionality exists

-                                          UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, Type.Int, true);

+                                          UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);

                                        .)

     ]

   | Expression<out e>                  (. ee = new List<Expression>(); ee.Add(e); .)

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 6577e993..1877fafe 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -109,13 +109,28 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   Contract.Requires(s != null);

   Contract.Requires(filename != null);

   Contract.Requires(cce.NonNullElements(modules));

+  Errors errors = new Errors();

+  return Parse(s, filename, modules, builtIns, errors);

+}

+

+///<summary>

+/// Parses top-level things (modules, classes, datatypes, class members)

+/// and appends them in appropriate form to "modules".

+/// Returns the number of parsing errors encountered.

+/// Note: first initialize the Scanner with the given Errors sink.

+///</summary>

+public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns,

+                         Errors/*!*/ errors) {

+  Contract.Requires(s != null);

+  Contract.Requires(filename != null);

+  Contract.Requires(cce.NonNullElements(modules));

+  Contract.Requires(errors != null);

   List<ModuleDecl/*!*/> oldModules = theModules;

   theModules = modules;

   BuiltIns oldBuiltIns = builtIns;

   theBuiltIns = builtIns;

   byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));

   MemoryStream ms = new MemoryStream(buffer,false);

-  Errors errors = new Errors();

   Scanner scanner = new Scanner(ms, errors, filename);

   Parser parser = new Parser(scanner, errors);

   parser.Parse();

@@ -2045,13 +2060,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 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 = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=text

-  public string/*!*/ errMsgFormat4 = "{0}({1},{2}): Error: {3}"; // 0=line, 1=column, 2=text

-  public string/*!*/ errMsgFormat = "-- line {0} col {1}: {2}"; // 0=line, 1=column, 2=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) {

+	public virtual void SynErr (string filename, int line, int col, int n) {

+    string s = GetErrorString(n);

+		errorStream.WriteLine(errMsgFormat, filename, line, col, s);

+		count++;

+  }

+  public string GetErrorString(int n) {

 		string s;

-		Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);

 		switch (n) {

 			case 0: s = "EOF expected"; break;

 			case 1: s = "ident expected"; break;

@@ -2202,40 +2220,23 @@ public class Errors {
 

 			default: s = "error " + n; break;

 		}

-		//errorStream.WriteLine(errMsgFormat, line, col, s);

-		errorStream.WriteLine(s);

-		count++;

+    return s;

 	}

 

-	public void SemErr (int line, int col, string/*!*/ s) {

+	public virtual void SemErr (string filename, int line, int col, string/*!*/ s) {

 	  Contract.Requires(s != null);

-		errorStream.WriteLine(errMsgFormat, line, col, s);

-		count++;

-	}

-

-	public void SemErr (string filename, int line, int col, string/*!*/ s) {

-	  Contract.Requires(s != null);

-		errorStream.WriteLine(errMsgFormat4, filename, line, col, s);

+		errorStream.WriteLine(errMsgFormat, filename, line, col, s);

 		count++;

 	}

 	

-	public void SemErr (string s) {

-		errorStream.WriteLine(s);

-		count++;

+	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

+		Contract.Requires(tok != null);

+		Contract.Requires(msg != null);

+		SemErr(tok.filename, tok.line, tok.col, msg);

 	}

 

-    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

-      Contract.Requires(tok != null);

-      Contract.Requires(msg != null);

-      SemErr(tok.filename, tok.line, tok.col, msg);

-    }

-	

-	public void Warning (int line, int col, string s) {

-		errorStream.WriteLine(errMsgFormat, line, col, s);

-	}

-	

-	public void Warning(string s) {

-		errorStream.WriteLine(s);

+	public virtual void Warning (int line, int col, string s) {

+		errorStream.WriteLine(warningMsgFormat, line, col, s);

 	}

 } // Errors

 

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 75d301a4..de87c6ad 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -375,7 +375,7 @@ void objectInvariant(){
 				// eol handling uniform across Windows, Unix and Mac

 				if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 				if (ch == EOL) {

-					line++; col = 0;
+					line++; col = 0;

 				} else if (ch == '#' && col == 1) {

 				  int prLine = line;

 				  int prColumn = 0;

@@ -552,7 +552,7 @@ void objectInvariant(){
 		int recKind = noSym;

 		int recEnd = pos;

 		t = new Token();

-		t.pos = pos; t.col = col; t.line = line;
+		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

 		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }