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 System.Diagnostics.Contracts;
namespace Microsoft.Boogie {
public class Parser {
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;
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 Expr/*!*/ dummyExpr = new LiteralExpr(Token.NoToken, false);
static Cmd/*!*/ dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
static Block/*!*/ dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(),
new ReturnCmd(Token.NoToken));
static Bpl.Type/*!*/ dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
static Bpl.ExprSeq/*!*/ dummyExprSeq = new ExprSeq ();
static TransferCmd/*!*/ dummyTransferCmd = new ReturnCmd(Token.NoToken);
static StructuredCmd/*!*/ dummyStructuredCmd = new BreakCmd(Token.NoToken, null);
///
///Returns the number of parsing errors encountered. If 0, "program" returns as
///the parsed program.
///
public static int Parse (string/*!*/ filename, /*maybe null*/ List() != null); return Bpl.Type.Int; } }
public override void Resolve(ResolutionContext/*!*/ rc) {
Contract.Requires(rc != null);
rc.Error(this, "bitvector bounds in illegal position");
}
public override void Emit(TokenTextWriter/*!*/ stream,
int contextBindingStrength, bool fragileContext) {
Contract.Requires(stream != null);
{Contract.Assert(false);throw new cce.UnreachableException();}
}
public override void ComputeFreeVariables(GSet/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }
public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } }
}
/*--------------------------------------------------------------------------*/
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
}
void SynErr (int n) {
if (errDist >= minErrDist) errors.SynErr(la.filename, la.line, la.col, n);
errDist = 0;
}
public void SemErr (string/*!*/ msg) {
Contract.Requires(msg != null);
if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
Contract.Requires(tok != null);
Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
void Get () {
for (;;) {
t = la;
la = scanner.Scan();
if (la.kind <= maxT) { ++errDist; break; }
la = t;
}
}
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
bool StartOf (int s) {
return set[s, la.kind];
}
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
SynErr(n);
while (!StartOf(follow)) Get();
}
}
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 {
SynErr(n);
while (!(set[syFol, kind] || set[repFol, kind] || set[0, kind])) {
Get();
kind = la.kind;
}
return StartOf(syFol);
}
}
void BoogiePL() {
VariableSeq/*!*/ vs;
DeclarationSeq/*!*/ ds;
Axiom/*!*/ ax;
List/*!*/ ids = new List();
List/*!*/ es = new List();
QKeyValue kv = null;
Expr en; List args;
c = dummyCmd;
bool isFree = false;
if (la.kind == 33) {
Get();
isFree = true;
}
Expect(48);
x = t;
while (la.kind == 25) {
Attribute(ref kv);
}
if (la.kind == 1) {
Ident(out first);
if (la.kind == 8) {
Get();
if (StartOf(8)) {
CallForallArg(out en);
es.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
es.Add(en);
}
}
Expect(9);
c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
} else if (la.kind == 11 || la.kind == 47) {
ids.Add(new IdentifierExpr(first, first.val));
if (la.kind == 11) {
Get();
CallOutIdent(out p);
if (p==null) {
ids.Add(null);
} else {
ids.Add(new IdentifierExpr(p, p.val));
}
while (la.kind == 11) {
Get();
CallOutIdent(out p);
if (p==null) {
ids.Add(null);
} else {
ids.Add(new IdentifierExpr(p, p.val));
}
}
}
Expect(47);
Ident(out first);
Expect(8);
if (StartOf(8)) {
CallForallArg(out en);
es.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
es.Add(en);
}
}
Expect(9);
c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
} else SynErr(103);
} else if (la.kind == 49) {
Get();
Ident(out first);
Expect(8);
args = new List();
if (StartOf(8)) {
CallForallArg(out en);
args.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
args.Add(en);
}
}
Expect(9);
c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree;
} else if (la.kind == 42) {
Get();
ids.Add(null);
if (la.kind == 11) {
Get();
CallOutIdent(out p);
if (p==null) {
ids.Add(null);
} else {
ids.Add(new IdentifierExpr(p, p.val));
}
while (la.kind == 11) {
Get();
CallOutIdent(out p);
if (p==null) {
ids.Add(null);
} else {
ids.Add(new IdentifierExpr(p, p.val));
}
}
}
Expect(47);
Ident(out first);
Expect(8);
if (StartOf(8)) {
CallForallArg(out en);
es.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
es.Add(en);
}
}
Expect(9);
c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
} else SynErr(104);
}
void MapAssignIndex(out IToken/*!*/ x, out List