Boogie: Added an additional parameter 'defines' to the method 'BoogiePL.Parser.Parse'.

6 files changed, 15 insertions, 8 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc
index c1bf358e..1923ca49 100644
--- a/Source/BoogieDriver/BoogieDriver.ssc
+++ b/Source/BoogieDriver/BoogieDriver.ssc
@@ -349,7 +349,7 @@ namespace Microsoft.Boogie
         Program programSnippet;

         int errorCount;

         try {

-          errorCount = BoogiePL.Parser.Parse(bplFileName, out programSnippet);

+          errorCount = BoogiePL.Parser.Parse(bplFileName, null, out programSnippet);

           if (programSnippet == null || errorCount != 0) {

             Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);

             okay = false;

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 896dc0e5..42f9f735 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -34,13 +34,16 @@ static StructuredCmd! dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
 ///Returns the number of parsing errors encountered.  If 0, "program" returns as

 ///the parsed program.

 ///</summary>

-public static int Parse (string! filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

+public static int Parse (string! filename, /*maybe null*/ List<string!> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

 

 

   FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);

 //  Scanner scanner = new Scanner(stream);

   

-  string s = ParserHelper.Fill(stream,new List<string!>());

+  if (defines == null) {

+    defines = new List<string!>();

+  }

+  string s = ParserHelper.Fill(stream, defines);

   byte[]! buffer = (!) UTF8Encoding.Default.GetBytes(s);

   MemoryStream ms = new MemoryStream(buffer,false);

   Errors errors = new Errors();

diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc
index f23e0f9e..7ca3bd73 100644
--- a/Source/Core/Parser.ssc
+++ b/Source/Core/Parser.ssc
@@ -53,13 +53,16 @@ static StructuredCmd! dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
 ///Returns the number of parsing errors encountered.  If 0, "program" returns as

 ///the parsed program.

 ///</summary>

-public static int Parse (string! filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

+public static int Parse (string! filename, /*maybe null*/ List<string!> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

 

 

   FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);

 //  Scanner scanner = new Scanner(stream);

   

-  string s = ParserHelper.Fill(stream,new List<string!>());

+  if (defines == null) {

+    defines = new List<string!>();

+  }

+  string s = ParserHelper.Fill(stream, defines);

   byte[]! buffer = (!) UTF8Encoding.Default.GetBytes(s);

   MemoryStream ms = new MemoryStream(buffer,false);

   Errors errors = new Errors();

diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc
index d7f8dc69..c4988de3 100644
--- a/Source/Core/Scanner.ssc
+++ b/Source/Core/Scanner.ssc
@@ -7,9 +7,10 @@ using System.Text;
 using Microsoft.Contracts;

 using Microsoft.Boogie;

 using BoogiePL;

-namespace Microsoft.Boogie {

 

 

+namespace Microsoft.Boogie {

+

 //-----------------------------------------------------------------------------------

 // Buffer

 //-----------------------------------------------------------------------------------

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 48b1beaf..e417ac68 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -250,7 +250,7 @@ namespace Microsoft.Dafny {
       string! preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl");

       

       Bpl.Program prelude;

-      int errorCount = Bpl.Parser.Parse(preludePath, out prelude);

+      int errorCount = Bpl.Parser.Parse(preludePath, null, out prelude);

       if (prelude == null || errorCount > 0) {

         return null;

       } else {

diff --git a/Source/DafnyDriver/DafnyDriver.ssc b/Source/DafnyDriver/DafnyDriver.ssc
index d9d9a6be..952a5ea6 100644
--- a/Source/DafnyDriver/DafnyDriver.ssc
+++ b/Source/DafnyDriver/DafnyDriver.ssc
@@ -366,7 +366,7 @@ namespace Microsoft.Boogie
         Program programSnippet;

         int errorCount;

         try {

-          errorCount = Microsoft.Boogie.Parser.Parse(bplFileName, out programSnippet);

+          errorCount = Microsoft.Boogie.Parser.Parse(bplFileName, null, out programSnippet);

           if (programSnippet == null || errorCount != 0) {

             Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);

             okay = false;