From 1ac82df441e621fce2f38d53b5d17c69650d7358 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 21 Aug 2012 00:24:08 -0700
Subject: Dafny and Boogie: get rid of 'static' fields in parser

---
 Source/Core/BoogiePL.atg | 58 +++++++++++++++++++++++++++++-------------------
 1 file changed, 35 insertions(+), 23 deletions(-)

(limited to 'Source/Core/BoogiePL.atg')

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index aed741d8..9c721703 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -19,16 +19,15 @@ COMPILER BoogiePL
 
 /*--------------------------------------------------------------------------*/
 
-static Program/*!*/ Pgm = new Program();
+readonly Program/*!*/ Pgm;
 
-static Expr/*!*/ dummyExpr = new LiteralExpr(Token.NoToken, false);
-static Cmd/*!*/ dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
-static Block/*!*/ dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(),
-                                     new ReturnCmd(Token.NoToken));
-static Bpl.Type/*!*/ dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
-static Bpl.ExprSeq/*!*/ dummyExprSeq = new ExprSeq ();
-static TransferCmd/*!*/ dummyTransferCmd = new ReturnCmd(Token.NoToken);
-static StructuredCmd/*!*/ dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
+readonly Expr/*!*/ dummyExpr;
+readonly Cmd/*!*/ dummyCmd;
+readonly Block/*!*/ dummyBlock;
+readonly Bpl.Type/*!*/ dummyType;
+readonly Bpl.ExprSeq/*!*/ dummyExprSeq;
+readonly TransferCmd/*!*/ dummyTransferCmd;
+readonly StructuredCmd/*!*/ dummyStructuredCmd;
 
 ///<summary>
 ///Returns the number of parsing errors encountered.  If 0, "program" returns as
@@ -64,20 +63,33 @@ public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Prog
   Errors errors = new Errors();
   Scanner scanner = new Scanner(ms, errors, filename);
 
-  Parser parser = new Parser(scanner, errors);
-  Pgm = new Program(); // reset the global variable
-    parser.Parse();
-    if (parser.errors.count == 0)
-    {
-      program = Pgm;
-      program.ProcessDatatypeConstructors();
-      return 0;
-    }
-    else
-    {
-      program = null;
-      return parser.errors.count;
-    }
+  Parser parser = new Parser(scanner, errors, false);
+  parser.Parse();
+  if (parser.errors.count == 0)
+  {
+    program = parser.Pgm;
+    program.ProcessDatatypeConstructors();
+    return 0;
+  }
+  else
+  {
+    program = null;
+    return parser.errors.count;
+  }
+}
+
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
+ : this(scanner, errors)
+{
+  // initialize readonly fields
+  Pgm = new Program();
+  dummyExpr = new LiteralExpr(Token.NoToken, false);
+  dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
+  dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(), new ReturnCmd(Token.NoToken));
+  dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
+  dummyExprSeq = new ExprSeq ();
+  dummyTransferCmd = new ReturnCmd(Token.NoToken);
+  dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
 }
 
 // Class to represent the bounds of a bitvector expression t[a:b].
-- 
cgit v1.2.3