Updated the frame files to work with the latest Coco/R. This entails *not* having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories.

Lots of code changes to compensate for the new frame files.

10 files changed, 1536 insertions, 1675 deletions

diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc
index 6b4cae62..07723e4d 100644
--- a/Source/Core/Absy.ssc
+++ b/Source/Core/Absy.ssc
@@ -1680,17 +1680,26 @@ namespace Microsoft.Boogie
                           VariableSeq! inParams, VariableSeq! outParams,

                           VariableSeq! localVariables, [Captured] StmtList! structuredStmts)

     {

-      this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null);

+      this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors());

     }

 

     public Implementation(IToken! tok, string! name, TypeVariableSeq! typeParams,

                           VariableSeq! inParams, VariableSeq! outParams,

-                          VariableSeq! localVariables, [Captured] StmtList! structuredStmts, QKeyValue kv)

+                          VariableSeq! localVariables, [Captured] StmtList! structuredStmts,

+                          Errors! errorHandler)

+    {

+      this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler);

+    }

+

+    public Implementation(IToken! tok, string! name, TypeVariableSeq! typeParams,

+                          VariableSeq! inParams, VariableSeq! outParams,

+                          VariableSeq! localVariables, [Captured] StmtList! structuredStmts, QKeyValue kv,

+                          Errors! errorHandler)

       : base(tok, name, typeParams, inParams, outParams)

     {

       LocVars = localVariables;

       StructuredStmts = structuredStmts;

-      BigBlocksResolutionContext ctx = new BigBlocksResolutionContext(structuredStmts);

+      BigBlocksResolutionContext ctx = new BigBlocksResolutionContext(structuredStmts, errorHandler);

       Blocks = ctx.Blocks;

       BlockPredecessorsComputed = false;

       scc = null;

diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index bf80116c..d682029e 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -202,9 +202,11 @@ namespace Microsoft.Boogie
     string! prefix = "anon";

     int anon = 0;

     Set<string!> allLabels = new Set<string!>();

+    Errors! errorHandler;

 

-    public BigBlocksResolutionContext(StmtList! stmtList) {

+    public BigBlocksResolutionContext(StmtList! stmtList, Errors! errorHandler) {

       this.stmtList = stmtList;

+      this.errorHandler = errorHandler;

     }

 

     public List<Block!>! Blocks {

@@ -212,7 +214,7 @@ namespace Microsoft.Boogie
         if (blocks == null) {

           blocks = new List<Block!>();

 

-          int startErrorCount = BoogiePL.Errors.count;

+          int startErrorCount = this.errorHandler.count;

           // Check that there are no goto's into the middle of a block, and no break statement to a non-enclosing loop.

           // Also, determine a good value for "prefix".

           CheckLegalLabels(stmtList, null, null);

@@ -223,7 +225,7 @@ namespace Microsoft.Boogie
           // determine successor blocks

           RecordSuccessors(stmtList, null);

 

-          if (BoogiePL.Errors.count == startErrorCount) {

+          if (this.errorHandler.count == startErrorCount) {

             // generate blocks from the big blocks

             CreateBlocks(stmtList, null);

           }

@@ -270,7 +272,7 @@ namespace Microsoft.Boogie
               }

             }

             if (!found) {

-              BoogiePL.Errors.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined or out of reach");

+              this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined or out of reach");

             }

           }

         }

@@ -299,7 +301,7 @@ namespace Microsoft.Boogie
                 bcmd.BreakEnclosure = bb;

               } else {

                 // the label of bb refers to the first statement of bb, which in which case is a simple statement, not an if/while statement

-                BoogiePL.Errors.SemErr(bcmd.tok, "Error: break label '" + bcmd.Label + "' must designate an enclosing statement");

+                this.errorHandler.SemErr(bcmd.tok, "Error: break label '" + bcmd.Label + "' must designate an enclosing statement");

               }

               found = true;  // don't look any further, since we've found a matching label

               break;

@@ -307,9 +309,9 @@ namespace Microsoft.Boogie
           }

           if (!found) {

             if (bcmd.Label == null) {

-              BoogiePL.Errors.SemErr(bcmd.tok, "Error: break statement is not inside a loop");

+              this.errorHandler.SemErr(bcmd.tok, "Error: break statement is not inside a loop");

             } else {

-              BoogiePL.Errors.SemErr(bcmd.tok, "Error: break label '" + bcmd.Label + "' must designate an enclosing statement");

+              this.errorHandler.SemErr(bcmd.tok, "Error: break label '" + bcmd.Label + "' must designate an enclosing statement");

             }

           }

         }

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index aded331b..896dc0e5 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -7,6 +7,8 @@
 using PureCollections;

 using System.Collections;

 using System.Collections.Generic;

+using System.IO;

+using System.Text;

 using Microsoft.Boogie;

 using Microsoft.Basetypes;

 using Bpl = Microsoft.Boogie;

@@ -33,22 +35,24 @@ static StructuredCmd! dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
 ///the parsed program.

 ///</summary>

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

-  using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

-    Buffer.Fill(reader);

-    Scanner.Init(filename);

-    return Parse(out program);

-  }

-}

 

-///<summary>

-///Returns the number of parsing errors encountered.  If 0, "program" returns as

-///the parsed program.

-///Note: first initialize the Scanner.

-///</summary>

-public static int Parse (out /*maybe null*/ Program program) {

+

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

+//  Scanner scanner = new Scanner(stream);

+  

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

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

+  MemoryStream ms = new MemoryStream(buffer,false);

+  Errors errors = new Errors();

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

+

+/*  

+  Scanner scanner = new Scanner(filename);

+*/

+  Parser parser = new Parser(scanner, errors);

   Pgm = new Program(); // reset the global variable

-    Parse();

-    if (Errors.count == 0)

+    parser.Parse();

+    if (parser.errors.count == 0)

     {

       program = Pgm;

       return 0;

@@ -56,22 +60,50 @@ public static int Parse (out /*maybe null*/ Program program) {
     else

     {

       program = null;

-      return Errors.count;

+      return parser.errors.count;

     }

+/*

+  using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

+    Buffer.Fill(reader);

+    Scanner.Init(filename);

+    return Parse(out program);

+  }

+*/

 }

 

-

+///<summary>

+///Returns the number of parsing errors encountered.  If 0, "program" returns as

+///the parsed program.

+///Note: first initialize the Scanner.

+///</summary>

+//public static int Parse (out /*maybe null*/ Program program) {

+//  Pgm = new Program(); // reset the global variable

+//    Parse();

+//    if (Errors.count == 0)

+//    {

+//      program = Pgm;

+//      return 0;

+//    }

+//    else

+//    {

+//      program = null;

+//      return Errors.count;

+//    }

+//}

+

+/*

 public static int ParseProposition (string! text, out Expr! expression)

 {

   Buffer.Fill(text);

   Scanner.Init(string.Format("\"{0}\"", text));

 

   Errors.SynErr = new ErrorProc(SynErr);

-  t = new Token();

+  la = new Token();

   Get();

   Proposition(out expression);

   return Errors.count;

 }

+*/

 

 // Class to represent the bounds of a bitvector expression t[a:b].

 // Objects of this class only exist during parsing and are directly

@@ -228,7 +260,7 @@ IdsTypeWhere<bool allowWhereClauses, TypedIdentSeq! tyds>
   [ "where" Expression<out nne>  (. if (allowWhereClauses) {

                                       wh = nne;

                                     } else {

-                                      SemErr("where clause not allowed here");

+                                      this.SemErr("where clause not allowed here");

                                     }

                                  .)

   ]

@@ -267,8 +299,8 @@ TypeArgs<TypeSeq! ts>
 

 TypeAtom<out Bpl.Type! ty>

 = (. ty = dummyType; .)

-  ( "int"              (. ty = new BasicType(token, SimpleType.Int); .)

-  | "bool"             (. ty = new BasicType(token, SimpleType.Bool); .)

+  ( "int"              (. ty = new BasicType(t, SimpleType.Int); .)

+  | "bool"             (. ty = new BasicType(t, SimpleType.Bool); .)

   /* note: bitvectors are handled in UnresolvedTypeIdentifier */

   |

   "("

@@ -285,7 +317,7 @@ MapType<out Bpl.Type! ty>
      TypeVariableSeq! typeParameters = new TypeVariableSeq();

    .)

   [ TypeParams<out nnTok, out typeParameters> (. tok = nnTok; .) ]

-  "["                                         (.  if (tok == null) tok = token;  .)

+  "["                                         (.  if (tok == null) tok = t;  .)

     [ Types<arguments> ]

   "]"

   Type<out result>

@@ -296,7 +328,7 @@ MapType<out Bpl.Type! ty>
 

 TypeParams<out IToken! tok, out Bpl.TypeVariableSeq! typeParams>

 = (. TokenSeq! typeParamToks; .)

-  "<"    (.  tok = token;  .)

+  "<"    (.  tok = t;  .)

     Idents<out typeParamToks>

   ">"

   (.

@@ -321,7 +353,7 @@ Consts<out VariableSeq! ds>
      bool u = false; QKeyValue kv = null;

      bool ChildrenComplete = false;

      List<ConstantParent!> Parents = null; .)

-  "const"                 (. y = token; .)

+  "const"                 (. y = t; .)

   { Attribute<ref kv> }

   [ "unique"              (. u = true;  .)

   ]

@@ -349,7 +381,7 @@ Consts<out VariableSeq! ds>
   ";"

   .

 

-OrderSpec<out bool ChildrenComplete, out List<ConstantParent!\> Parents>

+OrderSpec<.out bool ChildrenComplete, out List<ConstantParent!> Parents.>

 = (. ChildrenComplete = false;

      Parents = null;

      bool u;

@@ -401,7 +433,7 @@ Function<out DeclarationSeq! ds>
   (.

     if (retTyd == null) {

       // construct a dummy type for the case of syntax error

-      tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));

+      tyd = new TypedIdent(t, "", new BasicType(t, SimpleType.Int));

     } else {

       tyd = retTyd;

     }

@@ -421,7 +453,7 @@ Function<out DeclarationSeq! ds>
         TypedIdent! curr = ((!)arguments[i]).TypedIdent;

         if (curr.Name == "") {

 	  if (prevType == null) {

-	    SemErr(curr.tok, "the type of the last parameter is unspecified");

+	    this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");

 	    break;

 	  }

 	  Type ty = curr.Type;

@@ -430,7 +462,7 @@ Function<out DeclarationSeq! ds>
 	    curr.Name = ((!)(ty as UnresolvedTypeIdentifier)).Name;

 	    curr.Type = prevType;

 	  } else {

-	    SemErr(curr.tok, "expecting an identifier as parameter name");

+	    this.errors.SemErr(curr.tok, "expecting an identifier as parameter name");

 	  }

 	} else {

 	  prevType = curr.Type;

@@ -479,7 +511,7 @@ VarOrType<out TypedIdent! tyd>
                          ((!)(ty as UnresolvedTypeIdentifier)).Arguments.Length == 0) {

                        varName = ((!)(ty as UnresolvedTypeIdentifier)).Name;

                      } else {

-                       SemErr("expected identifier before ':'");

+                       this.SemErr("expected identifier before ':'");

                      }

                   .)

     Type<out ty>

@@ -492,12 +524,12 @@ Axiom<out Axiom! m>
 = (. Expr! e; QKeyValue kv = null; .)

   "axiom"

    { Attribute<ref kv> }

-   (. IToken! x = token; .)

+   (. IToken! x = t; .)

   Proposition<out e> ";"  (. m = new Axiom(x,e, null, kv); .)

   .

 

 /*------------------------------------------------------------------------*/

-UserDefinedTypes<out List<Declaration!\>! ts>

+UserDefinedTypes<.out List<Declaration!>! ts.>

 = (. Declaration! decl; QKeyValue kv = null; ts = new List<Declaration!> (); .)

   "type"

   { Attribute<ref kv> }

@@ -552,7 +584,7 @@ Procedure<out Procedure! proc, out /*maybe null*/ Implementation impl>
     (.

       // here we attach kv only to the Procedure, not its implementation

       impl = new Implementation(x, x.val, typeParams,

-                                Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null); 

+                                Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors); 

     .)

   )

   (. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .)

@@ -571,7 +603,7 @@ Implementation<out Implementation! impl>
   "implementation"

   ProcSignature<false, out x, out typeParams, out ins, out outs, out kv>

   ImplBody<out locals, out stmtList>

-    (. impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv); .)

+    (. impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); .)

   .

 

 

@@ -602,14 +634,14 @@ Spec<RequiresSeq! pre, IdentifierExprSeq! mods, EnsuresSeq! post>
 

 SpecPrePost<bool free, RequiresSeq! pre, EnsuresSeq! post>

 = (. Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null; .)

-  ( "requires"              (. tok = token; .)

+  ( "requires"              (. tok = t; .)

     { Attribute<ref kv> }

     (Proposition<out e> ";"  (. pre.Add(new Requires(tok, free, e, null, kv)); .)

     |

      SpecBody<out locals, out blocks> ";"

                             (. pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); .)

     )

-  | "ensures"               (. tok = token; .)

+  | "ensures"               (. tok = t; .)

     { Attribute<ref kv> }

     (Proposition<out e> ";"  (. post.Add(new Ensures(tok, free, e, null, kv)); .)

     |

@@ -645,16 +677,16 @@ SpecBlock<out Block! b>
                             cs.Add(c);

                           } else {

                             assert label != null;

-                            SemErr("SpecBlock's can only have one label");

+                            this.SemErr("SpecBlock's can only have one label");

                           }

                        .)

   }

-  ( "goto"             (. y = token; .)

+  ( "goto"             (. y = t; .)

     Idents<out xs>     (. foreach (IToken! s in xs) { ss.Add(s.val); }

                           b = new Block(x,x.val,cs,new GotoCmd(y,ss));

                        .)

   | "return" Expression<out e>

-                       (. b = new Block(x,x.val,cs,new ReturnExprCmd(token,e)); .)

+                       (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .)

   ) ";"

   .

 

@@ -724,9 +756,9 @@ StmtList<out StmtList! stmtList>
   )

   }

   "}"

