Updated parser.cs files to pick up the new .frame improvements from boogiepartners

3 files changed, 34 insertions, 28 deletions

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 9b344a4f..0d906de4 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -2038,12 +2038,15 @@ public class Errors {
   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 virtual void SynErr (string filename, int line, int col, int n) {

-    string s = GetErrorString(n);

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

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

+    SynErr(filename, line, col, GetSyntaxErrorString(n));

+  }

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

+	  Contract.Requires(msg != null);

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

 		count++;

   }

-  public string GetErrorString(int n) {

+  string GetSyntaxErrorString(int n) {

 		string s;

 		switch (n) {

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

@@ -2181,20 +2184,20 @@ public class Errors {
     return s;

 	}

 

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

-	  Contract.Requires(s != null);

-		errorStream.WriteLine(errMsgFormat, filename, line, col, 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 virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

+	  Contract.Requires(msg != null);

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

+		count++;

+	}

 

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

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

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

+		Contract.Requires(msg != null);

+		errorStream.WriteLine(warningMsgFormat, filename, line, col, msg);

 	}

 } // Errors

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 1877fafe..cc295157 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2063,12 +2063,15 @@ public class Errors {
   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 virtual void SynErr (string filename, int line, int col, int n) {

-    string s = GetErrorString(n);

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

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

+    SynErr(filename, line, col, GetSyntaxErrorString(n));

+  }

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

+	  Contract.Requires(msg != null);

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

 		count++;

   }

-  public string GetErrorString(int n) {

+  string GetSyntaxErrorString(int n) {

 		string s;

 		switch (n) {

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

@@ -2223,20 +2226,20 @@ public class Errors {
     return s;

 	}

 

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

-	  Contract.Requires(s != null);

-		errorStream.WriteLine(errMsgFormat, filename, line, col, 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 virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

+	  Contract.Requires(msg != null);

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

+		count++;

+	}

 

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

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

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

+		Contract.Requires(msg != null);

+		errorStream.WriteLine(warningMsgFormat, filename, line, col, msg);

 	}

 } // Errors

 

diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer
index d861d253..6f4068c6 100644
--- a/Test/bitvectors/Answer
+++ b/Test/bitvectors/Answer
@@ -25,8 +25,8 @@ bv3.bpl(2,5): Error: type name: bv16 is registered for bitvectors
 

 Boogie program verifier finished with 1 verified, 0 errors

 -------------------- bv7.bpl --------------------

-bv7.bpl(4,14): Error: arguments of extract need to be integer literals

-bv7.bpl(5,15): Error: parentheses around bitvector bounds are not allowed

+bv7.bpl(4,14): error: arguments of extract need to be integer literals

+bv7.bpl(5,15): error: parentheses around bitvector bounds are not allowed

 2 parse errors detected in bv7.bpl

 -------------------- bv4.bpl - /bv:n --------------------

 bv4.bpl(3,6): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

@@ -37,13 +37,13 @@ bv4.bpl(5,14): Error: no bitvector handling specified, please use /bv:i or /bv:z
 -------------------- bv5.bpl --------------------

 bv5.bpl(10,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        bv5.bpl(5,12): anon0

+    bv5.bpl(5,12): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 -------------------- bv6.bpl --------------------

 bv6.bpl(8,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        bv6.bpl(5,5): anon0

+    bv6.bpl(5,5): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 -------------------- bv8.bpl --------------------