From 0557e6509f413fe48ee21f538b69bf72e52fc36e Mon Sep 17 00:00:00 2001 From: rustanleino Date: Tue, 26 Oct 2010 01:10:24 +0000 Subject: 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 --- Source/Core/Parser.cs | 48 +++++++++++++----------------------- Source/Core/Scanner.cs | 4 +-- Source/Dafny/Dafny.atg | 19 +++++++++++++-- Source/Dafny/Parser.cs | 65 +++++++++++++++++++++++++------------------------ Source/Dafny/Scanner.cs | 4 +-- 5 files changed, 71 insertions(+), 69 deletions(-) (limited to 'Source') 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 +/// 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. +/// +public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ modules, BuiltIns builtIns, + Errors/*!*/ errors) { + Contract.Requires(s != null); + Contract.Requires(filename != null); + Contract.Requires(cce.NonNullElements(modules)); + Contract.Requires(errors != null); List 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 ee, out Type ty.> { "," Expression (. 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 (. ee = new List(); 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 +/// 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. +/// +public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ modules, BuiltIns builtIns, + Errors/*!*/ errors) { + Contract.Requires(s != null); + Contract.Requires(filename != null); + Contract.Requires(cce.NonNullElements(modules)); + Contract.Requires(errors != null); List 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/*!*/ 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]); } -- cgit v1.2.3