-  (. IToken! endCurly = token;

+  (. IToken! endCurly = t;

      if (startToken == null && bigblocks.Count == 0) {

-       startToken = token;  cs = new CmdSeq();

+       startToken = t;  cs = new CmdSeq();

      }

      if (startToken != null) {

        assert cs != null;

@@ -743,11 +775,11 @@ TransferCmd<out TransferCmd! tc>
      Token y;  TokenSeq! xs;

      StringSeq ss = new StringSeq();

   .)

-  ( "goto"             (. y = token; .)

+  ( "goto"             (. y = t; .)

     Idents<out xs>     (. foreach (IToken! s in xs) { ss.Add(s.val); }

                           tc = new GotoCmd(y, ss);

                        .)

-  | "return"           (. tc = new ReturnCmd(token); .)

+  | "return"           (. tc = new ReturnCmd(t); .)

   ) ";"

   .

 

@@ -768,7 +800,7 @@ IfCmd<out IfCmd! ifcmd>
      IfCmd! elseIf;  IfCmd elseIfOption = null;

      StmtList! els;  StmtList elseOption = null;

   .)

-  "if"                       (. x = token; .)

+  "if"                       (. x = t; .)

   Guard<out guard>

   "{" StmtList<out thn>

   [ "else"

@@ -786,9 +818,9 @@ WhileCmd<out WhileCmd! wcmd>
      List<PredicateCmd!> invariants = new List<PredicateCmd!>();

      StmtList! body;

   .)

-  "while"             (. x = token; .)

+  "while"             (. x = t; .)

   Guard<out guard>    (. assume guard == null || Owner.None(guard); .)

-  {                   (. isFree = false; z = t/*lookahead token*/; .)

+  {                   (. isFree = false; z = la/*lookahead token*/; .)

     [ "free"          (. isFree = true;  .)

     ]

     "invariant"

@@ -817,7 +849,7 @@ BreakCmd<out BreakCmd! bcmd>
 = (. IToken! x;  IToken! y;

      string breakLabel = null;

   .)

-  "break"             (. x = token; .)

+  "break"             (. x = t; .)

   [ Ident<out y>      (. breakLabel = y.val; .)

   ] ";"               (. bcmd = new BreakCmd(x, breakLabel); .)

   .

@@ -834,14 +866,14 @@ LabelOrCmd<out Cmd c, out IToken label>
      QKeyValue kv = null;

   .)

   ( LabelOrAssign<out c, out label>

-  | "assert"              (. x = token; .)

+  | "assert"              (. x = t; .)

     { Attribute<ref kv> }

     Proposition<out e>    (. c = new AssertCmd(x,e, kv); .)

     ";"

-  | "assume"              (. x = token; .)

+  | "assume"              (. x = t; .)

     Proposition<out e>    (. c = new AssumeCmd(x,e); .)

     ";"

-  | "havoc"               (. x = token; .)

+  | "havoc"               (. x = t; .)

     Idents<out xs> ";"    (. ids = new IdentifierExprSeq();

                              foreach (IToken! y in xs) {

                                ids.Add(new IdentifierExpr(y, y.val));

@@ -862,7 +894,7 @@ LabelOrAssign<out Cmd c, out IToken label>
      List<AssignLhs!>! lhss;

      List<Expr!>! rhss;

   .)

-  Ident<out id>              (. x = token; .)

+  Ident<out id>              (. x = t; .)

   ( ":"                      (. c = null;  label = x; .)

   | 

     MapAssignIndexes<id, out lhs>    (. lhss = new List<AssignLhs!> ();

@@ -871,7 +903,7 @@ LabelOrAssign<out Cmd c, out IToken label>
       Ident<out id>

       MapAssignIndexes<id, out lhs>  (. lhss.Add(lhs); .)

     }

-    ":="                     (. x = token; /* use location of := */ .)

+    ":="                     (. x = t; /* use location of := */ .)

     Expression<out e0>       (. rhss = new List<Expr!> ();

                                 rhss.Add(e0); .)

     { ","

@@ -890,7 +922,7 @@ MapAssignIndexes<IToken! assignedVariable, out AssignLhs! lhs>
      Expr! e0;

   .)

   {

-    "["                        (. x = token;

+    "["                        (. x = t;

                                   indexes = new List<Expr!> (); .)

       [

         Expression<out e0>     (. indexes.Add(e0); .)

@@ -913,7 +945,7 @@ CallCmd<out Cmd! c>
      Expr en;  List<Expr> args;

      c = dummyCmd;

   .)

-  "call"                          (. x = token; .)

+  "call"                          (. x = t; .)

   { Attribute<ref kv> }

   ( Ident<out first>

     ( "("

@@ -1033,7 +1065,7 @@ Expressions<out ExprSeq! es>
 Expression<out Expr! e0>

 = (. IToken! x; Expr! e1; .)

   ImpliesExpression<false, out e0>

-  { EquivOp        (. x = token; .)

+  { EquivOp        (. x = t; .)

     ImpliesExpression<false, out e1>

                    (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); .)

   }

@@ -1046,19 +1078,19 @@ ImpliesExpression<bool noExplies, out Expr! e0>
 = (. IToken! x; Expr! e1; .)

   LogicalExpression<out e0>

   [

-    ImpliesOp      (. x = token; .)

+    ImpliesOp      (. x = t; .)

     /* recurse because implication is right-associative */

     ImpliesExpression<true, out e1>

                    (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); .)

   |

     ExpliesOp      (. if (noExplies)

-                        SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");

-                      x = token; .)

+                        this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");

+                      x = t; .)

     LogicalExpression<out e1> 

                    (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .)

     /* loop because explies is left-associative */

     {

-      ExpliesOp    (. x = token; .)

+      ExpliesOp    (. x = t; .)

       LogicalExpression<out e1> 

                    (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); .)

     }

@@ -1072,17 +1104,17 @@ ExpliesOp = "<==" | '\u21d0'.
 LogicalExpression<out Expr! e0>

 = (. IToken! x; Expr! e1; BinaryOperator.Opcode op; .)

   RelationalExpression<out e0>

-  [ AndOp          (. x = token; .)

+  [ AndOp          (. x = t; .)

     RelationalExpression<out e1>

     (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .)

-    { AndOp        (. x = token; .)

+    { AndOp        (. x = t; .)

       RelationalExpression<out e1>

       (. e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); .)

     }

-  | OrOp           (. x = token; .)

+  | OrOp           (. x = t; .)

     RelationalExpression<out e1>

     (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .)

-    { OrOp         (. x = token; .)

+    { OrOp         (. x = t; .)

       RelationalExpression<out e1>

       (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); .)

     }

@@ -1103,16 +1135,16 @@ RelationalExpression<out Expr! e0>
 

 RelOp<out IToken! x, out BinaryOperator.Opcode op>

 =                  (. x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)

-  ( "=="           (. x = token; op=BinaryOperator.Opcode.Eq; .)

-  | "<"            (. x = token; op=BinaryOperator.Opcode.Lt; .)

-  | ">"            (. x = token; op=BinaryOperator.Opcode.Gt; .)

-  | "<="           (. x = token; op=BinaryOperator.Opcode.Le; .)

-  | ">="           (. x = token; op=BinaryOperator.Opcode.Ge; .)

-  | "!="           (. x = token; op=BinaryOperator.Opcode.Neq; .)

-  | "<:"           (. x = token; op=BinaryOperator.Opcode.Subtype; .)

-  | '\u2260'       (. x = token; op=BinaryOperator.Opcode.Neq; .)

-  | '\u2264'       (. x = token; op=BinaryOperator.Opcode.Le; .)

-  | '\u2265'       (. x = token; op=BinaryOperator.Opcode.Ge; .)

+  ( "=="           (. x = t; op=BinaryOperator.Opcode.Eq; .)

+  | "<"            (. x = t; op=BinaryOperator.Opcode.Lt; .)

+  | ">"            (. x = t; op=BinaryOperator.Opcode.Gt; .)

+  | "<="           (. x = t; op=BinaryOperator.Opcode.Le; .)

+  | ">="           (. x = t; op=BinaryOperator.Opcode.Ge; .)

+  | "!="           (. x = t; op=BinaryOperator.Opcode.Neq; .)

+  | "<:"           (. x = t; op=BinaryOperator.Opcode.Subtype; .)

+  | '\u2260'       (. x = t; op=BinaryOperator.Opcode.Neq; .)

+  | '\u2264'       (. x = t; op=BinaryOperator.Opcode.Le; .)

+  | '\u2265'       (. x = t; op=BinaryOperator.Opcode.Ge; .)

   )

   .

 

@@ -1120,7 +1152,7 @@ RelOp<out IToken! x, out BinaryOperator.Opcode op>
 BvTerm<out Expr! e0>

 = (. IToken! x; Expr! e1; .)

   Term<out e0>

-  { "++"                  (. x = token; .)

+  { "++"                  (. x = t; .)

     Term<out e1>          (. e0 = new BvConcatExpr(x, e0, e1); .)

   }

   .

@@ -1137,8 +1169,8 @@ Term<out Expr! e0>
 

 AddOp<out IToken! x, out BinaryOperator.Opcode op>

 =                  (. x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)

-  ( "+"            (. x = token; op=BinaryOperator.Opcode.Add; .)

-  | "-"            (. x = token; op=BinaryOperator.Opcode.Sub; .)

+  ( "+"            (. x = t; op=BinaryOperator.Opcode.Add; .)

+  | "-"            (. x = t; op=BinaryOperator.Opcode.Sub; .)

   )

   .

 

@@ -1153,9 +1185,9 @@ Factor<out Expr! e0>
 

 MulOp<out IToken! x, out BinaryOperator.Opcode op>

 =                  (. x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; .)

-  ( "*"            (. x = token; op=BinaryOperator.Opcode.Mul; .)

-  | "/"            (. x = token; op=BinaryOperator.Opcode.Div; .)

-  | "%"            (. x = token; op=BinaryOperator.Opcode.Mod; .)

+  ( "*"            (. x = t; op=BinaryOperator.Opcode.Mul; .)

+  | "/"            (. x = t; op=BinaryOperator.Opcode.Div; .)

+  | "%"            (. x = t; op=BinaryOperator.Opcode.Mod; .)

   )

   .

 

@@ -1164,9 +1196,9 @@ UnaryExpression<out Expr! e>
 = (. IToken! x;

      e = dummyExpr;

   .)

-  ( "-"                        (. x = token; .)

+  ( "-"                        (. x = t; .)

     UnaryExpression<out e>     (. e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); .)

-  | NegOp                      (. x = token; .)

+  | NegOp                      (. x = t; .)

     UnaryExpression<out e>     (. e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); .)

   | CoercionExpression<out e>

   )

@@ -1189,14 +1221,14 @@ CoercionExpression<out Expr! e>
      BigNum bn;

     .)

   ArrayExpression<out e>

-  { ":"                     (. x = token; .)

+  { ":"                     (. x = t; .)

     (

       Type<out coercedTo>   (. e = Expr.CoerceType(x, e, coercedTo); .)

     |

       Nat<out bn>           /* This means that we really look at a bitvector

                                expression t[a:b] */

                             (. if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) {

-                                 SemErr("arguments of extract need to be integer literals");

+                                 this.SemErr("arguments of extract need to be integer literals");

                                  e = new BvBounds(x, bn, BigNum.ZERO);

                                } else {

                                  e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);

@@ -1214,7 +1246,7 @@ ArrayExpression<out Expr! e>
      ExprSeq! allArgs = dummyExprSeq;

   .)

   AtomExpression<out e>

-  { "["        (. x = token; allArgs = new ExprSeq ();

+  { "["        (. x = t; allArgs = new ExprSeq ();

                   allArgs.Add(e);

                   store = false; bvExtract = false; .)

       [

@@ -1226,13 +1258,13 @@ ArrayExpression<out Expr! e>
                .)

         { "," Expression<out e1> 

                (. if (bvExtract || e1 is BvBounds)

-                    SemErr("bitvectors only have one dimension");

+                    this.SemErr("bitvectors only have one dimension");

                   allArgs.Add(e1);

                .)

         }

         [ ":=" Expression<out e1> 

                (. if (bvExtract || e1 is BvBounds)

-                    SemErr("assignment to bitvectors is not possible");

+                    this.SemErr("assignment to bitvectors is not possible");

                   allArgs.Add(e1); store = true;

                .)

         ]

@@ -1262,10 +1294,10 @@ AtomExpression<out Expr! e>
      QKeyValue kv;

      e = dummyExpr;

   .)

-  ( "false"           (. e = new LiteralExpr(token, false); .)

-  | "true"            (. e = new LiteralExpr(token, true); .)

-  | Nat<out bn>            (. e = new LiteralExpr(token, bn); .)

-  | BvLit<out bn, out n> (. e = new LiteralExpr(token, bn, n); .)

+  ( "false"           (. e = new LiteralExpr(t, false); .)

+  | "true"            (. e = new LiteralExpr(t, true); .)

+  | Nat<out bn>            (. e = new LiteralExpr(t, bn); .)

+  | BvLit<out bn, out n> (. e = new LiteralExpr(t, bn, n); .)

 

   | Ident<out x>            (. id = new IdentifierExpr(x, x.val);  e = id; .)

     [ "("

@@ -1275,23 +1307,23 @@ AtomExpression<out Expr! e>
       ")"

     ]

 

-  | "old"                   (. x = token; .)

+  | "old"                   (. x = t; .)

     "("

     Expression<out e>

     ")"                     (. e = new OldExpr(x, e); .)

 

   | "(" ( Expression<out e>                 (. if (e is BvBounds)

-                                                 SemErr("parentheses around bitvector bounds " +

+                                                 this.SemErr("parentheses around bitvector bounds " +

                                                         "are not allowed"); .)

-        | Forall                            (. x = token; .)

+        | Forall                            (. x = t; .)

           QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e>

                                             (. if (typeParams.Length + ds.Length > 0)

                                                  e = new ForallExpr(x, typeParams, ds, kv, trig, e); .)

-        | Exists                            (. x = token; .)

+        | Exists                            (. x = t; .)

           QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e> 

                                             (. if (typeParams.Length + ds.Length > 0)

                                                  e = new ExistsExpr(x, typeParams, ds, kv, trig, e); .)

-        | Lambda                            (. x = token; .)

+        | Lambda                            (. x = t; .)

           QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e> 

                                             (. if (trig != null)

                                                  SemErr("triggers not allowed in lambda expressions");

@@ -1305,7 +1337,7 @@ AtomExpression<out Expr! e>
 

 Attribute<ref QKeyValue kv>

 = (. Trigger trig = null; .)

-  AttributeOrTrigger<ref kv, ref trig> (.  if (trig != null) SemErr("only attributes, not triggers, allowed here"); .)

+  AttributeOrTrigger<ref kv, ref trig> (.  if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); .)

 .

 

 AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>

@@ -1313,9 +1345,9 @@ AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>
      string key;  string value;

      List<object!> parameters;  object! param;

   .)

-  "{"                                         (. tok = token; .)

+  "{"                                         (. tok = t; .)

      (

-       ":" ident                              (. key = token.val;  parameters = new List<object!>(); .)

+       ":" ident                              (. key = t.val;  parameters = new List<object!>(); .)

        [ AttributeParameter<out param>        (. parameters.Add(param); .)

          { "," AttributeParameter<out param>  (. parameters.Add(param); .)

          }

@@ -1329,7 +1361,7 @@ AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>
                 trig.AddLast(new Trigger(tok, false, new ExprSeq(e), null));

               }

             } else {

-              SemErr("the 'nopats' quantifier attribute expects a string-literal parameter");

+              this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter");

             }

           } else {

             if (kv==null) {

@@ -1356,7 +1388,7 @@ AttributeParameter<out object! o>
 = (. o = "error";

      Expr! e;

   .)

-  ( string                (. o = token.val.Substring(1, token.val.Length-2); .)

+  ( string                (. o = t.val.Substring(1, t.val.Length-2); .)

   | Expression<out e>     (. o = e; .)

   )

   .

@@ -1365,7 +1397,7 @@ IfThenElseExpression<out Expr! e>
 = (. IToken! tok;

      Expr! e0, e1, e2; 

      e = dummyExpr; .)

-  "if" (. tok = token; .) Expression<out e0> "then" Expression<out e1> "else" Expression<out e2>

+  "if" (. tok = t; .) Expression<out e0> "then" Expression<out e1> "else" Expression<out e2>

   (. e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); .)

   .

 

@@ -1396,7 +1428,7 @@ QSep = "::" | '\u2022'.
 /*------------------------------------------------------------------------*/

 Ident<out IToken! x>

 =

-  ident            (.  x = token;

+  ident            (.  x = t;

                        if (x.val.StartsWith("\\"))

                          x.val = x.val.Substring(1);

                     .)

@@ -1407,9 +1439,9 @@ Nat<out BigNum n>
 =

   digits

   (. try {

-       n = BigNum.FromString(token.val);

+       n = BigNum.FromString(t.val);

      } catch (FormatException) {

-       SemErr("incorrectly formatted number");

+       this.SemErr("incorrectly formatted number");

        n = BigNum.ZERO;

      }

   .)

@@ -1420,14 +1452,14 @@ BvLit<out BigNum n, out int m>
 =

   bvlit

   (.

-     int pos = token.val.IndexOf("bv");

-     string a = token.val.Substring(0, pos);

-     string b = token.val.Substring(pos + 2);

+     int pos = t.val.IndexOf("bv");

+     string a = t.val.Substring(0, pos);

+     string b = t.val.Substring(pos + 2);

      try {

        n = BigNum.FromString(a);

        m = Convert.ToInt32(b);

      } catch (FormatException) {

-       SemErr("incorrectly formatted bitvector");

+       this.SemErr("incorrectly formatted bitvector");

        n = BigNum.ZERO;

        m = 0;

      }

diff --git a/Source/Core/Core.sscproj b/Source/Core/Core.sscproj
index 91bbaf47..4929e1c7 100644
--- a/Source/Core/Core.sscproj
+++ b/Source/Core/Core.sscproj
@@ -172,6 +172,10 @@
                  />

         <File BuildAction="Compile"

                  SubType="Code"

+                 RelPath="ParserHelper.ssc"

+                 />

+        <File BuildAction="Compile"

+                 SubType="Code"

                  RelPath="GraphAlgorithms.ssc"

                  />

         <File BuildAction="Compile"

diff --git a/Source/Core/Makefile b/Source/Core/Makefile
index ee73b25d..d7236a5b 100644
--- a/Source/Core/Makefile
+++ b/Source/Core/Makefile
@@ -1,6 +1,11 @@
 COCO = ..\..\Binaries\Coco.exe

 ASML = ..\..\Binaries\asmlc.boot.exe

 

+# ###############################################################################

+# The frame files are no longer in this directory. They must be downloaded

+# from http://boogiepartners.codeplex.com/ and then copied into this directory.

+# ###############################################################################

+

 # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they

 # are both generated in one go and I don't know a better way to tell

 # nmake that.  --KRML

@@ -10,7 +15,7 @@ all: Parser.ssc
 #  $(ASML) /target:library Graph.as

   

 Parser.ssc: Scanner.frame Parser.frame BoogiePL.atg

-	$(COCO) BoogiePL.atg

+	$(COCO) BoogiePL.atg -namespace Microsoft.Boogie

 	copy Parser.cs Parser.ssc

 	copy Scanner.cs Scanner.ssc

 

diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc
index 60b441cf..f23e0f9e 100644
--- a/Source/Core/Parser.ssc
+++ b/Source/Core/Parser.ssc
@@ -1,27 +1,44 @@
 using PureCollections;

 using System.Collections;

 using System.Collections.Generic;

+using System.IO;

+using System.Text;

 using Microsoft.Boogie;

 using Microsoft.Basetypes;

 using Bpl = Microsoft.Boogie;

 using AI = Microsoft.AbstractInterpretationFramework;

+

+

+

+

 using System;

 using Microsoft.Contracts;

 

-namespace BoogiePL {

+namespace Microsoft.Boogie {

+

+

 

 public class Parser {

-	const int maxT = 88;

+	public const int _EOF = 0;

+	public const int _ident = 1;

+	public const int _bvlit = 2;

+	public const int _digits = 3;

+	public const int _string = 4;

+	public const int _float = 5;

+	public const int maxT = 88;

 

 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

 	

-	static Token/*!*/ token;			// last recognized token

-	static Token/*!*/ t;				// lookahead token

-	static int errDist = minErrDist;

+	public Scanner/*!*/ scanner;

+	public Errors/*!*/  errors;

+

+	public Token/*!*/ t;    // last recognized token

+	public Token/*!*/ la;   // lookahead token

+	int errDist = minErrDist;

 

-	static Program! Pgm = new Program();

+static Program! Pgm = new Program();

 

 static Expr! dummyExpr = new LiteralExpr(Token.NoToken, false);

 static Cmd! dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);

@@ -37,22 +54,24 @@ static StructuredCmd! dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
 ///the parsed program.

 ///</summary>

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

-  using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

-    Buffer.Fill(reader);

-    Scanner.Init(filename);

-    return Parse(out program);

-  }

-}

 

-///<summary>

-///Returns the number of parsing errors encountered.  If 0, "program" returns as

-///the parsed program.

-///Note: first initialize the Scanner.

-///</summary>

-public static int Parse (out /*maybe null*/ Program program) {

+

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

+//  Scanner scanner = new Scanner(stream);

+  

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

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

+  MemoryStream ms = new MemoryStream(buffer,false);

+  Errors errors = new Errors();

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

+

+/*  

+  Scanner scanner = new Scanner(filename);

+*/

+  Parser parser = new Parser(scanner, errors);

   Pgm = new Program(); // reset the global variable

-    Parse();

-    if (Errors.count == 0)

+    parser.Parse();

+    if (parser.errors.count == 0)

     {

       program = Pgm;

       return 0;

@@ -60,22 +79,50 @@ public static int Parse (out /*maybe null*/ Program program) {
     else

     {

       program = null;

-      return Errors.count;

+      return parser.errors.count;

     }

+/*

+  using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {

+    Buffer.Fill(reader);

+    Scanner.Init(filename);

+    return Parse(out program);

+  }

+*/

 }

 

-

+///<summary>

+///Returns the number of parsing errors encountered.  If 0, "program" returns as

+///the parsed program.

+///Note: first initialize the Scanner.

+///</summary>

+//public static int Parse (out /*maybe null*/ Program program) {

+//  Pgm = new Program(); // reset the global variable

+//    Parse();

+//    if (Errors.count == 0)

+//    {

+//      program = Pgm;

+//      return 0;

+//    }

+//    else

+//    {

+//      program = null;

+//      return Errors.count;

+//    }

+//}

+

+/*

 public static int ParseProposition (string! text, out Expr! expression)

 {

   Buffer.Fill(text);

   Scanner.Init(string.Format("\"{0}\"", text));

 

   Errors.SynErr = new ErrorProc(SynErr);

-  t = new Token();

+  la = new Token();

   Get();

   Proposition(out expression);

   return Errors.count;

 }

+*/

 

 // Class to represent the bounds of a bitvector expression t[a:b].

 // Objects of this class only exist during parsing and are directly

@@ -103,61 +150,72 @@ private class BvBounds : Expr {
 /*--------------------------------------------------------------------------*/

 

 

-	static void Error(int n) {

-		if (errDist >= minErrDist) Errors.SynErr(n, t.filename, t.line, t.col);

-		errDist = 0;

+	public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) {

+		this.scanner = scanner;

+		this.errors = errors;

+		Token! tok = new Token();

+		tok.val = "";

+		this.la = tok;

+		this.t = new Token(); // just to satisfy its non-null constraint

 	}

-	

-	public static void SemErr(string! msg) {

-		if (errDist >= minErrDist) Errors.SemErr(token.filename, token.line, token.col, msg);

+

+	void SynErr (int n) {

+		if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n);

 		errDist = 0;

 	}

 

-	public static void SemErr(IToken! tok, string! msg) {

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

+	public void SemErr (string! msg) {

+		if (errDist >= minErrDist) errors.SemErr(t, msg);

+		errDist = 0;

+	}

+	

+    public void SemErr(IToken! tok, string! msg) {

+	  errors.SemErr(tok, msg);

 	}

 

-	static void Get() {

+	void Get () {

 		for (;;) {

-			token = t;

-			t = Scanner.Scan();

-			if (t.kind<=maxT) {errDist++; return;}

+			t = la;

+			la = scanner.Scan();

+			if (la.kind <= maxT) { ++errDist; break; }

 

-			t = token;

+			la = t;

 		}

 	}

 	

-	static void Expect(int n) {

-		if (t.kind==n) Get(); else Error(n);

+	void Expect (int n) {

+		if (la.kind==n) Get(); else { SynErr(n); }

 	}

 	

-	static bool StartOf(int s) {

-		return set[s, t.kind];

+	bool StartOf (int s) {

+		return set[s, la.kind];

 	}

 	

-	static void ExpectWeak(int n, int follow) {

-		if (t.kind == n) Get();

+	void ExpectWeak (int n, int follow) {

+		if (la.kind == n) Get();

 		else {

-			Error(n);

+			SynErr(n);

 			while (!StartOf(follow)) Get();

 		}

 	}

-	

-	static bool WeakSeparator(int n, int syFol, int repFol) {

-		bool[] s = new bool[maxT+1];

-		if (t.kind == n) {Get(); return true;}

-		else if (StartOf(repFol)) return false;

+

+

+	bool WeakSeparator(int n, int syFol, int repFol) {

+		int kind = la.kind;

+		if (kind == n) {Get(); return true;}

+		else if (StartOf(repFol)) {return false;}

 		else {

-			for (int i=0; i <= maxT; i++) {

-				s[i] = set[syFol, i] || set[repFol, i] || set[0, i];

+			SynErr(n);

+			while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) {

+				Get();

+				kind = la.kind;

 			}

-			Error(n);

-			while (!s[t.kind]) Get();

 			return StartOf(syFol);

 		}

 	}

+

 	

-	static void BoogiePL() {

+	void BoogiePL() {

 		VariableSeq! vs;

 		DeclarationSeq! ds;

 		Axiom! ax;

@@ -167,7 +225,7 @@ private class BvBounds : Expr {
 		Implementation! nnim;

 		

 		while (StartOf(1)) {

-			switch (t.kind) {

+			switch (la.kind) {

 			case 19: {

 				Consts(out vs);

 				foreach (Bpl.Variable! v in vs) { Pgm.TopLevelDeclarations.Add(v); } 

@@ -214,46 +272,48 @@ private class BvBounds : Expr {
 		Expect(0);

 	}

 

-	static void Consts(out VariableSeq! ds) {

+	void Consts(out VariableSeq! ds) {

 		IToken! y; TypedIdentSeq! xs;

 		ds = new VariableSeq();

 		bool u = false; QKeyValue kv = null;

 		bool ChildrenComplete = false;

 		List<ConstantParent!> Parents = null; 

 		Expect(19);

-		y = token; 

-		while (t.kind == 25) {

+		y = t; 

+		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

-		if (t.kind == 20) {

+		if (la.kind == 20) {

 			Get();

 			u = true;  

 		}

 		IdsType(out xs);

-		if (t.kind == 21) {

+		if (la.kind == 21) {

 			OrderSpec(out ChildrenComplete, out Parents);

 		}

 		bool makeClone = false;

 		foreach(TypedIdent! x in xs) {

-		    // ensure that no sharing is introduced

-		  List<ConstantParent!> ParentsClone;

-		  if (makeClone && Parents != null) {

-		    ParentsClone = new List<ConstantParent!> ();

-		    foreach (ConstantParent! p in Parents)

-		      ParentsClone.Add(new ConstantParent (

-		                       new IdentifierExpr (p.Parent.tok, p.Parent.Name),

-		                       p.Unique));

-		  } else {

-		    ParentsClone = Parents;

-		  }

-		  makeClone = true;

-		    ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));

-		}

 		

+		       // ensure that no sharing is introduced

+		       List<ConstantParent!> ParentsClone;

+		       if (makeClone && Parents != null) {

+		         ParentsClone = new List<ConstantParent!> ();

+		         foreach (ConstantParent! p in Parents)

+		           ParentsClone.Add(new ConstantParent (

+		                            new IdentifierExpr (p.Parent.tok, p.Parent.Name),

+		                            p.Unique));

+		       } else {

+		         ParentsClone = Parents;

+		       }

+		       makeClone = true;

+		

+		       ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));

+		     }

+		  

 		Expect(7);

 	}

 

-	static void Function(out DeclarationSeq! ds) {

+	void Function(out DeclarationSeq! ds) {

 		ds = new DeclarationSeq(); IToken! z;

 		IToken! typeParamTok;

 		TypeVariableSeq! typeParams = new TypeVariableSeq();

@@ -266,46 +326,46 @@ private class BvBounds : Expr {
 		Expr! tmp;

 		

 		Expect(23);

-		while (t.kind == 25) {

+		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

 		Ident(out z);

-		if (t.kind == 17) {

+		if (la.kind == 17) {

 			TypeParams(out typeParamTok, out typeParams);

 		}

 		Expect(8);

 		if (StartOf(2)) {

 			VarOrType(out tyd);

 			arguments.Add(new Formal(tyd.tok, tyd, true)); 

-			while (t.kind == 11) {

+			while (la.kind == 11) {

 				Get();

 				VarOrType(out tyd);

 				arguments.Add(new Formal(tyd.tok, tyd, true)); 

 			}

 		}

 		Expect(9);

-		if (t.kind == 24) {

+		if (la.kind == 24) {

 			Get();

 			Expect(8);

 			VarOrType(out tyd);

 			Expect(9);

 			retTyd = tyd; 

-		} else if (t.kind == 10) {

+		} else if (la.kind == 10) {

 			Get();

 			Type(out retTy);

 			retTyd = new TypedIdent(retTy.tok, "", retTy); 

-		} else Error(89);

-		if (t.kind == 25) {

+		} else SynErr(89);

+		if (la.kind == 25) {

 			Get();

 			Expression(out tmp);

 			definition = tmp; 

 			Expect(26);

-		} else if (t.kind == 7) {

+		} else if (la.kind == 7) {

 			Get();

-		} else Error(90);

+		} else SynErr(90);

 		if (retTyd == null) {

 		 // construct a dummy type for the case of syntax error

-		 tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));

+		 tyd = new TypedIdent(t, "", new BasicType(t, SimpleType.Int));

 		} else {

 		  tyd = retTyd;

 		}

@@ -325,7 +385,7 @@ private class BvBounds : Expr {
 		       TypedIdent! curr = ((!)arguments[i]).TypedIdent;

 		       if (curr.Name == "") {

 		  if (prevType == null) {

-		    SemErr(curr.tok, "the type of the last parameter is unspecified");

+		    this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");

 		    break;

 		  }

 		  Type ty = curr.Type;

@@ -334,7 +394,7 @@ private class BvBounds : Expr {
 		    curr.Name = ((!)(ty as UnresolvedTypeIdentifier)).Name;

 		    curr.Type = prevType;

 		  } else {

-		    SemErr(curr.tok, "expecting an identifier as parameter name");

+		    this.errors.SemErr(curr.tok, "expecting an identifier as parameter name");

 		  }

 		} else {

 		  prevType = curr.Type;

@@ -359,44 +419,44 @@ private class BvBounds : Expr {
 		       foreach (TypeVariable! t in typeParams)

 		         quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));

 		

-		       Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);

-		       // specify the type of the function, because it might be that

-		       // type parameters only occur in the output type

-		       call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());

-			    Expr def = Expr.Eq(call, definition);

-			    if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

-			      def = new ForallExpr(z, quantifiedTypeVars, dummies, 

-			                           kv, 

-			                           new Trigger(z, true, new ExprSeq(call), null),

-			                           def);

-			    }

-		       ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));

-		     }

-		   }

-		 

-	}

-

-	static void Axiom(out Axiom! m) {

+		        Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);

+		        // specify the type of the function, because it might be that

+		        // type parameters only occur in the output type

+		        call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());

+				    Expr def = Expr.Eq(call, definition);

+				    if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

+				      def = new ForallExpr(z, quantifiedTypeVars, dummies, 

+				                           kv, 

+				                           new Trigger(z, true, new ExprSeq(call), null),

+				                           def);

+				    }

+		        ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));

+		      }

+		    }

+		  

+	}

+

+	void Axiom(out Axiom! m) {

 		Expr! e; QKeyValue kv = null; 

 		Expect(27);

-		while (t.kind == 25) {

+		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

-		IToken! x = token; 

+		IToken! x = t; 

 		Proposition(out e);

 		Expect(7);

 		m = new Axiom(x,e, null, kv); 

 	}

 

-	static void UserDefinedTypes(out List<Declaration!>! ts) {

+	void UserDefinedTypes(out List<Declaration!>! ts) {

 		Declaration! decl; QKeyValue kv = null; ts = new List<Declaration!> (); 

 		Expect(28);

-		while (t.kind == 25) {

+		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

 		UserDefinedType(out decl, kv);

 		ts.Add(decl);  

-		while (t.kind == 11) {

+		while (la.kind == 11) {

 			Get();

 			UserDefinedType(out decl, kv);

 			ts.Add(decl);  

@@ -404,10 +464,10 @@ private class BvBounds : Expr {
 		Expect(7);

 	}

 

-	static void GlobalVars(out VariableSeq! ds) {

+	void GlobalVars(out VariableSeq! ds) {

 		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null; 

 		Expect(6);

-		while (t.kind == 25) {

+		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

 		IdsTypeWheres(true, tyds);

@@ -418,21 +478,22 @@ private class BvBounds : Expr {
 		

 	}

 

-	static void Procedure(out Procedure! proc, out /*maybe null*/ Implementation impl) {

+	void Procedure(out Procedure! proc, out /*maybe null*/ Implementation impl) {

 		IToken! x;

 		TypeVariableSeq! typeParams;

 		VariableSeq! ins, outs;

 		RequiresSeq! pre = new RequiresSeq();

 		IdentifierExprSeq! mods = new IdentifierExprSeq();

 		EnsuresSeq! post = new EnsuresSeq();

-		  VariableSeq! locals = new VariableSeq();

-		StmtList! stmtList;

-		QKeyValue kv = null;

-		impl = null;

 		

+		     VariableSeq! locals = new VariableSeq();

+		     StmtList! stmtList;

+		     QKeyValue kv = null;

+		     impl = null;

+		  

 		Expect(30);

 		ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);

-		if (t.kind == 7) {

+		if (la.kind == 7) {

 			Get();

 			while (StartOf(3)) {

 				Spec(pre, mods, post);

@@ -442,15 +503,14 @@ private class BvBounds : Expr {
 				Spec(pre, mods, post);

 			}

 			ImplBody(out locals, out stmtList);

-			// here we attach kv only to the Procedure, not its implementation

 			impl = new Implementation(x, x.val, typeParams,

-			                          Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null); 

+			                         Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors); 

 			

-		} else Error(91);

+		} else SynErr(91);

 		proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); 

 	}

 

-	static void Implementation(out Implementation! impl) {

+	void Implementation(out Implementation! impl) {

 		IToken! x;

 		TypeVariableSeq! typeParams;

 		VariableSeq! ins, outs;

@@ -461,27 +521,27 @@ private class BvBounds : Expr {
 		Expect(31);

 		ProcSignature(false, out x, out typeParams, out ins, out outs, out kv);

 		ImplBody(out locals, out stmtList);

-		impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv); 

+		impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); 

 	}

 

-	static void Attribute(ref QKeyValue kv) {

+	void Attribute(ref QKeyValue kv) {

 		Trigger trig = null; 

 		AttributeOrTrigger(ref kv, ref trig);

-		if (trig != null) SemErr("only attributes, not triggers, allowed here"); 

+		if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); 

 	}

 

-	static void IdsTypeWheres(bool allowWhereClauses, TypedIdentSeq! tyds) {

+	void IdsTypeWheres(bool allowWhereClauses, TypedIdentSeq! tyds) {

 		IdsTypeWhere(allowWhereClauses, tyds);

-		while (t.kind == 11) {

+		while (la.kind == 11) {

 			Get();

 			IdsTypeWhere(allowWhereClauses, tyds);

 		}

 	}

 

-	static void LocalVars(VariableSeq! ds) {

+	void LocalVars(VariableSeq! ds) {

 		TypedIdentSeq! tyds = new TypedIdentSeq(); QKeyValue kv = null; 

 		Expect(6);

-		while (t.kind == 25) {

+		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

 		IdsTypeWheres(true, tyds);

@@ -492,10 +552,10 @@ private class BvBounds : Expr {
 		

 	}

 

-	static void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq! ds) {

+	void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq! ds) {

 		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); 

 		Expect(8);

-		if (t.kind == 1) {

+		if (la.kind == 1) {

 			IdsTypeWheres(allowWhereClauses, tyds);

 		}

 		Expect(9);

@@ -505,7 +565,7 @@ private class BvBounds : Expr {
 		

 	}

 

-	static void BoundVars(IToken! x, out VariableSeq! ds) {

+	void BoundVars(IToken! x, out VariableSeq! ds) {

 		TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); 

 		IdsTypeWheres(false, tyds);

 		foreach (TypedIdent! tyd in tyds) {

@@ -514,7 +574,7 @@ private class BvBounds : Expr {
 		

 	}

 

-	static void IdsType(out TypedIdentSeq! tyds) {

+	void IdsType(out TypedIdentSeq! tyds) {

 		TokenSeq! ids;  Bpl.Type! ty; 

 		Idents(out ids);

 		Expect(10);

@@ -526,45 +586,45 @@ private class BvBounds : Expr {
 		

 	}

 

-	static void Idents(out TokenSeq! xs) {

+	void Idents(out TokenSeq! xs) {

 		IToken! id; xs = new TokenSeq(); 

 		Ident(out id);

 		xs.Add(id); 

-		while (t.kind == 11) {

+		while (la.kind == 11) {

 			Get();

 			Ident(out id);

 			xs.Add(id); 

 		}

 	}

 

-	static void Type(out Bpl.Type! ty) {

+	void Type(out Bpl.Type! ty) {

 		IToken! tok; ty = dummyType; 

-		if (t.kind == 8 || t.kind == 13 || t.kind == 14) {

+		if (la.kind == 8 || la.kind == 13 || la.kind == 14) {

 			TypeAtom(out ty);

-		} else if (t.kind == 1) {

+		} else if (la.kind == 1) {

 			Ident(out tok);

 			TypeSeq! args = new TypeSeq (); 

 			if (StartOf(2)) {

 				TypeArgs(args);

 			}

 			ty = new UnresolvedTypeIdentifier (tok, tok.val, args); 

-		} else if (t.kind == 15 || t.kind == 17) {

+		} else if (la.kind == 15 || la.kind == 17) {

 			MapType(out ty);

-		} else Error(92);

+		} else SynErr(92);

 	}

 

-	static void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {

+	void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {

 		TokenSeq! ids;  Bpl.Type! ty;  Expr wh = null;  Expr! nne; 

 		Idents(out ids);

 		Expect(10);

 		Type(out ty);

-		if (t.kind == 12) {

+		if (la.kind == 12) {

 			Get();

 			Expression(out nne);

 			if (allowWhereClauses) {

 			 wh = nne;

 			} else {

-			  SemErr("where clause not allowed here");

+			  this.SemErr("where clause not allowed here");

 			}

 			

 		}

@@ -574,74 +634,74 @@ private class BvBounds : Expr {
 		

 	}

 

-	static void Expression(out Expr! e0) {

+	void Expression(out Expr! e0) {

 		IToken! x; Expr! e1; 

 		ImpliesExpression(false, out e0);

-		while (t.kind == 52 || t.kind == 53) {

+		while (la.kind == 52 || la.kind == 53) {

 			EquivOp();

-			x = token; 

+			x = t; 

 			ImpliesExpression(false, out e1);

 			e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); 

 		}

 	}

 

-	static void TypeAtom(out Bpl.Type! ty) {

+	void TypeAtom(out Bpl.Type! ty) {

 		ty = dummyType; 

-		if (t.kind == 13) {

+		if (la.kind == 13) {

 			Get();

-			ty = new BasicType(token, SimpleType.Int); 

-		} else if (t.kind == 14) {

+			ty = new BasicType(t, SimpleType.Int); 

+		} else if (la.kind == 14) {

 			Get();

-			ty = new BasicType(token, SimpleType.Bool); 

-		} else if (t.kind == 8) {

+			ty = new BasicType(t, SimpleType.Bool); 

+		} else if (la.kind == 8) {

 			Get();

 			Type(out ty);

 			Expect(9);

-		} else Error(93);

+		} else SynErr(93);

 	}

 

-	static void Ident(out IToken! x) {

+	void Ident(out IToken! x) {

 		Expect(1);

-		x = token;

+		x = t;

 		if (x.val.StartsWith("\\"))

 		  x.val = x.val.Substring(1);

 		

 	}

 

-	static void TypeArgs(TypeSeq! ts) {

+	void TypeArgs(TypeSeq! ts) {

 		IToken! tok; Type! ty; 

-		if (t.kind == 8 || t.kind == 13 || t.kind == 14) {

+		if (la.kind == 8 || la.kind == 13 || la.kind == 14) {

 			TypeAtom(out ty);

 			ts.Add(ty); 

 			if (StartOf(2)) {

 				TypeArgs(ts);

 			}

-		} else if (t.kind == 1) {

+		} else if (la.kind == 1) {

 			Ident(out tok);

 			TypeSeq! args = new TypeSeq ();

 			ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); 

 			if (StartOf(2)) {

 				TypeArgs(ts);

 			}

-		} else if (t.kind == 15 || t.kind == 17) {

+		} else if (la.kind == 15 || la.kind == 17) {

 			MapType(out ty);

 			ts.Add(ty); 

-		} else Error(94);

+		} else SynErr(94);

 	}

 

-	static void MapType(out Bpl.Type! ty) {

+	void MapType(out Bpl.Type! ty) {

 		IToken tok = null;

 		IToken! nnTok;

 		TypeSeq! arguments = new TypeSeq();

 		Type! result;

 		TypeVariableSeq! typeParameters = new TypeVariableSeq();

 		

-		if (t.kind == 17) {

+		if (la.kind == 17) {

 			TypeParams(out nnTok, out typeParameters);

 			tok = nnTok; 

 		}

 		Expect(15);

-		if (tok == null) tok = token;  

+		if (tok == null) tok = t;  

 		if (StartOf(2)) {

 			Types(arguments);

 		}

@@ -651,10 +711,10 @@ private class BvBounds : Expr {
 		

 	}

 

-	static void TypeParams(out IToken! tok, out Bpl.TypeVariableSeq! typeParams) {

+	void TypeParams(out IToken! tok, out Bpl.TypeVariableSeq! typeParams) {

 		TokenSeq! typeParamToks; 

 		Expect(17);

-		tok = token;  

+		tok = t;  

 		Idents(out typeParamToks);

 		Expect(18);

 		typeParams = new TypeVariableSeq ();

@@ -663,18 +723,18 @@ private class BvBounds : Expr {
 		

 	}

 

-	static void Types(TypeSeq! ts) {

+	void Types(TypeSeq! ts) {

 		Bpl.Type! ty; 

 		Type(out ty);

 		ts.Add(ty); 

-		while (t.kind == 11) {

+		while (la.kind == 11) {

 			Get();

 			Type(out ty);

 			ts.Add(ty); 

 		}

 	}

 

-	static void OrderSpec(out bool ChildrenComplete, out List<ConstantParent!> Parents) {

+	void OrderSpec(out bool ChildrenComplete, out List<ConstantParent!> Parents) {

 		ChildrenComplete = false;

 		Parents = null;

 		bool u;

@@ -682,18 +742,18 @@ private class BvBounds : Expr {
 		Expect(21);

 		Parents = new List<ConstantParent!> ();

 		u = false; 

-		if (t.kind == 1 || t.kind == 20) {

-			if (t.kind == 20) {

+		if (la.kind == 1 || la.kind == 20) {

+			if (la.kind == 20) {

 				Get();

 				u = true; 

 			}

 			Ident(out parent);

 			Parents.Add(new ConstantParent (

 			           new IdentifierExpr(parent, parent.val), u)); 

-			while (t.kind == 11) {

+			while (la.kind == 11) {

 				Get();

 				u = false; 

-				if (t.kind == 20) {

+				if (la.kind == 20) {

 					Get();

 					u = true; 

 				}

@@ -702,23 +762,23 @@ private class BvBounds : Expr {
 				           new IdentifierExpr(parent, parent.val), u)); 

 			}

 		}

-		if (t.kind == 22) {

+		if (la.kind == 22) {

 			Get();

 			ChildrenComplete = true; 

 		}

 	}

 

-	static void VarOrType(out TypedIdent! tyd) {

+	void VarOrType(out TypedIdent! tyd) {

 		string! varName = ""; Bpl.Type! ty; IToken! tok; 

 		Type(out ty);

 		tok = ty.tok; 

-		if (t.kind == 10) {

+		if (la.kind == 10) {

 			Get();

 			if (ty is UnresolvedTypeIdentifier &&

 			   ((!)(ty as UnresolvedTypeIdentifier)).Arguments.Length == 0) {

 			 varName = ((!)(ty as UnresolvedTypeIdentifier)).Name;

 			} else {

-			  SemErr("expected identifier before ':'");

+			  this.SemErr("expected identifier before ':'");

 			}

 			

 			Type(out ty);

@@ -726,18 +786,18 @@ private class BvBounds : Expr {
 		tyd = new TypedIdent(tok, varName, ty); 

 	}

 

-	static void Proposition(out Expr! e) {

+	void Proposition(out Expr! e) {

 		Expression(out e);

 	}

 

-	static void UserDefinedType(out Declaration! decl, QKeyValue kv) {

+	void UserDefinedType(out Declaration! decl, QKeyValue kv) {

 		IToken! id; IToken! id2; TokenSeq! paramTokens = new TokenSeq ();

 		Type! body = dummyType; bool synonym = false; 

 		Ident(out id);

-		if (t.kind == 1) {

+		if (la.kind == 1) {

 			WhiteSpaceIdents(out paramTokens);

 		}

-		if (t.kind == 29) {

+		if (la.kind == 29) {

 			Get();

 			Type(out body);

 			synonym = true; 

@@ -753,39 +813,39 @@ private class BvBounds : Expr {
 		

 	}

 

-	static void WhiteSpaceIdents(out TokenSeq! xs) {

+	void WhiteSpaceIdents(out TokenSeq! xs) {

 		IToken! id; xs = new TokenSeq(); 

 		Ident(out id);

 		xs.Add(id); 

-		while (t.kind == 1) {

+		while (la.kind == 1) {

 			Ident(out id);

 			xs.Add(id); 

 		}

 	}

 

-	static void ProcSignature(bool allowWhereClausesOnFormals, out IToken! name, out TypeVariableSeq! typeParams,

+	void ProcSignature(bool allowWhereClausesOnFormals, out IToken! name, out TypeVariableSeq! typeParams,

 out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {

 		IToken! typeParamTok; typeParams = new TypeVariableSeq();

 		outs = new VariableSeq(); kv = null; 

-		while (t.kind == 25) {

+		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

 		Ident(out name);

-		if (t.kind == 17) {

+		if (la.kind == 17) {

 			TypeParams(out typeParamTok, out typeParams);

 		}

 		ProcFormals(true, allowWhereClausesOnFormals, out ins);

-		if (t.kind == 24) {

+		if (la.kind == 24) {

 			Get();

 			ProcFormals(false, allowWhereClausesOnFormals, out outs);

 		}

 	}

 

-	static void Spec(RequiresSeq! pre, IdentifierExprSeq! mods, EnsuresSeq! post) {

+	void Spec(RequiresSeq! pre, IdentifierExprSeq! mods, EnsuresSeq! post) {

 		TokenSeq! ms; 

-		if (t.kind == 32) {

+		if (la.kind == 32) {

 			Get();

-			if (t.kind == 1) {

+			if (la.kind == 1) {

 				Idents(out ms);

 				foreach (IToken! m in ms) {

 				 mods.Add(new IdentifierExpr(m, m.val));

@@ -793,74 +853,74 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				

 			}

 			Expect(7);

-		} else if (t.kind == 33) {

+		} else if (la.kind == 33) {

 			Get();

 			SpecPrePost(true, pre, post);

-		} else if (t.kind == 34 || t.kind == 35) {

+		} else if (la.kind == 34 || la.kind == 35) {

 			SpecPrePost(false, pre, post);

-		} else Error(95);

+		} else SynErr(95);

 	}

 

-	static void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {

+	void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {

 		locals = new VariableSeq(); 

 		Expect(25);

-		while (t.kind == 6) {

+		while (la.kind == 6) {

 			LocalVars(locals);

 		}

 		StmtList(out stmtList);

 	}

 

-	static void SpecPrePost(bool free, RequiresSeq! pre, EnsuresSeq! post) {

+	void SpecPrePost(bool free, RequiresSeq! pre, EnsuresSeq! post) {

 		Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null; 

-		if (t.kind == 34) {

+		if (la.kind == 34) {

 			Get();

-			tok = token; 

-			while (t.kind == 25) {

+			tok = t; 

+			while (la.kind == 25) {

 				Attribute(ref kv);

 			}

 			if (StartOf(5)) {

 				Proposition(out e);

 				Expect(7);

 				pre.Add(new Requires(tok, free, e, null, kv)); 

-			} else if (t.kind == 36) {

+			} else if (la.kind == 36) {

 				SpecBody(out locals, out blocks);

 				Expect(7);

 				pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); 

-			} else Error(96);

-		} else if (t.kind == 35) {

+			} else SynErr(96);

+		} else if (la.kind == 35) {

 			Get();

-			tok = token; 

-			while (t.kind == 25) {

+			tok = t; 

+			while (la.kind == 25) {

 				Attribute(ref kv);

 			}

 			if (StartOf(5)) {

 				Proposition(out e);

 				Expect(7);

 				post.Add(new Ensures(tok, free, e, null, kv)); 

-			} else if (t.kind == 36) {

+			} else if (la.kind == 36) {

 				SpecBody(out locals, out blocks);

 				Expect(7);

 				post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv)); 

-			} else Error(97);

-		} else Error(98);

+			} else SynErr(97);

+		} else SynErr(98);

 	}

 

-	static void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {

+	void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {

 		locals = new VariableSeq(); Block! b; 

 		Expect(36);

-		while (t.kind == 6) {

+		while (la.kind == 6) {

 			LocalVars(locals);

 		}

 		SpecBlock(out b);

 		blocks = new BlockSeq(b); 

-		while (t.kind == 1) {

+		while (la.kind == 1) {

 			SpecBlock(out b);

 			blocks.Add(b); 

 		}

 		Expect(37);

 	}

 

-	static void SpecBlock(out Block! b) {

+	void SpecBlock(out Block! b) {

 		IToken! x; IToken! y;

 		Cmd c;  IToken label;

 		CmdSeq cs = new CmdSeq();

@@ -878,26 +938,26 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			 cs.Add(c);

 			} else {

 			  assert label != null;

-			  SemErr("SpecBlock's can only have one label");

+			  this.SemErr("SpecBlock's can only have one label");

 			}

 			

 		}

-		if (t.kind == 38) {

+		if (la.kind == 38) {

 			Get();

-			y = token; 

+			y = t; 

 			Idents(out xs);

 			foreach (IToken! s in xs) { ss.Add(s.val); }

 			b = new Block(x,x.val,cs,new GotoCmd(y,ss));

 			

-		} else if (t.kind == 39) {

+		} else if (la.kind == 39) {

 			Get();

 			Expression(out e);

-			b = new Block(x,x.val,cs,new ReturnExprCmd(token,e)); 

-		} else Error(99);

+			b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); 

+		} else SynErr(99);

 		Expect(7);

 	}

 

-	static void LabelOrCmd(out Cmd c, out IToken label) {

+	void LabelOrCmd(out Cmd c, out IToken label) {

 		IToken! x; Expr! e;

 		TokenSeq! xs;

 		IdentifierExprSeq ids;

@@ -905,26 +965,26 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		Cmd! cn;

 		QKeyValue kv = null;

 		

-		if (t.kind == 1) {

+		if (la.kind == 1) {

 			LabelOrAssign(out c, out label);

-		} else if (t.kind == 46) {

+		} else if (la.kind == 46) {

 			Get();

-			x = token; 

-			while (t.kind == 25) {

+			x = t; 

+			while (la.kind == 25) {

 				Attribute(ref kv);

 			}

 			Proposition(out e);

 			c = new AssertCmd(x,e, kv); 

 			Expect(7);

-		} else if (t.kind == 47) {

+		} else if (la.kind == 47) {

 			Get();

-			x = token; 

+			x = t; 

 			Proposition(out e);

 			c = new AssumeCmd(x,e); 

 			Expect(7);

-		} else if (t.kind == 48) {

+		} else if (la.kind == 48) {

 			Get();

-			x = token; 

+			x = t; 

 			Idents(out xs);

 			Expect(7);

 			ids = new IdentifierExprSeq();

@@ -933,14 +993,14 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			}

 			c = new HavocCmd(x,ids);

 			

-		} else if (t.kind == 50) {

+		} else if (la.kind == 50) {

 			CallCmd(out cn);

 			Expect(7);

 			c = cn; 

-		} else Error(100);

+		} else SynErr(100);

 	}

 

-	static void StmtList(out StmtList! stmtList) {

+	void StmtList(out StmtList! stmtList) {

 		List<BigBlock!> bigblocks = new List<BigBlock!>();

 		/* built-up state for the current BigBlock: */

 		IToken startToken = null;  string currentLabel = null;

@@ -974,7 +1034,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				  cs = new CmdSeq();

 				}

 				

-			} else if (t.kind == 40 || t.kind == 42 || t.kind == 45) {

+			} else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {

 				StructuredCmd(out ecn);

 				ec = ecn;

 				if (startToken == null) { startToken = ec.tok;  cs = new CmdSeq(); }

@@ -995,55 +1055,56 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			}

 		}

 		Expect(26);

-		IToken! endCurly = token;

+		IToken! endCurly = t;

 		if (startToken == null && bigblocks.Count == 0) {

-		  startToken = token;  cs = new CmdSeq();

+		  startToken = t;  cs = new CmdSeq();

 		}

 		if (startToken != null) {

 		  assert cs != null;

 		  b = new BigBlock(startToken, currentLabel, cs, null, null);

 		  bigblocks.Add(b);

 		}

-		  stmtList = new StmtList(bigblocks, endCurly);

 		

+		     stmtList = new StmtList(bigblocks, endCurly);

+		  

 	}

 

-	static void StructuredCmd(out StructuredCmd! ec) {

+	void StructuredCmd(out StructuredCmd! ec) {

 		ec = dummyStructuredCmd;  assume ec.IsPeerConsistent;

 		IfCmd! ifcmd;  WhileCmd! wcmd;  BreakCmd! bcmd;

 		

-		if (t.kind == 40) {

+		if (la.kind == 40) {

 			IfCmd(out ifcmd);

 			ec = ifcmd; 

-		} else if (t.kind == 42) {

+		} else if (la.kind == 42) {

 			WhileCmd(out wcmd);

 			ec = wcmd; 

-		} else if (t.kind == 45) {

+		} else if (la.kind == 45) {

 			BreakCmd(out bcmd);

 			ec = bcmd; 

-		} else Error(101);

+		} else SynErr(101);

 	}

 

-	static void TransferCmd(out TransferCmd! tc) {

+	void TransferCmd(out TransferCmd! tc) {

 		tc = dummyTransferCmd;

 		Token y;  TokenSeq! xs;

 		StringSeq ss = new StringSeq();

 		

-		if (t.kind == 38) {

+		if (la.kind == 38) {

 			Get();

-			y = token; 

+			y = t; 

 			Idents(out xs);

 			foreach (IToken! s in xs) { ss.Add(s.val); }

 			tc = new GotoCmd(y, ss);

 			

-		} else if (t.kind == 39) {

+		} else if (la.kind == 39) {

 			Get();

-			tc = new ReturnCmd(token); 

-		} else Error(102);

+			tc = new ReturnCmd(t); 

+		} else SynErr(102);

 		Expect(7);

 	}

 

-	static void IfCmd(out IfCmd! ifcmd) {

+	void IfCmd(out IfCmd! ifcmd) {

 		IToken! x;

 		Expr guard;

 		StmtList! thn;

@@ -1051,37 +1112,37 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		StmtList! els;  StmtList elseOption = null;

 		

 		Expect(40);

-		x = token; 

+		x = t; 

 		Guard(out guard);

 		Expect(25);

 		StmtList(out thn);

-		if (t.kind == 41) {

+		if (la.kind == 41) {

 			Get();

-			if (t.kind == 40) {

+			if (la.kind == 40) {

 				IfCmd(out elseIf);

 				elseIfOption = elseIf; 

-			} else if (t.kind == 25) {

+			} else if (la.kind == 25) {

 				Get();

 				StmtList(out els);

 				elseOption = els; 

-			} else Error(103);

+			} else SynErr(103);

 		}

 		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 

 	}

 

-	static void WhileCmd(out WhileCmd! wcmd) {

+	void WhileCmd(out WhileCmd! wcmd) {

 		IToken! x;  Token z;

 		Expr guard;  Expr! e;  bool isFree;

 		List<PredicateCmd!> invariants = new List<PredicateCmd!>();

 		StmtList! body;

 		

 		Expect(42);

-		x = token; 

+		x = t; 

 		Guard(out guard);

 		assume guard == null || Owner.None(guard); 

-		while (t.kind == 33 || t.kind == 43) {

-			isFree = false; z = t/*lookahead token*/; 

-			if (t.kind == 33) {

+		while (la.kind == 33 || la.kind == 43) {

+			isFree = false; z = la/*lookahead token*/; 

+			if (la.kind == 33) {

 				Get();

 				isFree = true;  

 			}

@@ -1100,13 +1161,13 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		wcmd = new WhileCmd(x, guard, invariants, body); 

 	}

 

-	static void BreakCmd(out BreakCmd! bcmd) {

+	void BreakCmd(out BreakCmd! bcmd) {

 		IToken! x;  IToken! y;

 		string breakLabel = null;

 		

 		Expect(45);

-		x = token; 

-		if (t.kind == 1) {

+		x = t; 

+		if (la.kind == 1) {

 			Ident(out y);

 			breakLabel = y.val; 

 		}

@@ -1114,20 +1175,20 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		bcmd = new BreakCmd(x, breakLabel); 

 	}

 

-	static void Guard(out Expr e) {

+	void Guard(out Expr e) {

 		Expr! ee;  e = null; 

 		Expect(8);

-		if (t.kind == 44) {

+		if (la.kind == 44) {

 			Get();

 			e = null; 

 		} else if (StartOf(5)) {

 			Expression(out ee);

 			e = ee; 

-		} else Error(104);

+		} else SynErr(104);

 		Expect(9);

 	}

 

-	static void LabelOrAssign(out Cmd c, out IToken label) {

+	void LabelOrAssign(out Cmd c, out IToken label) {

 		IToken! id; IToken! x; Expr! e, e0;

 		c = dummyCmd;  label = null;

 		AssignLhs! lhs;

@@ -1135,36 +1196,36 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		List<Expr!>! rhss;

 		

 		Ident(out id);

-		x = token; 

-		if (t.kind == 10) {

+		x = t; 

+		if (la.kind == 10) {

 			Get();

 			c = null;  label = x; 

-		} else if (t.kind == 11 || t.kind == 15 || t.kind == 49) {

+		} else if (la.kind == 11 || la.kind == 15 || la.kind == 49) {

 			MapAssignIndexes(id, out lhs);

 			lhss = new List<AssignLhs!> ();

 			lhss.Add(lhs); 

-			while (t.kind == 11) {

+			while (la.kind == 11) {

 				Get();

 				Ident(out id);

 				MapAssignIndexes(id, out lhs);

 				lhss.Add(lhs); 

 			}

 			Expect(49);

-			x = token; /* use location of := */ 

+			x = t; /* use location of := */ 

 			Expression(out e0);

 			rhss = new List<Expr!> ();

 			rhss.Add(e0); 

-			while (t.kind == 11) {

+			while (la.kind == 11) {

 				Get();

 				Expression(out e0);

 				rhss.Add(e0); 

 			}

 			Expect(7);

 			c = new AssignCmd(x, lhss, rhss); 

-		} else Error(105);

+		} else SynErr(105);

 	}

 

-	static void CallCmd(out Cmd! c) {

+	void CallCmd(out Cmd! c) {

 		IToken! x; IToken! first; IToken p;

 		List<IdentifierExpr>! ids = new List<IdentifierExpr>();

 		List<Expr>! es = new List<Expr>();

@@ -1173,18 +1234,18 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		c = dummyCmd;

 		

 		Expect(50);

-		x = token; 

-		while (t.kind == 25) {

+		x = t; 

+		while (la.kind == 25) {

 			Attribute(ref kv);

 		}

-		if (t.kind == 1) {

+		if (la.kind == 1) {

 			Ident(out first);

-			if (t.kind == 8) {

+			if (la.kind == 8) {

 				Get();

 				if (StartOf(8)) {

 					CallForallArg(out en);

 					es.Add(en); 

-					while (t.kind == 11) {

+					while (la.kind == 11) {

 						Get();

 						CallForallArg(out en);

 						es.Add(en); 

@@ -1192,9 +1253,9 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				}

 				Expect(9);

 				c = new CallCmd(x, first.val, es, ids, kv); 

-			} else if (t.kind == 11 || t.kind == 49) {

+			} else if (la.kind == 11 || la.kind == 49) {

 				ids.Add(new IdentifierExpr(first, first.val)); 

-				if (t.kind == 11) {

+				if (la.kind == 11) {

 					Get();

 					CallOutIdent(out p);

 					if (p==null) {

@@ -1203,7 +1264,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 					   ids.Add(new IdentifierExpr(p, p.val));

 					}

 					

-					while (t.kind == 11) {

+					while (la.kind == 11) {

 						Get();

 						CallOutIdent(out p);

 						if (p==null) {

@@ -1220,7 +1281,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				if (StartOf(8)) {

 					CallForallArg(out en);

 					es.Add(en); 

-					while (t.kind == 11) {

+					while (la.kind == 11) {

 						Get();

 						CallForallArg(out en);

 						es.Add(en); 

@@ -1228,8 +1289,8 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				}

 				Expect(9);

 				c = new CallCmd(x, first.val, es, ids, kv); 

-			} else Error(106);

-		} else if (t.kind == 51) {

+			} else SynErr(106);

+		} else if (la.kind == 51) {

 			Get();

 			Ident(out first);

 			Expect(8);

@@ -1237,7 +1298,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			if (StartOf(8)) {

 				CallForallArg(out en);

 				args.Add(en); 

-				while (t.kind == 11) {

+				while (la.kind == 11) {

 					Get();

 					CallForallArg(out en);

 					args.Add(en); 

@@ -1245,10 +1306,10 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			}

 			Expect(9);

 			c = new CallForallCmd(x, first.val, args, kv); 

-		} else if (t.kind == 44) {

+		} else if (la.kind == 44) {

 			Get();

 			ids.Add(null); 

-			if (t.kind == 11) {

+			if (la.kind == 11) {

 				Get();

 				CallOutIdent(out p);

 				if (p==null) {

@@ -1257,7 +1318,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				   ids.Add(new IdentifierExpr(p, p.val));

 				}

 				

-				while (t.kind == 11) {

+				while (la.kind == 11) {

 					Get();

 					CallOutIdent(out p);

 					if (p==null) {

@@ -1274,7 +1335,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			if (StartOf(8)) {

 				CallForallArg(out en);

 				es.Add(en); 

-				while (t.kind == 11) {

+				while (la.kind == 11) {

 					Get();

 					CallForallArg(out en);

 					es.Add(en); 

@@ -1282,10 +1343,10 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			}

 			Expect(9);

 			c = new CallCmd(x, first.val, es, ids, kv); 

-		} else Error(107);

+		} else SynErr(107);

 	}

 

-	static void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {

+	void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {

 		IToken! x;

 		AssignLhs! runningLhs =

 		  new SimpleAssignLhs(assignedVariable,

@@ -1293,14 +1354,14 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		List<Expr!>! indexes;

 		Expr! e0;

 		

-		while (t.kind == 15) {

+		while (la.kind == 15) {

 			Get();

-			x = token;

+			x = t;

 			indexes = new List<Expr!> (); 

 			if (StartOf(5)) {

 				Expression(out e0);

 				indexes.Add(e0); 

-				while (t.kind == 11) {

+				while (la.kind == 11) {

 					Get();

 					Expression(out e0);

 					indexes.Add(e0); 

@@ -1313,60 +1374,60 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		lhs = runningLhs; 

 	}

 

-	static void CallForallArg(out Expr exprOptional) {

+	void CallForallArg(out Expr exprOptional) {

 		exprOptional = null;

 		Expr! e;

 		

-		if (t.kind == 44) {

+		if (la.kind == 44) {

 			Get();

 		} else if (StartOf(5)) {

 			Expression(out e);

 			exprOptional = e; 

-		} else Error(108);

+		} else SynErr(108);

 	}

 

-	static void CallOutIdent(out IToken id) {

+	void CallOutIdent(out IToken id) {

 		id = null;

 		IToken! p;

 		

-		if (t.kind == 44) {

+		if (la.kind == 44) {

 			Get();

-		} else if (t.kind == 1) {

+		} else if (la.kind == 1) {

 			Ident(out p);

 			id = p; 

-		} else Error(109);

+		} else SynErr(109);

 	}

 

-	static void Expressions(out ExprSeq! es) {

+	void Expressions(out ExprSeq! es) {

 		Expr! e; es = new ExprSeq(); 

 		Expression(out e);

 		es.Add(e); 

-		while (t.kind == 11) {

+		while (la.kind == 11) {

 			Get();

 			Expression(out e);

 			es.Add(e); 

 		}

 	}

 

-	static void ImpliesExpression(bool noExplies, out Expr! e0) {

+	void ImpliesExpression(bool noExplies, out Expr! e0) {

 		IToken! x; Expr! e1; 

 		LogicalExpression(out e0);

 		if (StartOf(9)) {

-			if (t.kind == 54 || t.kind == 55) {

+			if (la.kind == 54 || la.kind == 55) {

 				ImpliesOp();

-				x = token; 

+				x = t; 

 				ImpliesExpression(true, out e1);

 				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); 

 			} else {

 				ExpliesOp();

 				if (noExplies)

-				 SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");

-				x = token; 

+				 this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");

+				x = t; 

 				LogicalExpression(out e1);

 				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); 

-				while (t.kind == 56 || t.kind == 57) {

+				while (la.kind == 56 || la.kind == 57) {

 					ExpliesOp();

-					x = token; 

+					x = t; 

 					LogicalExpression(out e1);

 					e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); 

 				}

@@ -1374,37 +1435,37 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		}

 	}

 

-	static void EquivOp() {

-		if (t.kind == 52) {

+	void EquivOp() {

+		if (la.kind == 52) {

 			Get();

-		} else if (t.kind == 53) {

+		} else if (la.kind == 53) {

 			Get();

-		} else Error(110);

+		} else SynErr(110);

 	}

 

-	static void LogicalExpression(out Expr! e0) {

+	void LogicalExpression(out Expr! e0) {

 		IToken! x; Expr! e1; BinaryOperator.Opcode op; 

 		RelationalExpression(out e0);

 		if (StartOf(10)) {

-			if (t.kind == 58 || t.kind == 59) {

+			if (la.kind == 58 || la.kind == 59) {

 				AndOp();

-				x = token; 

+				x = t; 

 				RelationalExpression(out e1);

 				e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); 

-				while (t.kind == 58 || t.kind == 59) {

+				while (la.kind == 58 || la.kind == 59) {

 					AndOp();

-					x = token; 

+					x = t; 

 					RelationalExpression(out e1);

 					e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); 

 				}

 			} else {

 				OrOp();

-				x = token; 

+				x = t; 

 				RelationalExpression(out e1);

 				e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); 

-				while (t.kind == 60 || t.kind == 61) {

+				while (la.kind == 60 || la.kind == 61) {

 					OrOp();

-					x = token; 

+					x = t; 

 					RelationalExpression(out e1);

 					e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); 

 				}

@@ -1412,23 +1473,23 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		}

 	}

 

-	static void ImpliesOp() {

-		if (t.kind == 54) {

+	void ImpliesOp() {

+		if (la.kind == 54) {

 			Get();

-		} else if (t.kind == 55) {

+		} else if (la.kind == 55) {

 			Get();

-		} else Error(111);

+		} else SynErr(111);

 	}

 

-	static void ExpliesOp() {

-		if (t.kind == 56) {

+	void ExpliesOp() {

+		if (la.kind == 56) {

 			Get();

-		} else if (t.kind == 57) {

+		} else if (la.kind == 57) {

 			Get();

-		} else Error(112);

+		} else SynErr(112);

 	}

 

-	static void RelationalExpression(out Expr! e0) {

+	void RelationalExpression(out Expr! e0) {

 		IToken! x; Expr! e1; BinaryOperator.Opcode op; 

 		BvTerm(out e0);

 		if (StartOf(11)) {

@@ -1438,197 +1499,197 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		}

 	}

 

-	static void AndOp() {

-		if (t.kind == 58) {

+	void AndOp() {

+		if (la.kind == 58) {

 			Get();

-		} else if (t.kind == 59) {

+		} else if (la.kind == 59) {

 			Get();

-		} else Error(113);

+		} else SynErr(113);

 	}

 

-	static void OrOp() {

-		if (t.kind == 60) {

+	void OrOp() {

+		if (la.kind == 60) {

 			Get();

-		} else if (t.kind == 61) {

+		} else if (la.kind == 61) {

 			Get();

-		} else Error(114);

+		} else SynErr(114);

 	}

 

-	static void BvTerm(out Expr! e0) {

+	void BvTerm(out Expr! e0) {

 		IToken! x; Expr! e1; 

 		Term(out e0);

-		while (t.kind == 70) {

+		while (la.kind == 70) {

 			Get();

-			x = token; 

+			x = t; 

 			Term(out e1);

 			e0 = new BvConcatExpr(x, e0, e1); 

 		}

 	}

 

-	static void RelOp(out IToken! x, out BinaryOperator.Opcode op) {

+	void RelOp(out IToken! x, out BinaryOperator.Opcode op) {

 		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 

-		switch (t.kind) {

+		switch (la.kind) {

 		case 62: {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Eq; 

+			x = t; op=BinaryOperator.Opcode.Eq; 

 			break;

 		}

 		case 17: {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Lt; 

+			x = t; op=BinaryOperator.Opcode.Lt; 

 			break;

 		}

 		case 18: {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Gt; 

+			x = t; op=BinaryOperator.Opcode.Gt; 

 			break;

 		}

 		case 63: {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Le; 

+			x = t; op=BinaryOperator.Opcode.Le; 

 			break;

 		}

 		case 64: {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Ge; 

+			x = t; op=BinaryOperator.Opcode.Ge; 

 			break;

 		}

 		case 65: {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Neq; 

+			x = t; op=BinaryOperator.Opcode.Neq; 

 			break;

 		}

 		case 66: {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Subtype; 

+			x = t; op=BinaryOperator.Opcode.Subtype; 

 			break;

 		}

 		case 67: {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Neq; 

+			x = t; op=BinaryOperator.Opcode.Neq; 

 			break;

 		}

 		case 68: {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Le; 

+			x = t; op=BinaryOperator.Opcode.Le; 

 			break;

 		}

 		case 69: {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Ge; 

+			x = t; op=BinaryOperator.Opcode.Ge; 

 			break;

 		}

-		default: Error(115); break;

+		default: SynErr(115); break;

 		}

 	}

 

-	static void Term(out Expr! e0) {

+	void Term(out Expr! e0) {

 		IToken! x; Expr! e1; BinaryOperator.Opcode op; 

 		Factor(out e0);

-		while (t.kind == 71 || t.kind == 72) {

+		while (la.kind == 71 || la.kind == 72) {

 			AddOp(out x, out op);

 			Factor(out e1);

 			e0 = Expr.Binary(x, op, e0, e1); 

 		}

 	}

 

-	static void Factor(out Expr! e0) {

+	void Factor(out Expr! e0) {

 		IToken! x; Expr! e1; BinaryOperator.Opcode op; 

 		UnaryExpression(out e0);

-		while (t.kind == 44 || t.kind == 73 || t.kind == 74) {

+		while (la.kind == 44 || la.kind == 73 || la.kind == 74) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

 			e0 = Expr.Binary(x, op, e0, e1); 

 		}

 	}

 

-	static void AddOp(out IToken! x, out BinaryOperator.Opcode op) {

+	void AddOp(out IToken! x, out BinaryOperator.Opcode op) {

 		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 

-		if (t.kind == 71) {

+		if (la.kind == 71) {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Add; 

-		} else if (t.kind == 72) {

+			x = t; op=BinaryOperator.Opcode.Add; 

+		} else if (la.kind == 72) {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Sub; 

-		} else Error(116);

+			x = t; op=BinaryOperator.Opcode.Sub; 

+		} else SynErr(116);

 	}

 

-	static void UnaryExpression(out Expr! e) {

+	void UnaryExpression(out Expr! e) {

 		IToken! x;

 		e = dummyExpr;

 		

-		if (t.kind == 72) {

+		if (la.kind == 72) {

 			Get();

-			x = token; 

+			x = t; 

 			UnaryExpression(out e);

 			e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); 

-		} else if (t.kind == 75 || t.kind == 76) {

+		} else if (la.kind == 75 || la.kind == 76) {

 			NegOp();

-			x = token; 

+			x = t; 

 			UnaryExpression(out e);

 			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 

 		} else if (StartOf(12)) {

 			CoercionExpression(out e);

-		} else Error(117);

+		} else SynErr(117);

 	}

 

-	static void MulOp(out IToken! x, out BinaryOperator.Opcode op) {

+	void MulOp(out IToken! x, out BinaryOperator.Opcode op) {

 		x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 

-		if (t.kind == 44) {

+		if (la.kind == 44) {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Mul; 

-		} else if (t.kind == 73) {

+			x = t; op=BinaryOperator.Opcode.Mul; 

+		} else if (la.kind == 73) {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Div; 

-		} else if (t.kind == 74) {

+			x = t; op=BinaryOperator.Opcode.Div; 

+		} else if (la.kind == 74) {

 			Get();

-			x = token; op=BinaryOperator.Opcode.Mod; 

-		} else Error(118);

+			x = t; op=BinaryOperator.Opcode.Mod; 

+		} else SynErr(118);

 	}

 

-	static void NegOp() {

-		if (t.kind == 75) {

+	void NegOp() {

+		if (la.kind == 75) {

 			Get();

-		} else if (t.kind == 76) {

+		} else if (la.kind == 76) {

 			Get();

-		} else Error(119);

+		} else SynErr(119);

 	}

 

-	static void CoercionExpression(out Expr! e) {

+	void CoercionExpression(out Expr! e) {

 		IToken! x;

 		Type! coercedTo;

 		BigNum bn;

 		

 		ArrayExpression(out e);

-		while (t.kind == 10) {

+		while (la.kind == 10) {

 			Get();

-			x = token; 

+			x = t; 

 			if (StartOf(2)) {

 				Type(out coercedTo);

 				e = Expr.CoerceType(x, e, coercedTo); 

-			} else if (t.kind == 3) {

+			} else if (la.kind == 3) {

 				Nat(out bn);

 				if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) {

-				 SemErr("arguments of extract need to be integer literals");

+				 this.SemErr("arguments of extract need to be integer literals");

 				 e = new BvBounds(x, bn, BigNum.ZERO);

 				} else {

 				  e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);

 				}

 				

-			} else Error(120);

+			} else SynErr(120);

 		}

 	}

 

-	static void ArrayExpression(out Expr! e) {

+	void ArrayExpression(out Expr! e) {

 		IToken! x;

 		Expr! index0 = dummyExpr; Expr! e1;

 		bool store; bool bvExtract;

 		ExprSeq! allArgs = dummyExprSeq;

 		

 		AtomExpression(out e);

-		while (t.kind == 15) {

+		while (la.kind == 15) {

 			Get();

-			x = token; allArgs = new ExprSeq ();

+			x = t; allArgs = new ExprSeq ();

 			allArgs.Add(e);

 			store = false; bvExtract = false; 

 			if (StartOf(13)) {

@@ -1639,19 +1700,19 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 					else

 					  allArgs.Add(index0);

 					

-					while (t.kind == 11) {

+					while (la.kind == 11) {

 						Get();

 						Expression(out e1);

 						if (bvExtract || e1 is BvBounds)

-						 SemErr("bitvectors only have one dimension");

+						 this.SemErr("bitvectors only have one dimension");

 						allArgs.Add(e1);

 						

 					}

-					if (t.kind == 49) {

+					if (la.kind == 49) {

 						Get();

 						Expression(out e1);

 						if (bvExtract || e1 is BvBounds)

-						 SemErr("assignment to bitvectors is not possible");

+						 this.SemErr("assignment to bitvectors is not possible");

 						allArgs.Add(e1); store = true;

 						

 					}

@@ -1674,18 +1735,18 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		}

 	}

 

-	static void Nat(out BigNum n) {

+	void Nat(out BigNum n) {

 		Expect(3);

 		try {

-		 n = BigNum.FromString(token.val);

+		 n = BigNum.FromString(t.val);

 		} catch (FormatException) {

-		  SemErr("incorrectly formatted number");

+		  this.SemErr("incorrectly formatted number");

 		  n = BigNum.ZERO;

 		}

 		

 	}

 

-	static void AtomExpression(out Expr! e) {

+	void AtomExpression(out Expr! e) {

 		IToken! x; int n; BigNum bn;

 		ExprSeq! es;  VariableSeq! ds;  Trigger trig;

 		TypeVariableSeq! typeParams;

@@ -1694,45 +1755,45 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		QKeyValue kv;

 		e = dummyExpr;

 		

-		switch (t.kind) {

+		switch (la.kind) {

 		case 77: {

 			Get();

-			e = new LiteralExpr(token, false); 

+			e = new LiteralExpr(t, false); 

 			break;

 		}

 		case 78: {

 			Get();

-			e = new LiteralExpr(token, true); 

+			e = new LiteralExpr(t, true); 

 			break;

 		}

 		case 3: {

 			Nat(out bn);

-			e = new LiteralExpr(token, bn); 

+			e = new LiteralExpr(t, bn); 

 			break;

 		}

 		case 2: {

 			BvLit(out bn, out n);

-			e = new LiteralExpr(token, bn, n); 

+			e = new LiteralExpr(t, bn, n); 

 			break;

 		}

 		case 1: {

 			Ident(out x);

 			id = new IdentifierExpr(x, x.val);  e = id; 

-			if (t.kind == 8) {

+			if (la.kind == 8) {

 				Get();

 				if (StartOf(5)) {

 					Expressions(out es);

 					e = new NAryExpr(x, new FunctionCall(id), es); 

-				} else if (t.kind == 9) {

+				} else if (la.kind == 9) {

 					e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); 

-				} else Error(121);

+				} else SynErr(121);

 				Expect(9);

 			}

 			break;

 		}

 		case 79: {

 			Get();

-			x = token; 

+			x = t; 

 			Expect(8);

 			Expression(out e);

 			Expect(9);

@@ -1744,29 +1805,29 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			if (StartOf(5)) {

 				Expression(out e);

 				if (e is BvBounds)

-				 SemErr("parentheses around bitvector bounds " +

+				 this.SemErr("parentheses around bitvector bounds " +

 				        "are not allowed"); 

-			} else if (t.kind == 51 || t.kind == 81) {

+			} else if (la.kind == 51 || la.kind == 81) {

 				Forall();

-				x = token; 

+				x = t; 

 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (typeParams.Length + ds.Length > 0)

 				 e = new ForallExpr(x, typeParams, ds, kv, trig, e); 

-			} else if (t.kind == 82 || t.kind == 83) {

+			} else if (la.kind == 82 || la.kind == 83) {

 				Exists();

-				x = token; 

+				x = t; 

 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (typeParams.Length + ds.Length > 0)

 				 e = new ExistsExpr(x, typeParams, ds, kv, trig, e); 

-			} else if (t.kind == 84 || t.kind == 85) {

+			} else if (la.kind == 84 || la.kind == 85) {

 				Lambda();

-				x = token; 

+				x = t; 

 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (trig != null)

 				 SemErr("triggers not allowed in lambda expressions");

 				if (typeParams.Length + ds.Length > 0)

 				  e = new LambdaExpr(x, typeParams, ds, kv, e); 

-			} else Error(122);

+			} else SynErr(122);

 			Expect(9);

 			break;

 		}

@@ -1774,78 +1835,78 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			IfThenElseExpression(out e);

 			break;

 		}

-		default: Error(123); break;

+		default: SynErr(123); break;

 		}

 	}

 

-	static void BvLit(out BigNum n, out int m) {

+	void BvLit(out BigNum n, out int m) {

 		Expect(2);

-		int pos = token.val.IndexOf("bv");

-		string a = token.val.Substring(0, pos);

-		string b = token.val.Substring(pos + 2);

+		int pos = t.val.IndexOf("bv");

+		string a = t.val.Substring(0, pos);

+		string b = t.val.Substring(pos + 2);

 		try {

 		  n = BigNum.FromString(a);

 		  m = Convert.ToInt32(b);

 		} catch (FormatException) {

-		  SemErr("incorrectly formatted bitvector");

+		  this.SemErr("incorrectly formatted bitvector");

 		  n = BigNum.ZERO;

 		  m = 0;

 		}

 		

 	}

 

-	static void Forall() {

-		if (t.kind == 51) {

+	void Forall() {

+		if (la.kind == 51) {

 			Get();

-		} else if (t.kind == 81) {

+		} else if (la.kind == 81) {

 			Get();

-		} else Error(124);

+		} else SynErr(124);

 	}

 

-	static void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,

+	void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,

 out QKeyValue kv, out Trigger trig, out Expr! body) {

 		trig = null; typeParams = new TypeVariableSeq ();

 		IToken! tok;  Expr! e;  ExprSeq! es;

 		kv = null;  string key;  string value;

 		ds = new VariableSeq ();

 		

-		if (t.kind == 17) {

+		if (la.kind == 17) {

 			TypeParams(out tok, out typeParams);

-			if (t.kind == 1) {

+			if (la.kind == 1) {

 				BoundVars(q, out ds);

 			}

-		} else if (t.kind == 1) {

+		} else if (la.kind == 1) {

 			BoundVars(q, out ds);

-		} else Error(125);

+		} else SynErr(125);

 		QSep();

-		while (t.kind == 25) {

+		while (la.kind == 25) {

 			AttributeOrTrigger(ref kv, ref trig);

 		}

 		Expression(out body);

 	}

 

-	static void Exists() {

-		if (t.kind == 82) {

+	void Exists() {

+		if (la.kind == 82) {

 			Get();

-		} else if (t.kind == 83) {

+		} else if (la.kind == 83) {

 			Get();

-		} else Error(126);

+		} else SynErr(126);

 	}

 

-	static void Lambda() {

-		if (t.kind == 84) {

+	void Lambda() {

+		if (la.kind == 84) {

 			Get();

-		} else if (t.kind == 85) {

+		} else if (la.kind == 85) {

 			Get();

-		} else Error(127);

+		} else SynErr(127);

 	}

 

-	static void IfThenElseExpression(out Expr! e) {

+	void IfThenElseExpression(out Expr! e) {

 		IToken! tok;

 		Expr! e0, e1, e2; 

 		e = dummyExpr; 

 		Expect(40);

-		tok = token; 

+		tok = t; 

 		Expression(out e0);

 		Expect(80);

 		Expression(out e1);

@@ -1854,21 +1915,21 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 		e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); 

 	}

 

-	static void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {

+	void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {

 		IToken! tok;  Expr! e;  ExprSeq! es;

 		string key;  string value;

 		List<object!> parameters;  object! param;

 		

 		Expect(25);

-		tok = token; 

-		if (t.kind == 10) {

+		tok = t; 

+		if (la.kind == 10) {

 			Get();

 			Expect(1);

-			key = token.val;  parameters = new List<object!>(); 

+			key = t.val;  parameters = new List<object!>(); 

 			if (StartOf(14)) {

 				AttributeParameter(out param);

 				parameters.Add(param); 

-				while (t.kind == 11) {

+				while (la.kind == 11) {

 					Get();

 					AttributeParameter(out param);

 					parameters.Add(param); 

@@ -1883,7 +1944,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			     trig.AddLast(new Trigger(tok, false, new ExprSeq(e), null));

 			   }

 			 } else {

-			   SemErr("the 'nopats' quantifier attribute expects a string-literal parameter");

+			   this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter");

 			 }

 			} else {

 			  if (kv==null) {

@@ -1896,7 +1957,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 		} else if (StartOf(5)) {

 			Expression(out e);

 			es = new ExprSeq(e); 

-			while (t.kind == 11) {

+			while (la.kind == 11) {

 				Get();

 				Expression(out e);

 				es.Add(e); 

@@ -1907,46 +1968,73 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			  trig.AddLast(new Trigger(tok, true, es, null));

 			}

 			

-		} else Error(128);

+		} else SynErr(128);

 		Expect(26);

 	}

 

-	static void AttributeParameter(out object! o) {

+	void AttributeParameter(out object! o) {

 		o = "error";

 		Expr! e;

 		

-		if (t.kind == 4) {

+		if (la.kind == 4) {

 			Get();

-			o = token.val.Substring(1, token.val.Length-2); 

+			o = t.val.Substring(1, t.val.Length-2); 

 		} else if (StartOf(5)) {

 			Expression(out e);

 			o = e; 

-		} else Error(129);

+		} else SynErr(129);

 	}

 

-	static void QSep() {

-		if (t.kind == 86) {

+	void QSep() {

+		if (la.kind == 86) {

 			Get();

-		} else if (t.kind == 87) {

+		} else if (la.kind == 87) {

 			Get();

-		} else Error(130);

+		} else SynErr(130);

 	}

 

 

 

-	public static void Parse() {

-		Errors.SynErr = new ErrorProc(SynErr);

-		t = new Token();

+	public void Parse() {

+		la = new Token();

+		la.val = "";		

 		Get();

 		BoogiePL();

 

+    Expect(0);

 	}

+	

+	static readonly bool[,]! set = {

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

+		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x},

+		{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

+		{x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}

 

-	[Microsoft.Contracts.Verify(false)]

-	static void SynErr(int n, string filename, int line, int col) {

-		Errors.count++;

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

+	};

+} // end Parser

+

+

+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 void SynErr (string filename, int line, int col, 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;

@@ -1954,88 +2042,88 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			case 3: s = "digits expected"; break;

 			case 4: s = "string expected"; break;

 			case 5: s = "float expected"; break;

-			case 6: s = "var expected"; break;

-			case 7: s = "; expected"; break;

-			case 8: s = "( expected"; break;

-			case 9: s = ") expected"; break;

-			case 10: s = ": expected"; break;

-			case 11: s = ", expected"; break;

-			case 12: s = "where expected"; break;

-			case 13: s = "int expected"; break;

-			case 14: s = "bool expected"; break;

-			case 15: s = "[ expected"; break;

-			case 16: s = "] expected"; break;

-			case 17: s = "< expected"; break;

-			case 18: s = "> expected"; break;

-			case 19: s = "const expected"; break;

-			case 20: s = "unique expected"; break;

-			case 21: s = "extends expected"; break;

-			case 22: s = "complete expected"; break;

-			case 23: s = "function expected"; break;

-			case 24: s = "returns expected"; break;

-			case 25: s = "{ expected"; break;

-			case 26: s = "} expected"; break;

-			case 27: s = "axiom expected"; break;

-			case 28: s = "type expected"; break;

-			case 29: s = "= expected"; break;

-			case 30: s = "procedure expected"; break;

-			case 31: s = "implementation expected"; break;

-			case 32: s = "modifies expected"; break;

-			case 33: s = "free expected"; break;

-			case 34: s = "requires expected"; break;

-			case 35: s = "ensures expected"; break;

-			case 36: s = "{{ expected"; break;

-			case 37: s = "}} expected"; break;

-			case 38: s = "goto expected"; break;

-			case 39: s = "return expected"; break;

-			case 40: s = "if expected"; break;

-			case 41: s = "else expected"; break;

-			case 42: s = "while expected"; break;

-			case 43: s = "invariant expected"; break;

-			case 44: s = "* expected"; break;

-			case 45: s = "break expected"; break;

-			case 46: s = "assert expected"; break;

-			case 47: s = "assume expected"; break;

-			case 48: s = "havoc expected"; break;

-			case 49: s = ":= expected"; break;

-			case 50: s = "call expected"; break;

-			case 51: s = "forall expected"; break;

-			case 52: s = "<==> expected"; break;

-			case 53: s = "\\u21d4 expected"; break;

-			case 54: s = "==> expected"; break;

-			case 55: s = "\\u21d2 expected"; break;

-			case 56: s = "<== expected"; break;

-			case 57: s = "\\u21d0 expected"; break;

-			case 58: s = "&& expected"; break;

-			case 59: s = "\\u2227 expected"; break;

-			case 60: s = "|| expected"; break;

-			case 61: s = "\\u2228 expected"; break;

-			case 62: s = "== expected"; break;

-			case 63: s = "<= expected"; break;

-			case 64: s = ">= expected"; break;

-			case 65: s = "!= expected"; break;

-			case 66: s = "<: expected"; break;

-			case 67: s = "\\u2260 expected"; break;

-			case 68: s = "\\u2264 expected"; break;

-			case 69: s = "\\u2265 expected"; break;

-			case 70: s = "++ expected"; break;

-			case 71: s = "+ expected"; break;

-			case 72: s = "- expected"; break;

-			case 73: s = "/ expected"; break;

-			case 74: s = "% expected"; break;

-			case 75: s = "! expected"; break;

-			case 76: s = "\\u00ac expected"; break;

-			case 77: s = "false expected"; break;

-			case 78: s = "true expected"; break;

-			case 79: s = "old expected"; break;

-			case 80: s = "then expected"; break;

-			case 81: s = "\\u2200 expected"; break;

-			case 82: s = "exists expected"; break;

-			case 83: s = "\\u2203 expected"; break;

-			case 84: s = "lambda expected"; break;

-			case 85: s = "\\u03bb expected"; break;

-			case 86: s = ":: expected"; break;

-			case 87: s = "\\u2022 expected"; break;

+			case 6: s = "\"var\" expected"; break;

+			case 7: s = "\";\" expected"; break;

+			case 8: s = "\"(\" expected"; break;

+			case 9: s = "\")\" expected"; break;

+			case 10: s = "\":\" expected"; break;

+			case 11: s = "\",\" expected"; break;

+			case 12: s = "\"where\" expected"; break;

+			case 13: s = "\"int\" expected"; break;

+			case 14: s = "\"bool\" expected"; break;

+			case 15: s = "\"[\" expected"; break;

+			case 16: s = "\"]\" expected"; break;

+			case 17: s = "\"<\" expected"; break;

+			case 18: s = "\">\" expected"; break;

+			case 19: s = "\"const\" expected"; break;

+			case 20: s = "\"unique\" expected"; break;

+			case 21: s = "\"extends\" expected"; break;

+			case 22: s = "\"complete\" expected"; break;

+			case 23: s = "\"function\" expected"; break;

+			case 24: s = "\"returns\" expected"; break;

+			case 25: s = "\"{\" expected"; break;

+			case 26: s = "\"}\" expected"; break;

+			case 27: s = "\"axiom\" expected"; break;

+			case 28: s = "\"type\" expected"; break;

+			case 29: s = "\"=\" expected"; break;

+			case 30: s = "\"procedure\" expected"; break;

+			case 31: s = "\"implementation\" expected"; break;

+			case 32: s = "\"modifies\" expected"; break;

+			case 33: s = "\"free\" expected"; break;

+			case 34: s = "\"requires\" expected"; break;

+			case 35: s = "\"ensures\" expected"; break;

+			case 36: s = "\"{{\" expected"; break;

+			case 37: s = "\"}}\" expected"; break;

+			case 38: s = "\"goto\" expected"; break;

+			case 39: s = "\"return\" expected"; break;

+			case 40: s = "\"if\" expected"; break;

+			case 41: s = "\"else\" expected"; break;

+			case 42: s = "\"while\" expected"; break;

+			case 43: s = "\"invariant\" expected"; break;

+			case 44: s = "\"*\" expected"; break;

+			case 45: s = "\"break\" expected"; break;

+			case 46: s = "\"assert\" expected"; break;

+			case 47: s = "\"assume\" expected"; break;

+			case 48: s = "\"havoc\" expected"; break;

+			case 49: s = "\":=\" expected"; break;

+			case 50: s = "\"call\" expected"; break;

+			case 51: s = "\"forall\" expected"; break;

+			case 52: s = "\"<==>\" expected"; break;

+			case 53: s = "\"\\u21d4\" expected"; break;

+			case 54: s = "\"==>\" expected"; break;

+			case 55: s = "\"\\u21d2\" expected"; break;

+			case 56: s = "\"<==\" expected"; break;

+			case 57: s = "\"\\u21d0\" expected"; break;

+			case 58: s = "\"&&\" expected"; break;

+			case 59: s = "\"\\u2227\" expected"; break;

+			case 60: s = "\"||\" expected"; break;

+			case 61: s = "\"\\u2228\" expected"; break;

+			case 62: s = "\"==\" expected"; break;

+			case 63: s = "\"<=\" expected"; break;

+			case 64: s = "\">=\" expected"; break;

+			case 65: s = "\"!=\" expected"; break;

+			case 66: s = "\"<:\" expected"; break;

+			case 67: s = "\"\\u2260\" expected"; break;

+			case 68: s = "\"\\u2264\" expected"; break;

+			case 69: s = "\"\\u2265\" expected"; break;

+			case 70: s = "\"++\" expected"; break;

+			case 71: s = "\"+\" expected"; break;

+			case 72: s = "\"-\" expected"; break;

+			case 73: s = "\"/\" expected"; break;

+			case 74: s = "\"%\" expected"; break;

+			case 75: s = "\"!\" expected"; break;

+			case 76: s = "\"\\u00ac\" expected"; break;

+			case 77: s = "\"false\" expected"; break;

+			case 78: s = "\"true\" expected"; break;

+			case 79: s = "\"old\" expected"; break;

+			case 80: s = "\"then\" expected"; break;

+			case 81: s = "\"\\u2200\" expected"; break;

+			case 82: s = "\"exists\" expected"; break;

+			case 83: s = "\"\\u2203\" expected"; break;

+			case 84: s = "\"lambda\" expected"; break;

+			case 85: s = "\"\\u03bb\" expected"; break;

+			case 86: s = "\"::\" expected"; break;

+			case 87: s = "\"\\u2022\" expected"; break;

 			case 88: s = "??? expected"; break;

 			case 89: s = "invalid Function"; break;

 			case 90: s = "invalid Function"; break;

@@ -2082,30 +2170,42 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 

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

 		}

-		Console.WriteLine(s);

-	}

-

-	static bool[,]! set = {

-	{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-	{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-	{x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

-	{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-	{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

-	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x},

-	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

-	{x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}

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

+		errorStream.WriteLine(s);

+		count++;

+	}

 

-	};

+	public void SemErr (int line, int col, string! s) {

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

+		count++;

+	}

 

-	[Microsoft.Contracts.Verify(false)]

-	static Parser() {}

-} // end Parser

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

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

+		count++;

+	}

+	

+	public void SemErr (string s) {

+		errorStream.WriteLine(s);

+		count++;

+	}

+

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

+      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);

+	}

+} // Errors

+

+

+public class FatalError: Exception {

+	public FatalError(string m): base(m) {}

+}

 

-} // end namespace

+}
\ No newline at end of file
diff --git a/Source/Core/ParserHelper.ssc b/Source/Core/ParserHelper.ssc
new file mode 100644
index 00000000..ee01880a
--- /dev/null
+++ b/Source/Core/ParserHelper.ssc
@@ -0,0 +1,116 @@
+using System.Text;

+using System.Collections.Generic;

+using System.IO;

+namespace Microsoft.Boogie {

+public static class ParserHelper {

+  struct ReadState {

+    public bool hasSeenElse;

+    public bool mayStillIncludeAnotherAlternative;

+    public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) {

+      this.hasSeenElse = hasSeenElse;

+      this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative;

+    }

+  }

+  // "arg" is assumed to be trimmed

+  private static bool IfdefConditionSaysToInclude(string! arg, List<string!>! defines) {

+    bool sense = true;

+    while (arg.StartsWith("!")) {

+      sense = !sense;

+      arg = arg.Substring(1).TrimStart();

+    }

+    return defines.Contains(arg) == sense;

+  }

+  

+  public static string! Fill(FileStream! fileStream, List<string!>! defines) {

+    StreamReader! reader = new StreamReader(fileStream);

+    return Fill(reader, defines);

+  }

+  public static string! Fill(TextReader! reader, List<string!>! defines) {

+    StringBuilder sb = new StringBuilder();

+    List<ReadState>! readState = new List<ReadState>();  // readState.Count is the current nesting level of #if's

+    int ignoreCutoff = -1;  // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n

+    while (true)

+      //invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count;

+    {

+      string s = reader.ReadLine();

+      if (s == null) {

+        if (readState.Count != 0) {

+          sb.AppendLine("#MalformedInput: missing #endif");

+        }

+        break;

+      }

+      string t = s.Trim();

+      if (t.StartsWith("#if")) {

+        ReadState rs = new ReadState(false, false);

+        if (ignoreCutoff != -1) {

+          // we're already in a state of ignoring, so continue to ignore

+        } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) {

+          // include this branch

+        } else {

+          ignoreCutoff = readState.Count;  // start ignoring

+          rs.mayStillIncludeAnotherAlternative = true;  // allow some later "elsif" or "else" branch to be included

+        }

+        readState.Add(rs);

+        sb.AppendLine();  // ignore the #if line

+

+      } else if (t.StartsWith("#elsif")) {

+        ReadState rs;

+        if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) {

+          sb.AppendLine("#MalformedInput: misplaced #elsif");  // malformed input

+          break;

+        }

+        if (ignoreCutoff == -1) {

+          // we had included the previous branch

+          //assert !rs.mayStillIncludeAnotherAlternative;

+          ignoreCutoff = readState.Count-1;  // start ignoring

+        } else if (rs.mayStillIncludeAnotherAlternative && IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) {

+          // include this branch, but no subsequent branch at this level

+          ignoreCutoff = -1;

+          rs.mayStillIncludeAnotherAlternative = false;

+          readState[readState.Count-1] = rs;

+        }

+        sb.AppendLine();  // ignore the #elsif line

+

+      } else if (t == "#else") {

+        ReadState rs;

+        if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) {

+          sb.AppendLine("#MalformedInput: misplaced #else");  // malformed input

+          break;

+        }

+        rs.hasSeenElse = true;

+        if (ignoreCutoff == -1) {

+          // we had included the previous branch

+          //assert !rs.mayStillIncludeAnotherAlternative;

+          ignoreCutoff = readState.Count-1;  // start ignoring

+        } else if (rs.mayStillIncludeAnotherAlternative) {

+          // include this branch

+          ignoreCutoff = -1;

+          rs.mayStillIncludeAnotherAlternative = false;

+        }

+        readState[readState.Count-1] = rs;

+        sb.AppendLine();  // ignore the #else line

+

+      } else if (t == "#endif") {

+        if (readState.Count == 0) {

+          sb.AppendLine("#MalformedInput: misplaced #endif");  // malformed input

+          break;

+        }

+        readState.RemoveAt(readState.Count-1);  // pop

+        if (ignoreCutoff == readState.Count) {

+          // we had ignored the branch that ends here; so, now we start including again

+          ignoreCutoff = -1;

+        }

+        sb.AppendLine();  // ignore the #endif line

+

+      } else if (ignoreCutoff == -1) {

+        sb.AppendLine(s);  // included line

+

+      } else {

+        sb.AppendLine();  // ignore the line

+      }

+    }

+    

+    return sb.ToString();

+  }

+}

+}
\ No newline at end of file
diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc
index a6f2c0a4..3765574e 100644
--- a/Source/Core/Scanner.ssc
+++ b/Source/Core/Scanner.ssc
@@ -1,3 +1,4 @@
+

 using System;

 using System.IO;

 using System.Collections;

@@ -5,7 +6,6 @@ using System.Collections.Generic;
 using System.Text;

 using Microsoft.Contracts;

 

-

 namespace Microsoft.Boogie {

 

   [Immutable]

@@ -19,26 +19,30 @@ namespace Microsoft.Boogie {
 

     bool IsValid { get; }

   }

-  

+

   [Immutable]

   public class Token : IToken {

-    int _kind;         // token kind

+	public int _kind;    // token kind

     string _filename;  // token file

-    int _pos;          // token position in the source text (starting at 0)

-    int _col;          // token column (starting at 0)

-    int _line;         // token line (starting at 1)

-    string/*!*/ _val = "foo";  // token value

-

+	public int _pos;     // token position in the source text (starting at 0)

+	public int _col;     // token column (starting at 1)

+	public int _line;    // token line (starting at 1)

+	public string/*!*/ _val;  // token value

+	public Token next;  // ML 2005-03-11 Tokens are kept in linked list

+	

     public static IToken! NoToken = new Token();

 

-    public Token();

+    public Token() {

+      this._val = "anything so that it is nonnull";

+    }

     public Token(int linenum, int colnum) {

       this._line = linenum;

       this._col = colnum;

+      this._val = "anything so that it is nonnull";

       base();

     }

 

-    public int kind {

+	public int kind {

       get { return this._kind; }

       set { this._kind = value; }

     }

@@ -47,7 +51,7 @@ namespace Microsoft.Boogie {
       get { return this._filename; }

       set { this._filename = value; }

     }

-    

+

     public int pos{

       get { return this._pos; }

       set { this._pos = value; }

@@ -67,394 +71,435 @@ namespace Microsoft.Boogie {
       get { return this._val; }

       set { this._val = value; }

     }

-    

+

     public bool IsValid { get { return this._filename != null; } }

-  }

 

+	

 }

 

-namespace BoogiePL {

-

-using Microsoft.Boogie;

-

+//-----------------------------------------------------------------------------------

+// Buffer

+//-----------------------------------------------------------------------------------

 public class Buffer {

-  static string/*!*/ buf;

-  static int bufLen;

-  static int pos;

-  public const int eof = '\uffff';

+	// This Buffer supports the following cases:

+	// 1) seekable stream (file)

+	//    a) whole stream in buffer

+	//    b) part of stream in buffer

+	// 2) non seekable stream (network, console)

   

-  public static void Fill(TextReader! reader) {

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

-    Fill(reader, defines);

-  }

-  

-  struct ReadState {

-    public bool hasSeenElse;

-    public bool mayStillIncludeAnotherAlternative;

-    public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) {

-      this.hasSeenElse = hasSeenElse;

-      this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative;

-    }

-  }

-  

-  public static void Fill(TextReader! reader, List<string!>! defines) {

-    StringBuilder sb = new StringBuilder();

-    List<ReadState>! readState = new List<ReadState>();  // readState.Count is the current nesting level of #if's

-    int ignoreCutoff = -1;  // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n

-    while (true)

-      invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count;

-    {

-      string s = reader.ReadLine();

-      if (s == null) {

-        if (readState.Count != 0) {

-          sb.AppendLine("#MalformedInput: missing #endif");

-        }

-        break;

-      }

-      string t = s.Trim();

-      if (t.StartsWith("#if")) {

-        ReadState rs = new ReadState(false, false);

-        if (ignoreCutoff != -1) {

-          // we're already in a state of ignoring, so continue to ignore

-        } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) {

-          // include this branch

-        } else {

-          ignoreCutoff = readState.Count;  // start ignoring

-          rs.mayStillIncludeAnotherAlternative = true;  // allow some later "elsif" or "else" branch to be included

-        }

-        readState.Add(rs);

-        sb.AppendLine();  // ignore the #if line

-

-      } else if (t.StartsWith("#elsif")) {

-        ReadState rs;

-        if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) {

-          sb.AppendLine("#MalformedInput: misplaced #elsif");  // malformed input

-          break;

-        }

-        if (ignoreCutoff == -1) {

-          // we had included the previous branch

-          assert !rs.mayStillIncludeAnotherAlternative;

-          ignoreCutoff = readState.Count-1;  // start ignoring

-        } else if (rs.mayStillIncludeAnotherAlternative && IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) {

-          // include this branch, but no subsequent branch at this level

-          ignoreCutoff = -1;

-          rs.mayStillIncludeAnotherAlternative = false;

-          readState[readState.Count-1] = rs;

-        }

-        sb.AppendLine();  // ignore the #elsif line

-

-      } else if (t == "#else") {

-        ReadState rs;

-        if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) {

-          sb.AppendLine("#MalformedInput: misplaced #else");  // malformed input

-          break;

-        }

-        rs.hasSeenElse = true;

-        if (ignoreCutoff == -1) {

-          // we had included the previous branch

-          assert !rs.mayStillIncludeAnotherAlternative;

-          ignoreCutoff = readState.Count-1;  // start ignoring

-        } else if (rs.mayStillIncludeAnotherAlternative) {

-          // include this branch

-          ignoreCutoff = -1;

-          rs.mayStillIncludeAnotherAlternative = false;

-        }

-        readState[readState.Count-1] = rs;

-        sb.AppendLine();  // ignore the #else line

-

-      } else if (t == "#endif") {

-        if (readState.Count == 0) {

-          sb.AppendLine("#MalformedInput: misplaced #endif");  // malformed input

-          break;

-        }

-        readState.RemoveAt(readState.Count-1);  // pop

-        if (ignoreCutoff == readState.Count) {

-          // we had ignored the branch that ends here; so, now we start including again

-          ignoreCutoff = -1;

-        }

-        sb.AppendLine();  // ignore the #endif line

-

-      } else if (ignoreCutoff == -1) {

-        sb.AppendLine(s);  // included line

-

-      } else {

-        sb.AppendLine();  // ignore the line

-      }

-    }

-    

-    Fill(sb.ToString());

-  }

+	public const int EOF = 65535 + 1; // char.MaxValue + 1;

+	const int MIN_BUFFER_LENGTH = 1024; // 1KB

+	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB

+	byte[]! buf;         // input buffer

+	int bufStart;       // position of first byte in buffer relative to input stream

+	int bufLen;         // length of buffer

+	int fileLen;        // length of input stream (may change if the stream is no file)

+	int bufPos;         // current position in buffer

+	Stream! stream;      // input stream (seekable)

+	bool isUserStream;  // was the stream opened by the user?

+

+    [NotDelayed]

+	public Buffer (Stream! s, bool isUserStream) {

+		stream = s; this.isUserStream = isUserStream;

+		

+		int fl, bl;

+		if (s.CanSeek) {

+			fl = (int) s.Length;

+			bl = fl < MAX_BUFFER_LENGTH ? fl : MAX_BUFFER_LENGTH; // Math.Min(fileLen, MAX_BUFFER_LENGTH);

+			bufStart = Int32.MaxValue; // nothing in the buffer so far

+		} else {

+			fl = bl = bufStart = 0;

+		}

 

-  // "arg" is assumed to be trimmed

-  private static bool IfdefConditionSaysToInclude(string! arg, List<string!>! defines) {

-    bool sense = true;

-    while (arg.StartsWith("!")) {

-      sense = !sense;

-      arg = arg.Substring(1).TrimStart();

-    }

-    return defines.Contains(arg) == sense;

-  }

-  

-  public static void Fill(string! text) {

-    buf = text;

-    bufLen = buf.Length;

-    pos = 0;

-  }

-  

-  public static int Read() {

-    if (pos < bufLen) {

-      return buf[pos++];

-    } else {

-      return eof;

-    }

-  }

+		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];

+		fileLen = fl;  bufLen = bl;

+		base();

+		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)

+		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid

+		if (bufLen == fileLen && s.CanSeek) Close();

+	}

+	

+	protected Buffer(Buffer! b) { // called in UTF8Buffer constructor

+		buf = b.buf;

+		bufStart = b.bufStart;

+		bufLen = b.bufLen;

+		fileLen = b.fileLen;

+		bufPos = b.bufPos;

+		stream = b.stream;

+		// keep destructor from closing the stream

+		//b.stream = null;

+		isUserStream = b.isUserStream;

+		// keep destructor from closing the stream

+		b.isUserStream = true;

+	}

 

-  public static string/*!*/ ReadToEOL() {

-    int x = buf.IndexOf('\n', pos);

-    if (x == -1) {

-      string s = buf.Substring(pos);

-      pos = buf.Length;

-      return s;

-    } else {

-      string s = buf.Substring(pos, x+1 - pos);  // also include the '\n'

-      pos = x+1;

-      return s;

-    }

-  }

+	~Buffer() { Close(); }

+	

+	protected void Close() {

+		if (!isUserStream && stream != null) {

+			stream.Close();

+			//stream = null;

+		}

+	}

+	

+	public virtual int Read () {

+		if (bufPos < bufLen) {

+			return buf[bufPos++];

+		} else if (Pos < fileLen) {

+			Pos = Pos; // shift buffer start to Pos

+			return buf[bufPos++];

+		} else if (stream != null && !stream.CanSeek && ReadNextStreamChunk() > 0) {

+			return buf[bufPos++];

+		} else {

+			return EOF;

+		}

+	}

 

-  public static int Pos {

-    get { return pos; }

-    set {

-      if (value < 0) pos = 0; else if (value >= bufLen) pos = bufLen; else pos = value;

-    }

-  }

-}

+	public int Peek () {

+		int curPos = Pos;

+		int ch = Read();

+		Pos = curPos;

+		return ch;

+	}

+	

+	public string! GetString (int beg, int end) {

+		int len = 0;

+		char[] buf = new char[end - beg];

+		int oldPos = Pos;

+		Pos = beg;

+		while (Pos < end) buf[len++] = (char) Read();

+		Pos = oldPos;

+		return new String(buf, 0, len);

+	}

 

+	public int Pos {

+		get { return bufPos + bufStart; }

+		set {

+			if (value >= fileLen && stream != null && !stream.CanSeek) {

+				// Wanted position is after buffer and the stream

+				// is not seek-able e.g. network or console,

+				// thus we have to read the stream manually till

+				// the wanted position is in sight.

+				while (value >= fileLen && ReadNextStreamChunk() > 0);

+			}

 

+			if (value < 0 || value > fileLen) {

+				throw new FatalError("buffer out of bounds access, position: " + value);

+			}

 

+			if (value >= bufStart && value < bufStart + bufLen) { // already in buffer

+				bufPos = value - bufStart;

+			} else if (stream != null) { // must be swapped in

+				stream.Seek(value, SeekOrigin.Begin);

+				bufLen = stream.Read(buf, 0, buf.Length);

+				bufStart = value; bufPos = 0;

+			} else {

+				// set the position to the end of the file, Pos will return fileLen.

+				bufPos = fileLen - bufStart;

+			}

+		}

+	}

+	

+	// Read the next chunk of bytes from the stream, increases the buffer

+	// if needed and updates the fields fileLen and bufLen.

+	// Returns the number of bytes read.

+	private int ReadNextStreamChunk() {

+		int free = buf.Length - bufLen;

+		if (free == 0) {

+			// in the case of a growing input stream

+			// we can neither seek in the stream, nor can we

+			// foresee the maximum length, thus we must adapt

+			// the buffer size on demand.

+			byte[] newBuf = new byte[bufLen * 2];

+			Array.Copy(buf, newBuf, bufLen);

+			buf = newBuf;

+			free = bufLen;

+		}

+		int read = stream.Read(buf, bufLen, free);

+		if (read > 0) {

+			fileLen = bufLen = (bufLen + read);

+			return read;

+		}

+		// end of stream reached

+		return 0;

+	}

+}

+

+//-----------------------------------------------------------------------------------

+// UTF8Buffer

+//-----------------------------------------------------------------------------------

+public class UTF8Buffer: Buffer {

+	public UTF8Buffer(Buffer! b): base(b) {}

+

+	public override int Read() {

+		int ch;

+		do {

+			ch = base.Read();

+			// until we find a utf8 start (0xxxxxxx or 11xxxxxx)

+		} while ((ch >= 128) && ((ch & 0xC0) != 0xC0) && (ch != EOF));

+		if (ch < 128 || ch == EOF) {

+			// nothing to do, first 127 chars are the same in ascii and utf8

+			// 0xxxxxxx or end of file character

+		} else if ((ch & 0xF0) == 0xF0) {

+			// 11110xxx 10xxxxxx 10xxxxxx 10xxxxxx

+			int c1 = ch & 0x07; ch = base.Read();

+			int c2 = ch & 0x3F; ch = base.Read();

+			int c3 = ch & 0x3F; ch = base.Read();

+			int c4 = ch & 0x3F;

+			ch = (((((c1 << 6) | c2) << 6) | c3) << 6) | c4;

+		} else if ((ch & 0xE0) == 0xE0) {

+			// 1110xxxx 10xxxxxx 10xxxxxx

+			int c1 = ch & 0x0F; ch = base.Read();

+			int c2 = ch & 0x3F; ch = base.Read();

+			int c3 = ch & 0x3F;

+			ch = (((c1 << 6) | c2) << 6) | c3;

+		} else if ((ch & 0xC0) == 0xC0) {

+			// 110xxxxx 10xxxxxx

+			int c1 = ch & 0x1F; ch = base.Read();

+			int c2 = ch & 0x3F;

+			ch = (c1 << 6) | c2;

+		}

+		return ch;

+	}

+}

+

+//-----------------------------------------------------------------------------------

+// Scanner

+//-----------------------------------------------------------------------------------

 public class Scanner {

-  const char EOF = '\0';

-  const char CR  = '\r';

-  const char LF  = '\n';

-  [Microsoft.Contracts.Verify(false)]

+	const char EOL = '\n';

+	const int eofSym = 0; /* pdt */

+	const int maxT = 88;

+	const int noSym = 88;

+

+

+	public Buffer! buffer; // scanner buffer

+	

+	Token! t;          // current token

+	int ch;           // current input character

+	int pos;          // byte position of current character

+	int col;          // column number of current character

+	int line;         // line number of current character

+	int oldEols;      // EOLs that appeared in a comment;

+	static readonly Hashtable! start; // maps first token character to start state

+

+	Token! tokens;     // list of tokens already peeked (first token is a dummy)

+	Token! pt;         // current peek token

+	

+	char[]! tval = new char[128]; // text of current token

+	int tlen;         // length of current token

+	

+	private string! Filename;

+	private Errors! errorHandler;

+	

 	static Scanner() {

-		start[0] = 58;

-		start[33] = 41;

-		start[34] = 6;

-		start[35] = 2;

-		start[36] = 2;

-		start[37] = 51;

-		start[38] = 34;

-		start[39] = 2;

-		start[40] = 11;

-		start[41] = 12;

-		start[42] = 24;

-		start[43] = 47;

-		start[44] = 14;

-		start[45] = 49;

-		start[46] = 2;

-		start[47] = 50;

-		start[48] = 9;

-		start[49] = 9;

-		start[50] = 9;

-		start[51] = 9;

-		start[52] = 9;

-		start[53] = 9;

-		start[54] = 9;

-		start[55] = 9;

-		start[56] = 9;

-		start[57] = 9;

-		start[58] = 13;

-		start[59] = 10;

-		start[60] = 17;

-		start[61] = 21;

-		start[62] = 18;

-		start[63] = 2;

-		start[65] = 2;

-		start[66] = 2;

-		start[67] = 2;

-		start[68] = 2;

-		start[69] = 2;

-		start[70] = 2;

-		start[71] = 2;

-		start[72] = 2;

-		start[73] = 2;

-		start[74] = 2;

-		start[75] = 2;

-		start[76] = 2;

-		start[77] = 2;

-		start[78] = 2;

-		start[79] = 2;

-		start[80] = 2;

-		start[81] = 2;

-		start[82] = 2;

-		start[83] = 2;

-		start[84] = 2;

-		start[85] = 2;

-		start[86] = 2;

-		start[87] = 2;

-		start[88] = 2;

-		start[89] = 2;

-		start[90] = 2;

-		start[91] = 15;

-		start[92] = 1;

-		start[93] = 16;

-		start[94] = 2;

-		start[95] = 2;

-		start[96] = 2;

-		start[97] = 2;

-		start[98] = 2;

-		start[99] = 2;

-		start[100] = 2;

-		start[101] = 2;

-		start[102] = 2;

-		start[103] = 2;

-		start[104] = 2;

-		start[105] = 2;

-		start[106] = 2;

-		start[107] = 2;

-		start[108] = 2;

-		start[109] = 2;

-		start[110] = 2;

-		start[111] = 2;

-		start[112] = 2;

-		start[113] = 2;

-		start[114] = 2;

-		start[115] = 2;

-		start[116] = 2;

-		start[117] = 2;

-		start[118] = 2;

-		start[119] = 2;

-		start[120] = 2;

-		start[121] = 2;

-		start[122] = 2;

-		start[123] = 19;

-		start[124] = 37;

-		start[125] = 20;

-		start[126] = 2;

-		start[172] = 52;

-		start[955] = 55;

-		start[8226] = 57;

-		start[8656] = 33;

-		start[8658] = 32;

-		start[8660] = 29;

-		start[8704] = 53;

-		start[8707] = 54;

-		start[8743] = 36;

-		start[8744] = 39;

-		start[8800] = 44;

-		start[8804] = 45;

-		start[8805] = 46;

+		start = new Hashtable(128);

+		for (int i = 35; i <= 36; ++i) start[i] = 2;

+		for (int i = 39; i <= 39; ++i) start[i] = 2;

+		for (int i = 46; i <= 46; ++i) start[i] = 2;

+		for (int i = 63; i <= 63; ++i) start[i] = 2;

+		for (int i = 65; i <= 90; ++i) start[i] = 2;

+		for (int i = 94; i <= 122; ++i) start[i] = 2;

+		for (int i = 126; i <= 126; ++i) start[i] = 2;

+		for (int i = 48; i <= 57; ++i) start[i] = 9;

+		for (int i = 34; i <= 34; ++i) start[i] = 6;

+		start[92] = 1; 

+		start[59] = 10; 

+		start[40] = 11; 

+		start[41] = 12; 

+		start[58] = 47; 

+		start[44] = 13; 

+		start[91] = 14; 

+		start[93] = 15; 

+		start[60] = 48; 

+		start[62] = 49; 

+		start[123] = 50; 

+		start[125] = 51; 

+		start[61] = 52; 

+		start[42] = 18; 

+		start[8660] = 21; 

+		start[8658] = 23; 

+		start[8656] = 24; 

+		start[38] = 25; 

+		start[8743] = 27; 

+		start[124] = 28; 

+		start[8744] = 30; 

+		start[33] = 53; 

+		start[8800] = 34; 

+		start[8804] = 35; 

+		start[8805] = 36; 

+		start[43] = 54; 

+		start[45] = 38; 

+		start[47] = 39; 

+		start[37] = 40; 

+		start[172] = 41; 

+		start[8704] = 42; 

+		start[8707] = 43; 

+		start[955] = 44; 

+		start[8226] = 46; 

+		start[Buffer.EOF] = -1;

+

 	}

-	const int noSym = 88;

-	static short[] start = new short[16385];

-

-

-  static Token/*!*/ t;          // current token

-  static char ch;               // current input character

-  static int pos;               // column number of current character

-  static int line;              // line number of current character

-  static int lineStart;         // start position of current line

-  static Queue! oldEols;        // EOLs that appeared in a comment;

-  static BitArray/*!*/ ignore;  // set of characters to be ignored by the scanner  

-  static string Filename;

-

-  ///<summary>

-  ///Initializes the scanner. Note: first fill the Buffer.

-  ///</summary>

-  ///<param name="filename">File name used for error reporting</param>

-  public static void Init (string filename) {

-    Filename = filename;

-    pos = -1; line = 1; lineStart = 0;

-    oldEols = new Queue();

-    NextCh();

-		ignore = new BitArray(16384);

-		ignore[9] = true; ignore[10] = true; ignore[13] = true; ignore[32] = true; 

-		

-  }

-  

-  private static void NextCh() {

-    if (oldEols.Count > 0) {

-      ch = (char) ((!)oldEols.Dequeue());

-    } else {

-      while (true) {

-        ch = (char)Buffer.Read(); pos++;

-        if (ch == Buffer.eof) {

-          ch = EOF;

-        } else if (ch == LF) {

-          line++;

-          lineStart = pos + 1;

-

-        } else if (ch == '#' && pos == lineStart) {

-          int prLine = line;

-          int prColumn = pos - lineStart;  // which is 0

-

-          string hashLine = Buffer.ReadToEOL();  pos += hashLine.Length;

-          line++;

-          lineStart = pos + 1;

-

-          hashLine = hashLine.TrimEnd(null);

-          if (hashLine.StartsWith("line ") || hashLine == "line") {

-            // parse #line pragma:  #line num [filename]

-            string h = hashLine.Substring(4).TrimStart(null);

-            int x = h.IndexOf(' ');

-            if (x == -1) {

-              x = h.Length;  // this will be convenient below when we look for a filename

-            }

-            try {

-              int li = int.Parse(h.Substring(0, x));

-

-              h = h.Substring(x).Trim();

-

-              // act on #line

-              line = li;

-              if (h.Length != 0) {

-                // a filename was specified

-                Filename = h;

-              }

-              continue;  // successfully parsed and acted on the #line pragma

-

-            } catch (FormatException) {

-              // just fall down through to produce an error message

-            }

-            Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);

-            continue;

-          }

-

-          Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);

-          continue;

-        }

-        return;

-      }

-    }

-  }

-  

-
-	static bool Comment0() {

-		int level = 1, line0 = line, lineStart0 = lineStart;

+	

+	[NotDelayed]

+	public Scanner (string! fileName, Errors! errorHandler) {

+		this.errorHandler = errorHandler;

+		pt = tokens = new Token();  // first token is a dummy

+		t = new Token(); // dummy because t is a non-null field

+		try {

+			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

+			buffer = new Buffer(stream, false);

+			Filename = fileName;

+			base();

+			Init();

+		} catch (IOException) {

+			throw new FatalError("Cannot open file " + fileName);

+		}

+	}

+	

+	[NotDelayed]

+	public Scanner (Stream! s, Errors! errorHandler, string! fileName) {

+		pt = tokens = new Token();  // first token is a dummy

+		t = new Token(); // dummy because t is a non-null field

+		buffer = new Buffer(s, true);

+		this.errorHandler = errorHandler;

+		this.Filename = fileName;

+		base();

+		Init();

+	}

+	

+	void Init() {

+		pos = -1; line = 1; col = 0;

+		oldEols = 0;

+		NextCh();

+		if (ch == 0xEF) { // check optional byte order mark for UTF-8

+			NextCh(); int ch1 = ch;

+			NextCh(); int ch2 = ch;

+			if (ch1 != 0xBB || ch2 != 0xBF) {

+				throw new FatalError(String.Format("illegal byte order mark: EF {0,2:X} {1,2:X}", ch1, ch2));

+			}

+			buffer = new UTF8Buffer(buffer); col = 0;

+			NextCh();

+		}

+		pt = tokens = new Token();  // first token is a dummy

+	}

+

+	string! ReadToEOL(){

+	  int p = buffer.Pos;

+	  int ch = buffer.Read();

+      // replace isolated '\r' by '\n' in order to make

+	  // eol handling uniform across Windows, Unix and Mac

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

+	  while (ch != EOL && ch != Buffer.EOF){

+	    ch = buffer.Read();

+		// replace isolated '\r' by '\n' in order to make

+		// eol handling uniform across Windows, Unix and Mac

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

+	  }

+	  string! s = buffer.GetString(p, buffer.Pos);

+	  return s;

+	}

+

+	void NextCh() {

+		if (oldEols > 0) { ch = EOL; oldEols--; } 

+		else {

+//			pos = buffer.Pos;

+//			ch = buffer.Read(); col++;

+//			// replace isolated '\r' by '\n' in order to make

+//			// eol handling uniform across Windows, Unix and Mac

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

+//			if (ch == EOL) { line++; col = 0; }

+			

+			while (true) {

+			    pos = buffer.Pos;

+				ch = buffer.Read(); col++;

+				// replace isolated '\r' by '\n' in order to make

+				// eol handling uniform across Windows, Unix and Mac

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

+				if (ch == EOL) {

+					line++; col = 0; 

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

+				  int prLine = line;

+				  int prColumn = 0;

+

+				  string! hashLine = ReadToEOL();

+				  col = 0;

+				  line++;

+

+				  hashLine = hashLine.TrimEnd(null);

+				  if (hashLine.StartsWith("line ") || hashLine == "line") {

+					// parse #line pragma:  #line num [filename]

+					string h = hashLine.Substring(4).TrimStart(null);

+					int x = h.IndexOf(' ');

+					if (x == -1) {

+					  x = h.Length;  // this will be convenient below when we look for a filename

+					}

+					try {

+					  int li = int.Parse(h.Substring(0, x));

+

+					  h = h.Substring(x).Trim();

+

+					  // act on #line

+					  line = li;

+					  if (h.Length != 0) {

+						// a filename was specified

+						Filename = h;

+					  }

+					  continue;  // successfully parsed and acted on the #line pragma

+

+					} catch (FormatException) {

+					  // just fall down through to produce an error message

+					}

+					this.errorHandler.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);

+					continue;

+				  }

+

+				  this.errorHandler.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);

+				  continue;

+				}

+				return;

+			  }

+

+			

+		}

+

+	}

+

+	void AddCh() {

+		if (tlen >= tval.Length) {

+			char[] newBuf = new char[2 * tval.Length];

+			Array.Copy(tval, 0, newBuf, 0, tval.Length);

+			tval = newBuf;

+		}

+		if (ch != Buffer.EOF) {

+			tval[tlen++] = (char) ch;

+			NextCh();

+		}

+	}

+

+

+

+	bool Comment0() {

+		int level = 1, pos0 = pos, line0 = line, col0 = col;

 		NextCh();

 		if (ch == '/') {

 			NextCh();

 			for(;;) {

 				if (ch == 10) {

 					level--;

-					if (level == 0) {

-						while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}

-						NextCh(); return true;

-					}

+					if (level == 0) { oldEols = line - line0; NextCh(); return true; }

 					NextCh();

-				} else if (ch == EOF) return false;

+				} else if (ch == Buffer.EOF) return false;

 				else NextCh();

 			}

 		} else {

-			if (ch==CR) {line--; lineStart = lineStart0;}

-			pos = pos - 2; Buffer.Pos = pos+1; NextCh();

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

 		}

 		return false;

 	}

-
-	static bool Comment1() {

-		int level = 1, line0 = line, lineStart0 = lineStart;

+

+	bool Comment1() {

+		int level = 1, pos0 = pos, line0 = line, col0 = col;

 		NextCh();

 		if (ch == '*') {

 			NextCh();

@@ -463,10 +508,7 @@ public class Scanner {
 					NextCh();

 					if (ch == '/') {

 						level--;

-						if (level == 0) {

-							while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}

-							NextCh(); return true;

-						}

+						if (level == 0) { oldEols = line - line0; NextCh(); return true; }

 						NextCh();

 					}

 				} else if (ch == '/') {

@@ -474,19 +516,18 @@ public class Scanner {
 					if (ch == '*') {

 						level++; NextCh();

 					}

-				} else if (ch == EOF) return false;

+				} else if (ch == Buffer.EOF) return false;

 				else NextCh();

 			}

 		} else {

-			if (ch==CR) {line--; lineStart = lineStart0;}

-			pos = pos - 2; Buffer.Pos = pos+1; NextCh();

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

 		}

 		return false;

 	}

 

-  

-  static void CheckLiteral() {

-    switch (t.val) {

+

+	void CheckLiteral() {

+		switch (t.val) {

 			case "var": t.kind = 6; break;

 			case "where": t.kind = 12; break;

 			case "int": t.kind = 13; break;

@@ -524,197 +565,229 @@ public class Scanner {
 			case "exists": t.kind = 82; break;

 			case "lambda": t.kind = 84; break;

 			default: break;

+		}

+	}

 

-    }

-  }

-

-  public static Token/*!*/ Scan() {

-    while (ignore[ch]) { NextCh(); }

-		if (ch == '/' && Comment0()  || ch == '/' && Comment1() ) return Scan();

-    t = new Token();

-    t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename;

-    int state = (/*^ (!) ^*/ start)[ch];

-    StringBuilder buf = new StringBuilder(16);

-    buf.Append(ch); NextCh();

-    

-    switch (state) {

-      case 0: {t.kind = noSym; goto done;} // NextCh already done

+	Token! NextToken() {

+		while (ch == ' ' ||

+			ch >= 9 && ch <= 10 || ch == 13

+		) NextCh();

+		if (ch == '/' && Comment0() ||ch == '/' && Comment1()) return NextToken();

+		int recKind = noSym;

+		int recEnd = pos;

+		t = new Token();

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

+		t.filename = this.Filename;

+		int state;

+		if (start.ContainsKey(ch)) { state = (int) (!) start[ch]; }

+		else { state = 0; }

+		tlen = 0; AddCh();

+		

+		switch (state) {

+			case -1: { t.kind = eofSym; break; } // NextCh already done

+			case 0: {

+				if (recKind != noSym) {

+					tlen = recEnd - t.pos;

+					SetScannerBehindT();

+				}

+				t.kind = recKind; break;

+			} // NextCh already done

 			case 1:

-				if ((ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~')) {buf.Append(ch); NextCh(); goto case 2;}

-				else {t.kind = noSym; goto done;}

+				if (ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~') {AddCh(); goto case 2;}

+				else {goto case 0;}

 			case 2:

-				if ((ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~')) {buf.Append(ch); NextCh(); goto case 2;}

-				else {t.kind = 1; t.val = buf.ToString(); CheckLiteral(); return t;}

+				recEnd = pos; recKind = 1;

+				if (ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~') {AddCh(); goto case 2;}

+				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}

 			case 3:

-				if (ch == 'v') {buf.Append(ch); NextCh(); goto case 4;}

-				else {t.kind = noSym; goto done;}

+				if (ch == 'v') {AddCh(); goto case 4;}

+				else {goto case 0;}

 			case 4:

-				if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 5;}

-				else {t.kind = noSym; goto done;}

+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 5;}

+				else {goto case 0;}

 			case 5:

-				if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 5;}

-				else {t.kind = 2; goto done;}

+				recEnd = pos; recKind = 2;

+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 5;}

+				else {t.kind = 2; break;}

 			case 6:

-				if ((ch == '"')) {buf.Append(ch); NextCh(); goto case 7;}

-				else if ((ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~')) {buf.Append(ch); NextCh(); goto case 6;}

-				else {t.kind = noSym; goto done;}

+				if (ch == '"') {AddCh(); goto case 7;}

+				else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 6;}

+				else {goto case 0;}

 			case 7:

-				{t.kind = 4; goto done;}

+				{t.kind = 4; break;}

 			case 8:

-				if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 8;}

-				else {t.kind = 5; goto done;}

+				recEnd = pos; recKind = 5;

+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 8;}

+				else {t.kind = 5; break;}

 			case 9:

-				if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 9;}

-				else if (ch == 'b') {buf.Append(ch); NextCh(); goto case 3;}

-				else if (ch == '.') {buf.Append(ch); NextCh(); goto case 8;}

-				else {t.kind = 3; goto done;}

+				recEnd = pos; recKind = 3;

+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}

+				else if (ch == 'b') {AddCh(); goto case 3;}

+				else if (ch == '.') {AddCh(); goto case 8;}

+				else {t.kind = 3; break;}

 			case 10:

-				{t.kind = 7; goto done;}

+				{t.kind = 7; break;}

 			case 11:

-				{t.kind = 8; goto done;}

+				{t.kind = 8; break;}

 			case 12:

-				{t.kind = 9; goto done;}

+				{t.kind = 9; break;}

 			case 13:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 25;}

-				else if (ch == ':') {buf.Append(ch); NextCh(); goto case 56;}

-				else {t.kind = 10; goto done;}

+				{t.kind = 11; break;}

 			case 14:

-				{t.kind = 11; goto done;}

+				{t.kind = 15; break;}

 			case 15:

-				{t.kind = 15; goto done;}

+				{t.kind = 16; break;}

 			case 16:

-				{t.kind = 16; goto done;}

+				{t.kind = 36; break;}

 			case 17:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 26;}

-				else if (ch == ':') {buf.Append(ch); NextCh(); goto case 43;}

-				else {t.kind = 17; goto done;}

+				{t.kind = 37; break;}

 			case 18:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 40;}

-				else {t.kind = 18; goto done;}

+				{t.kind = 44; break;}

 			case 19:

-				if (ch == '{') {buf.Append(ch); NextCh(); goto case 22;}

-				else {t.kind = 25; goto done;}

+				{t.kind = 49; break;}

 			case 20:

-				if (ch == '}') {buf.Append(ch); NextCh(); goto case 23;}

-				else {t.kind = 26; goto done;}

+				{t.kind = 52; break;}

 			case 21:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 30;}

-				else {t.kind = 29; goto done;}

+				{t.kind = 53; break;}

 			case 22:

-				{t.kind = 36; goto done;}

+				{t.kind = 54; break;}

 			case 23:

-				{t.kind = 37; goto done;}

+				{t.kind = 55; break;}

 			case 24:

-				{t.kind = 44; goto done;}

+				{t.kind = 57; break;}

 			case 25:

-				{t.kind = 49; goto done;}

+				if (ch == '&') {AddCh(); goto case 26;}

+				else {goto case 0;}

 			case 26:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 27;}

-				else {t.kind = 63; goto done;}

+				{t.kind = 58; break;}

 			case 27:

-				if (ch == '>') {buf.Append(ch); NextCh(); goto case 28;}

-				else {t.kind = 56; goto done;}

+				{t.kind = 59; break;}

 			case 28:

-				{t.kind = 52; goto done;}

+				if (ch == '|') {AddCh(); goto case 29;}

+				else {goto case 0;}

 			case 29:

-				{t.kind = 53; goto done;}

+				{t.kind = 60; break;}

 			case 30:

-				if (ch == '>') {buf.Append(ch); NextCh(); goto case 31;}

-				else {t.kind = 62; goto done;}

+				{t.kind = 61; break;}

 			case 31:

-				{t.kind = 54; goto done;}

+				{t.kind = 64; break;}

 			case 32:

-				{t.kind = 55; goto done;}

+				{t.kind = 65; break;}

 			case 33:

-				{t.kind = 57; goto done;}

+				{t.kind = 66; break;}

 			case 34:

-				if (ch == '&') {buf.Append(ch); NextCh(); goto case 35;}

-				else {t.kind = noSym; goto done;}

+				{t.kind = 67; break;}

 			case 35:

-				{t.kind = 58; goto done;}

+				{t.kind = 68; break;}

 			case 36:

-				{t.kind = 59; goto done;}

+				{t.kind = 69; break;}

 			case 37:

-				if (ch == '|') {buf.Append(ch); NextCh(); goto case 38;}

-				else {t.kind = noSym; goto done;}

+				{t.kind = 70; break;}

 			case 38:

-				{t.kind = 60; goto done;}

+				{t.kind = 72; break;}

 			case 39:

-				{t.kind = 61; goto done;}

+				{t.kind = 73; break;}

 			case 40:

-				{t.kind = 64; goto done;}

+				{t.kind = 74; break;}

 			case 41:

-				if (ch == '=') {buf.Append(ch); NextCh(); goto case 42;}

-				else {t.kind = 75; goto done;}

+				{t.kind = 76; break;}

 			case 42:

-				{t.kind = 65; goto done;}

+				{t.kind = 81; break;}

 			case 43:

-				{t.kind = 66; goto done;}

+				{t.kind = 83; break;}

 			case 44:

-				{t.kind = 67; goto done;}

+				{t.kind = 85; break;}

 			case 45:

-				{t.kind = 68; goto done;}

+				{t.kind = 86; break;}

 			case 46:

-				{t.kind = 69; goto done;}

+				{t.kind = 87; break;}

 			case 47:

-				if (ch == '+') {buf.Append(ch); NextCh(); goto case 48;}

-				else {t.kind = 71; goto done;}

+				recEnd = pos; recKind = 10;

+				if (ch == '=') {AddCh(); goto case 19;}

+				else if (ch == ':') {AddCh(); goto case 45;}

+				else {t.kind = 10; break;}

 			case 48:

-				{t.kind = 70; goto done;}

+				recEnd = pos; recKind = 17;

+				if (ch == '=') {AddCh(); goto case 55;}

+				else if (ch == ':') {AddCh(); goto case 33;}

+				else {t.kind = 17; break;}

 			case 49:

-				{t.kind = 72; goto done;}

+				recEnd = pos; recKind = 18;

+				if (ch == '=') {AddCh(); goto case 31;}

+				else {t.kind = 18; break;}

 			case 50:

-				{t.kind = 73; goto done;}

+				recEnd = pos; recKind = 25;

+				if (ch == '{') {AddCh(); goto case 16;}

+				else {t.kind = 25; break;}

 			case 51:

-				{t.kind = 74; goto done;}

+				recEnd = pos; recKind = 26;

+				if (ch == '}') {AddCh(); goto case 17;}

+				else {t.kind = 26; break;}

 			case 52:

-				{t.kind = 76; goto done;}

+				recEnd = pos; recKind = 29;

+				if (ch == '=') {AddCh(); goto case 56;}

+				else {t.kind = 29; break;}

 			case 53:

-				{t.kind = 81; goto done;}

+				recEnd = pos; recKind = 75;

+				if (ch == '=') {AddCh(); goto case 32;}

+				else {t.kind = 75; break;}

 			case 54:

-				{t.kind = 83; goto done;}

+				recEnd = pos; recKind = 71;

+				if (ch == '+') {AddCh(); goto case 37;}

+				else {t.kind = 71; break;}

 			case 55:

-				{t.kind = 85; goto done;}

+				recEnd = pos; recKind = 63;

+				if (ch == '=') {AddCh(); goto case 57;}

+				else {t.kind = 63; break;}

 			case 56:

-				{t.kind = 86; goto done;}

+				recEnd = pos; recKind = 62;

+				if (ch == '>') {AddCh(); goto case 22;}

+				else {t.kind = 62; break;}

 			case 57:

-				{t.kind = 87; goto done;}

-			case 58: {t.kind = 0; goto done;}

-    }

-    done:

-    t.val = buf.ToString();

-    return t;

-  }

+				recEnd = pos; recKind = 56;

+				if (ch == '>') {AddCh(); goto case 20;}

+				else {t.kind = 56; break;}

 

-} // end Scanner

+		}

+		t.val = new String(tval, 0, tlen);

+		return t;

+	}

+	

+	private void SetScannerBehindT() {

+		buffer.Pos = t.pos;

+		NextCh();

+		line = t.line; col = t.col;

+		for (int i = 0; i < tlen; i++) NextCh();

+	}

+	

+	// get the next token (possibly a token already seen during peeking)

+	public Token! Scan () {

+		if (tokens.next == null) {

+			return NextToken();

+		} else {

+			pt = tokens = tokens.next;

+			return tokens;

+		}

+	}

 

+	// peek for the next token, ignore pragmas

+	public Token! Peek () {

+		do {

+			if (pt.next == null) {

+				pt.next = NextToken();

+			}

+			pt = pt.next;

+		} while (pt.kind > maxT); // skip pragmas

+	

+		return pt;

+	}

 

-public delegate void ErrorProc(int n, string filename, int line, int col);

+	// make sure that peeking starts at the current scan position

+	public void ResetPeek () { pt = tokens; }

 

-public class Errors {

-  public static int count = 0;  // number of errors detected

-  public static ErrorProc/*!*/ SynErr;  // syntactic errors

-  

-  public static void SemErr(string filename, int line, int col, string! msg) {  // semantic errors

-    ConsoleColor color = Console.ForegroundColor;

-    Console.ForegroundColor = ConsoleColor.Red;

-    Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg);

-    Console.ForegroundColor = color;

-    count++;

-  }

-  

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

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

-  }

-  

-  public static void Exception (string s) {

-    ConsoleColor color = Console.ForegroundColor;

-    Console.ForegroundColor = ConsoleColor.Red;

-    Console.WriteLine(s);

-    Console.ForegroundColor = color;

-    System.Environment.Exit(0);

-  }

+} // end Scanner

+

+public delegate void ErrorProc(int n, string filename, int line, int col);

 

-} // Errors

 

-} // end namespace

+}
\ No newline at end of file
diff --git a/Source/Core/parser.frame b/Source/Core/parser.frame
deleted file mode 100644
index c7818e57..00000000
--- a/Source/Core/parser.frame
+++ /dev/null
@@ -1,103 +0,0 @@
-

-using System;

-using Microsoft.Contracts;

-

-namespace -->namespace {

-

-public class Parser {

--->constants

-	const bool T = true;

-	const bool x = false;

-	const int minErrDist = 2;

-	

-	static Token/*!*/ token;			// last recognized token

-	static Token/*!*/ t;				// lookahead token

-	static int errDist = minErrDist;

-

-	-->declarations

-

-	static void Error(int n) {

-		if (errDist >= minErrDist) Errors.SynErr(n, t.filename, t.line, t.col);

-		errDist = 0;

-	}

-	

-	public static void SemErr(string! msg) {

-		if (errDist >= minErrDist) Errors.SemErr(token.filename, token.line, token.col, msg);

-		errDist = 0;

-	}

-

-	public static void SemErr(IToken! tok, string! msg) {

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

-	}

-

-	static void Get() {

-		for (;;) {

-			token = t;

-			t = Scanner.Scan();

-			if (t.kind<=maxT) {errDist++; return;}

--->pragmas

-			t = token;

-		}

-	}

-	

-	static void Expect(int n) {

-		if (t.kind==n) Get(); else Error(n);

-	}

-	

-	static bool StartOf(int s) {

-		return set[s, t.kind];

-	}

-	

-	static void ExpectWeak(int n, int follow) {

-		if (t.kind == n) Get();

-		else {

-			Error(n);

-			while (!StartOf(follow)) Get();

-		}

-	}

-	

-	static bool WeakSeparator(int n, int syFol, int repFol) {

-		bool[] s = new bool[maxT+1];

-		if (t.kind == n) {Get(); return true;}

-		else if (StartOf(repFol)) return false;

-		else {

-			for (int i=0; i <= maxT; i++) {

-				s[i] = set[syFol, i] || set[repFol, i] || set[0, i];

-			}

-			Error(n);

-			while (!s[t.kind]) Get();

-			return StartOf(syFol);

-		}

-	}

-	

--->productions

-

-	public static void Parse() {

-		Errors.SynErr = new ErrorProc(SynErr);

-		t = new Token();

-		Get();

--->parseRoot

-	}

-

-	[Microsoft.Contracts.Verify(false)]

-	static void SynErr(int n, string filename, int line, int col) {

-		Errors.count++;

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

-		string s;

-		switch (n) {

--->errors

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

-		}

-		Console.WriteLine(s);

-	}

-

-	static bool[,]! set = {

--->initialization

-	};

-

-	[Microsoft.Contracts.Verify(false)]

-	static Parser() {}

-} // end Parser

-

-} // end namespace

-$$$

diff --git a/Source/Core/scanner.frame b/Source/Core/scanner.frame
deleted file mode 100644
index b9a2ce02..00000000
--- a/Source/Core/scanner.frame
+++ /dev/null
@@ -1,377 +0,0 @@
-using System;

-using System.IO;

-using System.Collections;

-using System.Collections.Generic;

-using System.Text;

-using Microsoft.Contracts;

-

-

-namespace Microsoft.Boogie {

-

-  [Immutable]

-  public interface IToken {

-    int kind {get; set; }         // token kind

-    string filename {get; set; }  // token file

-    int pos {get; set; }          // token position in the source text (starting at 0)

-    int col {get; set; }          // token column (starting at 0)

-    int line {get; set; }         // token line (starting at 1)

-    string/*!*/ val {get; set; }  // token value

-

-    bool IsValid { get; }

-  }

-  

-  [Immutable]

-  public class Token : IToken {

-    int _kind;         // token kind

-    string _filename;  // token file

-    int _pos;          // token position in the source text (starting at 0)

-    int _col;          // token column (starting at 0)

-    int _line;         // token line (starting at 1)

-    string/*!*/ _val = "foo";  // token value

-

-    public static IToken! NoToken = new Token();

-

-    public Token();

-    public Token(int linenum, int colnum) {

-      this._line = linenum;

-      this._col = colnum;

-      base();

-    }

-

-    public int kind {

-      get { return this._kind; }

-      set { this._kind = value; }

-    }

-    

-    public string filename{

-      get { return this._filename; }

-      set { this._filename = value; }

-    }

-    

-    public int pos{

-      get { return this._pos; }

-      set { this._pos = value; }

-    }

-    

-    public int col{

-      get { return this._col; }

-      set { this._col = value; }

-    }

-    

-    public int line{

-      get { return this._line; }

-      set { this._line = value; }

-    }

-    

-    public string/*!*/ val{

-      get { return this._val; }

-      set { this._val = value; }

-    }

-    

-    public bool IsValid { get { return this._filename != null; } }

-  }

-

-}

-

-namespace -->namespace {

-

-using Microsoft.Boogie;

-

-public class Buffer {

-  static string/*!*/ buf;

-  static int bufLen;

-  static int pos;

-  public const int eof = '\uffff';

-  

-  public static void Fill(TextReader! reader) {

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

-    Fill(reader, defines);

-  }

-  

-  struct ReadState {

-    public bool hasSeenElse;

-    public bool mayStillIncludeAnotherAlternative;

-    public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) {

-      this.hasSeenElse = hasSeenElse;

-      this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative;

-    }

-  }

-  

-  public static void Fill(TextReader! reader, List<string!>! defines) {

-    StringBuilder sb = new StringBuilder();

-    List<ReadState>! readState = new List<ReadState>();  // readState.Count is the current nesting level of #if's

-    int ignoreCutoff = -1;  // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n

-    while (true)

-      invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count;

-    {

-      string s = reader.ReadLine();

-      if (s == null) {

-        if (readState.Count != 0) {

-          sb.AppendLine("#MalformedInput: missing #endif");

-        }

-        break;

-      }

-      string t = s.Trim();

-      if (t.StartsWith("#if")) {

-        ReadState rs = new ReadState(false, false);

-        if (ignoreCutoff != -1) {

-          // we're already in a state of ignoring, so continue to ignore

-        } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) {

-          // include this branch

-        } else {

-          ignoreCutoff = readState.Count;  // start ignoring

-          rs.mayStillIncludeAnotherAlternative = true;  // allow some later "elsif" or "else" branch to be included

-        }

-        readState.Add(rs);

-        sb.AppendLine();  // ignore the #if line

-

-      } else if (t.StartsWith("#elsif")) {

-        ReadState rs;

-        if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) {

-          sb.AppendLine("#MalformedInput: misplaced #elsif");  // malformed input

-          break;

-        }

-        if (ignoreCutoff == -1) {

-          // we had included the previous branch

-          assert !rs.mayStillIncludeAnotherAlternative;

-          ignoreCutoff = readState.Count-1;  // start ignoring

-        } else if (rs.mayStillIncludeAnotherAlternative && IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) {

-          // include this branch, but no subsequent branch at this level

-          ignoreCutoff = -1;

-          rs.mayStillIncludeAnotherAlternative = false;

-          readState[readState.Count-1] = rs;

-        }

-        sb.AppendLine();  // ignore the #elsif line

-

-      } else if (t == "#else") {

-        ReadState rs;

-        if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) {

-          sb.AppendLine("#MalformedInput: misplaced #else");  // malformed input

-          break;

-        }

-        rs.hasSeenElse = true;

-        if (ignoreCutoff == -1) {

-          // we had included the previous branch

-          assert !rs.mayStillIncludeAnotherAlternative;

-          ignoreCutoff = readState.Count-1;  // start ignoring

-        } else if (rs.mayStillIncludeAnotherAlternative) {

-          // include this branch

-          ignoreCutoff = -1;

-          rs.mayStillIncludeAnotherAlternative = false;

-        }

-        readState[readState.Count-1] = rs;

-        sb.AppendLine();  // ignore the #else line

-

-      } else if (t == "#endif") {

-        if (readState.Count == 0) {

-          sb.AppendLine("#MalformedInput: misplaced #endif");  // malformed input

-          break;

-        }

-        readState.RemoveAt(readState.Count-1);  // pop

-        if (ignoreCutoff == readState.Count) {

-          // we had ignored the branch that ends here; so, now we start including again

-          ignoreCutoff = -1;

-        }

-        sb.AppendLine();  // ignore the #endif line

-

-      } else if (ignoreCutoff == -1) {

-        sb.AppendLine(s);  // included line

-

-      } else {

-        sb.AppendLine();  // ignore the line

-      }

-    }

-    

-    Fill(sb.ToString());

-  }

-

-  // "arg" is assumed to be trimmed

-  private static bool IfdefConditionSaysToInclude(string! arg, List<string!>! defines) {

-    bool sense = true;

-    while (arg.StartsWith("!")) {

-      sense = !sense;

-      arg = arg.Substring(1).TrimStart();

-    }

-    return defines.Contains(arg) == sense;

-  }

-  

-  public static void Fill(string! text) {

-    buf = text;

-    bufLen = buf.Length;

-    pos = 0;

-  }

-  

-  public static int Read() {

-    if (pos < bufLen) {

-      return buf[pos++];

-    } else {

-      return eof;

-    }

-  }

-

-  public static string/*!*/ ReadToEOL() {

-    int x = buf.IndexOf('\n', pos);

-    if (x == -1) {

-      string s = buf.Substring(pos);

-      pos = buf.Length;

-      return s;

-    } else {

-      string s = buf.Substring(pos, x+1 - pos);  // also include the '\n'

-      pos = x+1;

-      return s;

-    }

-  }

-

-  public static int Pos {

-    get { return pos; }

-    set {

-      if (value < 0) pos = 0; else if (value >= bufLen) pos = bufLen; else pos = value;

-    }

-  }

-}

-

-

-

-public class Scanner {

-  const char EOF = '\0';

-  const char CR  = '\r';

-  const char LF  = '\n';

-  [Microsoft.Contracts.Verify(false)]

--->declarations

-

-  static Token/*!*/ t;          // current token

-  static char ch;               // current input character

-  static int pos;               // column number of current character

-  static int line;              // line number of current character

-  static int lineStart;         // start position of current line

-  static Queue! oldEols;        // EOLs that appeared in a comment;

-  static BitArray/*!*/ ignore;  // set of characters to be ignored by the scanner  

-  static string Filename;

-

-  ///<summary>

-  ///Initializes the scanner. Note: first fill the Buffer.

-  ///</summary>

-  ///<param name="filename">File name used for error reporting</param>

-  public static void Init (string filename) {

-    Filename = filename;

-    pos = -1; line = 1; lineStart = 0;

-    oldEols = new Queue();

-    NextCh();

--->initialization

-  }

-  

-  private static void NextCh() {

-    if (oldEols.Count > 0) {

-      ch = (char) ((!)oldEols.Dequeue());

-    } else {

-      while (true) {

-        ch = (char)Buffer.Read(); pos++;

-        if (ch == Buffer.eof) {

-          ch = EOF;

-        } else if (ch == LF) {

-          line++;

-          lineStart = pos + 1;

-

-        } else if (ch == '#' && pos == lineStart) {

-          int prLine = line;

-          int prColumn = pos - lineStart;  // which is 0

-

-          string hashLine = Buffer.ReadToEOL();  pos += hashLine.Length;

-          line++;

-          lineStart = pos + 1;

-

-          hashLine = hashLine.TrimEnd(null);

-          if (hashLine.StartsWith("line ") || hashLine == "line") {

-            // parse #line pragma:  #line num [filename]

-            string h = hashLine.Substring(4).TrimStart(null);

-            int x = h.IndexOf(' ');

-            if (x == -1) {

-              x = h.Length;  // this will be convenient below when we look for a filename

-            }

-            try {

-              int li = int.Parse(h.Substring(0, x));

-

-              h = h.Substring(x).Trim();

-

-              // act on #line

-              line = li;

-              if (h.Length != 0) {

-                // a filename was specified

-                Filename = h;

-              }

-              continue;  // successfully parsed and acted on the #line pragma

-

-            } catch (FormatException) {

-              // just fall down through to produce an error message

-            }

-            Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);

-            continue;

-          }

-

-          Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);

-          continue;

-        }

-        return;

-      }

-    }

-  }

-  

--->comment

-  

-  static void CheckLiteral() {

-    switch (t.val) {

--->literals

-    }

-  }

-

-  public static Token/*!*/ Scan() {

-    while (ignore[ch]) { NextCh(); }

--->scan1

-    t = new Token();

-    t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename;

-    int state = (/*^ (!) ^*/ start)[ch];

-    StringBuilder buf = new StringBuilder(16);

-    buf.Append(ch); NextCh();

-    

-    switch (state) {

-      case 0: {t.kind = noSym; goto done;} // NextCh already done

--->scan2

-    }

-    done:

-    t.val = buf.ToString();

-    return t;

-  }

-

-} // end Scanner

-

-

-public delegate void ErrorProc(int n, string filename, int line, int col);

-

-public class Errors {

-  public static int count = 0;  // number of errors detected

-  public static ErrorProc/*!*/ SynErr;  // syntactic errors

-  

-  public static void SemErr(string filename, int line, int col, string! msg) {  // semantic errors

-    ConsoleColor color = Console.ForegroundColor;

-    Console.ForegroundColor = ConsoleColor.Red;

-    Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg);

-    Console.ForegroundColor = color;

-    count++;

-  }

-  

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

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

-  }

-  

-  public static void Exception (string s) {

-    ConsoleColor color = Console.ForegroundColor;

-    Console.ForegroundColor = ConsoleColor.Red;

-    Console.WriteLine(s);

-    Console.ForegroundColor = color;

-    System.Environment.Exit(0);

-  }

-

-} // Errors

-

-} // end namespace

-$$$