diff options
Diffstat (limited to 'Source/Core/Parser.cs')
-rw-r--r-- | Source/Core/Parser.cs | 887 |
1 files changed, 454 insertions, 433 deletions
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 793bb96e..c91de177 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -23,8 +23,9 @@ public class Parser { public const int _digits = 3; public const int _string = 4; public const int _decimal = 5; - public const int _float = 6; - public const int maxT = 96; + public const int _dec_float = 6; + public const int _float = 7; + public const int maxT = 97; const bool T = true; const bool x = false; @@ -132,7 +133,8 @@ private class BvBounds : Expr { Contract.Assert(false);throw new cce.UnreachableException(); } public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); } - public override int ComputeHashCode() { + public override int ComputeHashCode() + { return base.GetHashCode(); } } @@ -219,7 +221,7 @@ private class BvBounds : Expr { while (StartOf(1)) { switch (la.kind) { - case 21: { + case 22: { Consts(out vs); foreach(Bpl.Variable/*!*/ v in vs){ Contract.Assert(v != null); @@ -228,7 +230,7 @@ private class BvBounds : Expr { break; } - case 25: { + case 26: { Function(out ds); foreach(Bpl.Declaration/*!*/ d in ds){ Contract.Assert(d != null); @@ -237,12 +239,12 @@ private class BvBounds : Expr { break; } - case 29: { + case 30: { Axiom(out ax); Pgm.AddTopLevelDeclaration(ax); break; } - case 30: { + case 31: { UserDefinedTypes(out ts); foreach(Declaration/*!*/ td in ts){ Contract.Assert(td != null); @@ -251,7 +253,7 @@ private class BvBounds : Expr { break; } - case 7: { + case 8: { GlobalVars(out vs); foreach(Bpl.Variable/*!*/ v in vs){ Contract.Assert(v != null); @@ -260,7 +262,7 @@ private class BvBounds : Expr { break; } - case 32: { + case 33: { Procedure(out pr, out im); Pgm.AddTopLevelDeclaration(pr); if (im != null) { @@ -269,7 +271,7 @@ private class BvBounds : Expr { break; } - case 33: { + case 34: { Implementation(out nnim); Pgm.AddTopLevelDeclaration(nnim); break; @@ -285,17 +287,17 @@ private class BvBounds : Expr { bool u = false; QKeyValue kv = null; bool ChildrenComplete = false; List<ConstantParent/*!*/> Parents = null; - Expect(21); + Expect(22); y = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } - if (la.kind == 22) { + if (la.kind == 23) { Get(); u = true; } IdsType(out xs); - if (la.kind == 23) { + if (la.kind == 24) { OrderSpec(out ChildrenComplete, out Parents); } bool makeClone = false; @@ -319,7 +321,7 @@ private class BvBounds : Expr { ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv)); } - Expect(8); + Expect(9); } void Function(out List<Declaration>/*!*/ ds) { @@ -336,44 +338,44 @@ private class BvBounds : Expr { Expr definition = null; Expr/*!*/ tmp; - Expect(25); - while (la.kind == 27) { + Expect(26); + while (la.kind == 28) { Attribute(ref kv); } Ident(out z); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out typeParamTok, out typeParams); } - Expect(9); + Expect(10); if (StartOf(2)) { VarOrType(out tyd, out argKv); arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); - while (la.kind == 12) { + while (la.kind == 13) { Get(); VarOrType(out tyd, out argKv); arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); } } - Expect(10); + Expect(11); argKv = null; - if (la.kind == 26) { + if (la.kind == 27) { Get(); - Expect(9); - VarOrType(out retTyd, out argKv); Expect(10); - } else if (la.kind == 11) { + VarOrType(out retTyd, out argKv); + Expect(11); + } else if (la.kind == 12) { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); - } else SynErr(97); - if (la.kind == 27) { + } else SynErr(98); + if (la.kind == 28) { Get(); Expression(out tmp); definition = tmp; - Expect(28); - } else if (la.kind == 8) { + Expect(29); + } else if (la.kind == 9) { Get(); - } else SynErr(98); + } else SynErr(99); if (retTyd == null) { // construct a dummy type for the case of syntax error retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int)); @@ -428,30 +430,30 @@ private class BvBounds : Expr { void Axiom(out Axiom/*!*/ m) { Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; - Expect(29); - while (la.kind == 27) { + Expect(30); + while (la.kind == 28) { Attribute(ref kv); } IToken/*!*/ x = t; Proposition(out e); - Expect(8); + Expect(9); m = new Axiom(x,e, null, kv); } void UserDefinedTypes(out List<Declaration/*!*/>/*!*/ ts) { Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> (); - Expect(30); - while (la.kind == 27) { + Expect(31); + while (la.kind == 28) { Attribute(ref kv); } UserDefinedType(out decl, kv); ts.Add(decl); - while (la.kind == 12) { + while (la.kind == 13) { Get(); UserDefinedType(out decl, kv); ts.Add(decl); } - Expect(8); + Expect(9); } void GlobalVars(out List<Variable>/*!*/ ds) { @@ -460,12 +462,12 @@ private class BvBounds : Expr { ds = new List<Variable>(); var dsx = ds; - Expect(7); - while (la.kind == 27) { + Expect(8); + while (la.kind == 28) { Attribute(ref kv); } IdsTypeWheres(true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } ); - Expect(8); + Expect(9); } void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) { @@ -481,9 +483,9 @@ private class BvBounds : Expr { QKeyValue kv = null; impl = null; - Expect(32); + Expect(33); ProcSignature(true, out x, out typeParams, out ins, out outs, out kv); - if (la.kind == 8) { + if (la.kind == 9) { Get(); while (StartOf(3)) { Spec(pre, mods, post); @@ -496,7 +498,7 @@ private class BvBounds : Expr { impl = new Implementation(x, x.val, typeParams, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(99); + } else SynErr(100); proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); } @@ -508,7 +510,7 @@ private class BvBounds : Expr { StmtList/*!*/ stmtList; QKeyValue kv; - Expect(33); + Expect(34); 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, this.errors); @@ -522,7 +524,7 @@ private class BvBounds : Expr { void IdsTypeWheres(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) { IdsTypeWhere(allowWhereClauses, context, action); - while (la.kind == 12) { + while (la.kind == 13) { Get(); IdsTypeWhere(allowWhereClauses, context, action); } @@ -532,12 +534,12 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out ds) != null); QKeyValue kv = null; - Expect(7); - while (la.kind == 27) { + Expect(8); + while (la.kind == 28) { Attribute(ref kv); } IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } ); - Expect(8); + Expect(9); } void ProcFormals(bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds) { @@ -546,16 +548,16 @@ private class BvBounds : Expr { var dsx = ds; var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals"; - Expect(9); - if (la.kind == 1 || la.kind == 27) { + Expect(10); + if (la.kind == 1 || la.kind == 28) { AttrsIdsTypeWheres(allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }); } - Expect(10); + Expect(11); } void AttrsIdsTypeWheres(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) { AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action); - while (la.kind == 12) { + while (la.kind == 13) { Get(); AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action); } @@ -574,7 +576,7 @@ private class BvBounds : Expr { void IdsType(out List<TypedIdent>/*!*/ tyds) { Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; Idents(out ids); - Expect(11); + Expect(12); Type(out ty); tyds = new List<TypedIdent>(); foreach(Token/*!*/ id in ids){ @@ -588,7 +590,7 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); Ident(out id); xs.Add(id); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Ident(out id); xs.Add(id); @@ -606,14 +608,14 @@ private class BvBounds : Expr { TypeArgs(args); } ty = new UnresolvedTypeIdentifier (tok, tok.val, args); - } else if (la.kind == 17 || la.kind == 19) { + } else if (la.kind == 18 || la.kind == 20) { MapType(out ty); - } else SynErr(100); + } else SynErr(101); } void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) { QKeyValue kv = null; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); if (!allowAttributes) { kv = null; @@ -627,9 +629,9 @@ private class BvBounds : Expr { void IdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) { List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne; Idents(out ids); - Expect(11); + Expect(12); Type(out ty); - if (la.kind == 13) { + if (la.kind == 14) { Get(); Expression(out nne); if (!allowWhereClauses) { @@ -649,7 +651,7 @@ private class BvBounds : Expr { void Expression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; ImpliesExpression(false, out e0); - while (la.kind == 55 || la.kind == 56) { + while (la.kind == 56 || la.kind == 57) { EquivOp(); x = t; ImpliesExpression(false, out e1); @@ -659,20 +661,20 @@ private class BvBounds : Expr { void TypeAtom(out Bpl.Type/*!*/ ty) { Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; - if (la.kind == 14) { + if (la.kind == 15) { Get(); ty = new BasicType(t, SimpleType.Int); - } else if (la.kind == 15) { + } else if (la.kind == 16) { Get(); ty = new BasicType(t, SimpleType.Real); - } else if (la.kind == 16) { + } else if (la.kind == 17) { Get(); ty = new BasicType(t, SimpleType.Bool); - } else if (la.kind == 9) { + } else if (la.kind == 10) { Get(); Type(out ty); - Expect(10); - } else SynErr(101); + Expect(11); + } else SynErr(102); } void Ident(out IToken/*!*/ x) { @@ -699,10 +701,10 @@ private class BvBounds : Expr { if (StartOf(6)) { TypeArgs(ts); } - } else if (la.kind == 17 || la.kind == 19) { + } else if (la.kind == 18 || la.kind == 20) { MapType(out ty); ts.Add(ty); - } else SynErr(102); + } else SynErr(103); } void MapType(out Bpl.Type/*!*/ ty) { @@ -712,16 +714,16 @@ private class BvBounds : Expr { Bpl.Type/*!*/ result; List<TypeVariable>/*!*/ typeParameters = new List<TypeVariable>(); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out nnTok, out typeParameters); tok = nnTok; } - Expect(17); + Expect(18); if (tok == null) tok = t; if (StartOf(6)) { Types(arguments); } - Expect(18); + Expect(19); Type(out result); ty = new MapType(tok, typeParameters, arguments, result); @@ -729,10 +731,10 @@ private class BvBounds : Expr { void TypeParams(out IToken/*!*/ tok, out List<TypeVariable>/*!*/ typeParams) { Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List<IToken>/*!*/ typeParamToks; - Expect(19); + Expect(20); tok = t; Idents(out typeParamToks); - Expect(20); + Expect(21); typeParams = new List<TypeVariable> (); foreach(Token/*!*/ id in typeParamToks){ Contract.Assert(id != null); @@ -744,7 +746,7 @@ private class BvBounds : Expr { Contract.Requires(ts != null); Bpl.Type/*!*/ ty; Type(out ty); ts.Add(ty); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Type(out ty); ts.Add(ty); @@ -756,21 +758,21 @@ private class BvBounds : Expr { Parents = null; bool u; IToken/*!*/ parent; - Expect(23); + Expect(24); Parents = new List<ConstantParent/*!*/> (); u = false; - if (la.kind == 1 || la.kind == 22) { - if (la.kind == 22) { + if (la.kind == 1 || la.kind == 23) { + if (la.kind == 23) { Get(); u = true; } Ident(out parent); Parents.Add(new ConstantParent ( new IdentifierExpr(parent, parent.val), u)); - while (la.kind == 12) { + while (la.kind == 13) { Get(); u = false; - if (la.kind == 22) { + if (la.kind == 23) { Get(); u = true; } @@ -779,7 +781,7 @@ private class BvBounds : Expr { new IdentifierExpr(parent, parent.val), u)); } } - if (la.kind == 24) { + if (la.kind == 25) { Get(); ChildrenComplete = true; } @@ -792,12 +794,12 @@ private class BvBounds : Expr { IToken/*!*/ tok; kv = null; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Type(out ty); tok = ty.tok; - if (la.kind == 11) { + if (la.kind == 12) { Get(); var uti = ty as UnresolvedTypeIdentifier; if (uti != null && uti.Arguments.Count == 0) { @@ -823,7 +825,7 @@ private class BvBounds : Expr { if (la.kind == 1) { WhiteSpaceIdents(out paramTokens); } - if (la.kind == 31) { + if (la.kind == 32) { Get(); Type(out body); synonym = true; @@ -855,15 +857,15 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null); IToken/*!*/ typeParamTok; typeParams = new List<TypeVariable>(); outs = new List<Variable>(); kv = null; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Ident(out name); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out typeParamTok, out typeParams); } ProcFormals(true, allowWhereClausesOnFormals, out ins); - if (la.kind == 26) { + if (la.kind == 27) { Get(); ProcFormals(false, allowWhereClausesOnFormals, out outs); } @@ -871,7 +873,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { void Spec(List<Requires>/*!*/ pre, List<IdentifierExpr>/*!*/ mods, List<Ensures>/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms; - if (la.kind == 34) { + if (la.kind == 35) { Get(); if (la.kind == 1) { Idents(out ms); @@ -881,19 +883,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } } - Expect(8); - } else if (la.kind == 35) { + Expect(9); + } else if (la.kind == 36) { Get(); SpecPrePost(true, pre, post); - } else if (la.kind == 36 || la.kind == 37) { + } else if (la.kind == 37 || la.kind == 38) { SpecPrePost(false, pre, post); - } else SynErr(103); + } else SynErr(104); } void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List<Variable>(); - Expect(27); - while (la.kind == 7) { + Expect(28); + while (la.kind == 8) { LocalVars(locals); } StmtList(out stmtList); @@ -901,25 +903,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; - if (la.kind == 36) { + if (la.kind == 37) { Get(); tok = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); - Expect(8); + Expect(9); pre.Add(new Requires(tok, free, e, null, kv)); - } else if (la.kind == 37) { + } else if (la.kind == 38) { Get(); tok = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); - Expect(8); + Expect(9); post.Add(new Ensures(tok, free, e, null, kv)); - } else SynErr(104); + } else SynErr(105); } void StmtList(out StmtList/*!*/ stmtList) { @@ -956,7 +958,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { cs = new List<Cmd>(); } - } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) { + } else if (la.kind == 41 || la.kind == 43 || la.kind == 46) { StructuredCmd(out ecn); ec = ecn; if (startToken == null) { startToken = ec.tok; cs = new List<Cmd>(); } @@ -976,7 +978,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } } - Expect(28); + Expect(29); IToken/*!*/ endCurly = t; if (startToken == null && bigblocks.Count == 0) { startToken = t; cs = new List<Cmd>(); @@ -1004,33 +1006,33 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { LabelOrAssign(out c, out label); break; } - case 46: { + case 47: { Get(); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); c = new AssertCmd(x, e, kv); - Expect(8); + Expect(9); break; } - case 47: { + case 48: { Get(); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); c = new AssumeCmd(x, e, kv); - Expect(8); + Expect(9); break; } - case 48: { + case 49: { Get(); x = t; Idents(out xs); - Expect(8); + Expect(9); ids = new List<IdentifierExpr>(); foreach(IToken/*!*/ y in xs){ Contract.Assert(y != null); @@ -1040,25 +1042,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { break; } - case 35: case 51: case 52: { + case 36: case 52: case 53: { CallCmd(out cn); - Expect(8); + Expect(9); c = cn; break; } - case 53: { + case 54: { ParCallCmd(out cn); c = cn; break; } - case 49: { + case 50: { Get(); x = t; - Expect(8); + Expect(9); c = new YieldCmd(x); break; } - default: SynErr(105); break; + default: SynErr(106); break; } } @@ -1066,16 +1068,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec)); IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd; - if (la.kind == 40) { + if (la.kind == 41) { IfCmd(out ifcmd); ec = ifcmd; - } else if (la.kind == 42) { + } else if (la.kind == 43) { WhileCmd(out wcmd); ec = wcmd; - } else if (la.kind == 45) { + } else if (la.kind == 46) { BreakCmd(out bcmd); ec = bcmd; - } else SynErr(106); + } else SynErr(107); } void TransferCmd(out TransferCmd/*!*/ tc) { @@ -1083,7 +1085,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Token y; List<IToken>/*!*/ xs; List<String> ss = new List<String>(); - if (la.kind == 38) { + if (la.kind == 39) { Get(); y = t; Idents(out xs); @@ -1092,11 +1094,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { ss.Add(s.val); } tc = new GotoCmd(y, ss); - } else if (la.kind == 39) { + } else if (la.kind == 40) { Get(); tc = new ReturnCmd(t); - } else SynErr(107); - Expect(8); + } else SynErr(108); + Expect(9); } void IfCmd(out IfCmd/*!*/ ifcmd) { @@ -1106,21 +1108,21 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { IfCmd/*!*/ elseIf; IfCmd elseIfOption = null; StmtList/*!*/ els; StmtList elseOption = null; - Expect(40); + Expect(41); x = t; Guard(out guard); - Expect(27); + Expect(28); StmtList(out thn); - if (la.kind == 41) { + if (la.kind == 42) { Get(); - if (la.kind == 40) { + if (la.kind == 41) { IfCmd(out elseIf); elseIfOption = elseIf; - } else if (la.kind == 27) { + } else if (la.kind == 28) { Get(); StmtList(out els); elseOption = els; - } else SynErr(108); + } else SynErr(109); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); } @@ -1132,18 +1134,18 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { StmtList/*!*/ body; QKeyValue kv = null; - Expect(42); + Expect(43); x = t; Guard(out guard); Contract.Assume(guard == null || cce.Owner.None(guard)); - while (la.kind == 35 || la.kind == 43) { + while (la.kind == 36 || la.kind == 44) { isFree = false; z = la/*lookahead token*/; - if (la.kind == 35) { + if (la.kind == 36) { Get(); isFree = true; } - Expect(43); - while (la.kind == 27) { + Expect(44); + while (la.kind == 28) { Attribute(ref kv); } Expression(out e); @@ -1154,9 +1156,9 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } kv = null; - Expect(8); + Expect(9); } - Expect(27); + Expect(28); StmtList(out body); wcmd = new WhileCmd(x, guard, invariants, body); } @@ -1165,27 +1167,27 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y; string breakLabel = null; - Expect(45); + Expect(46); x = t; if (la.kind == 1) { Ident(out y); breakLabel = y.val; } - Expect(8); + Expect(9); bcmd = new BreakCmd(x, breakLabel); } void Guard(out Expr e) { Expr/*!*/ ee; e = null; - Expect(9); - if (la.kind == 44) { + Expect(10); + if (la.kind == 45) { Get(); e = null; } else if (StartOf(9)) { Expression(out ee); e = ee; - } else SynErr(109); - Expect(10); + } else SynErr(110); + Expect(11); } void LabelOrAssign(out Cmd c, out IToken label) { @@ -1198,40 +1200,40 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Ident(out id); x = t; - if (la.kind == 11) { + if (la.kind == 12) { Get(); c = null; label = x; - } else if (la.kind == 12 || la.kind == 17 || la.kind == 50) { + } else if (la.kind == 13 || la.kind == 18 || la.kind == 51) { lhss = new List<AssignLhs/*!*/>(); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 17) { + while (la.kind == 18) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); } lhss.Add(lhs); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Ident(out id); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 17) { + while (la.kind == 18) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); } lhss.Add(lhs); } - Expect(50); + Expect(51); x = t; /* use location of := */ Expression(out e0); rhss = new List<Expr/*!*/> (); rhss.Add(e0); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e0); rhss.Add(e0); } - Expect(8); + Expect(9); c = new AssignCmd(x, lhss, rhss); - } else SynErr(110); + } else SynErr(111); } void CallCmd(out Cmd c) { @@ -1242,17 +1244,17 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { QKeyValue kv = null; c = null; - if (la.kind == 51) { + if (la.kind == 52) { Get(); isAsync = true; } - if (la.kind == 35) { + if (la.kind == 36) { Get(); isFree = true; } - Expect(52); + Expect(53); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } CallParams(isAsync, isFree, kv, x, out c); @@ -1266,19 +1268,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Cmd c = null; List<CallCmd> callCmds = new List<CallCmd>(); - Expect(53); + Expect(54); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } CallParams(false, false, kv, x, out c); callCmds.Add((CallCmd)c); - while (la.kind == 54) { + while (la.kind == 55) { Get(); CallParams(false, false, kv, x, out c); callCmds.Add((CallCmd)c); } - Expect(8); + Expect(9); d = new ParCallCmd(x, callCmds, kv); } @@ -1286,18 +1288,18 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> (); Expr/*!*/ e; - Expect(17); + Expect(18); x = t; if (StartOf(9)) { Expression(out e); indexes.Add(e); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e); indexes.Add(e); } } - Expect(18); + Expect(19); } void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, out Cmd c) { @@ -1309,53 +1311,53 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { c = null; Ident(out first); - if (la.kind == 9) { + if (la.kind == 10) { Get(); if (StartOf(9)) { Expression(out en); es.Add(en); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out en); es.Add(en); } } - Expect(10); + Expect(11); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else if (la.kind == 12 || la.kind == 50) { + } else if (la.kind == 13 || la.kind == 51) { ids.Add(new IdentifierExpr(first, first.val)); - if (la.kind == 12) { + if (la.kind == 13) { Get(); Ident(out p); ids.Add(new IdentifierExpr(p, p.val)); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Ident(out p); ids.Add(new IdentifierExpr(p, p.val)); } } - Expect(50); + Expect(51); Ident(out first); - Expect(9); + Expect(10); if (StartOf(9)) { Expression(out en); es.Add(en); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out en); es.Add(en); } } - Expect(10); + Expect(11); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else SynErr(111); + } else SynErr(112); } void Expressions(out List<Expr>/*!*/ es) { Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>(); Expression(out e); es.Add(e); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e); es.Add(e); @@ -1366,7 +1368,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; LogicalExpression(out e0); if (StartOf(10)) { - if (la.kind == 57 || la.kind == 58) { + if (la.kind == 58 || la.kind == 59) { ImpliesOp(); x = t; ImpliesExpression(true, out e1); @@ -1378,7 +1380,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { x = t; LogicalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); - while (la.kind == 59 || la.kind == 60) { + while (la.kind == 60 || la.kind == 61) { ExpliesOp(); x = t; LogicalExpression(out e1); @@ -1389,23 +1391,23 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void EquivOp() { - if (la.kind == 55) { + if (la.kind == 56) { Get(); - } else if (la.kind == 56) { + } else if (la.kind == 57) { Get(); - } else SynErr(112); + } else SynErr(113); } void LogicalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; RelationalExpression(out e0); if (StartOf(11)) { - if (la.kind == 61 || la.kind == 62) { + if (la.kind == 62 || la.kind == 63) { AndOp(); x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); - while (la.kind == 61 || la.kind == 62) { + while (la.kind == 62 || la.kind == 63) { AndOp(); x = t; RelationalExpression(out e1); @@ -1416,7 +1418,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); - while (la.kind == 63 || la.kind == 64) { + while (la.kind == 64 || la.kind == 65) { OrOp(); x = t; RelationalExpression(out e1); @@ -1427,19 +1429,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void ImpliesOp() { - if (la.kind == 57) { + if (la.kind == 58) { Get(); - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); - } else SynErr(113); + } else SynErr(114); } void ExpliesOp() { - if (la.kind == 59) { + if (la.kind == 60) { Get(); - } else if (la.kind == 60) { + } else if (la.kind == 61) { Get(); - } else SynErr(114); + } else SynErr(115); } void RelationalExpression(out Expr/*!*/ e0) { @@ -1453,25 +1455,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void AndOp() { - if (la.kind == 61) { + if (la.kind == 62) { Get(); - } else if (la.kind == 62) { + } else if (la.kind == 63) { Get(); - } else SynErr(115); + } else SynErr(116); } void OrOp() { - if (la.kind == 63) { + if (la.kind == 64) { Get(); - } else if (la.kind == 64) { + } else if (la.kind == 65) { Get(); - } else SynErr(116); + } else SynErr(117); } void BvTerm(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; Term(out e0); - while (la.kind == 73) { + while (la.kind == 74) { Get(); x = t; Term(out e1); @@ -1482,64 +1484,64 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; switch (la.kind) { - case 65: { + case 66: { Get(); x = t; op=BinaryOperator.Opcode.Eq; break; } - case 19: { + case 20: { Get(); x = t; op=BinaryOperator.Opcode.Lt; break; } - case 20: { + case 21: { Get(); x = t; op=BinaryOperator.Opcode.Gt; break; } - case 66: { + case 67: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 67: { + case 68: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - case 68: { + case 69: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 69: { + case 70: { Get(); x = t; op=BinaryOperator.Opcode.Subtype; break; } - case 70: { + case 71: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 71: { + case 72: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 72: { + case 73: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - default: SynErr(117); break; + default: SynErr(118); break; } } void Term(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; Factor(out e0); - while (la.kind == 74 || la.kind == 75) { + while (la.kind == 75 || la.kind == 76) { AddOp(out x, out op); Factor(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -1558,19 +1560,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 74) { + if (la.kind == 75) { Get(); x = t; op=BinaryOperator.Opcode.Add; - } else if (la.kind == 75) { + } else if (la.kind == 76) { Get(); x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(118); + } else SynErr(119); } void Power(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; UnaryExpression(out e0); - if (la.kind == 79) { + if (la.kind == 80) { Get(); x = t; Power(out e1); @@ -1580,46 +1582,46 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 44) { + if (la.kind == 45) { Get(); x = t; op=BinaryOperator.Opcode.Mul; - } else if (la.kind == 76) { + } else if (la.kind == 77) { Get(); x = t; op=BinaryOperator.Opcode.Div; - } else if (la.kind == 77) { + } else if (la.kind == 78) { Get(); x = t; op=BinaryOperator.Opcode.Mod; - } else if (la.kind == 78) { + } else if (la.kind == 79) { Get(); x = t; op=BinaryOperator.Opcode.RealDiv; - } else SynErr(119); + } else SynErr(120); } void UnaryExpression(out Expr/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; - if (la.kind == 75) { + if (la.kind == 76) { Get(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); - } else if (la.kind == 80 || la.kind == 81) { + } else if (la.kind == 81 || la.kind == 82) { NegOp(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); } else if (StartOf(14)) { CoercionExpression(out e); - } else SynErr(120); + } else SynErr(121); } void NegOp() { - if (la.kind == 80) { + if (la.kind == 81) { Get(); - } else if (la.kind == 81) { + } else if (la.kind == 82) { Get(); - } else SynErr(121); + } else SynErr(122); } void CoercionExpression(out Expr/*!*/ e) { @@ -1628,7 +1630,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { BigNum bn; ArrayExpression(out e); - while (la.kind == 11) { + while (la.kind == 12) { Get(); x = t; if (StartOf(6)) { @@ -1643,7 +1645,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(122); + } else SynErr(123); } } @@ -1654,7 +1656,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { List<Expr>/*!*/ allArgs = dummyExprSeq; AtomExpression(out e); - while (la.kind == 17) { + while (la.kind == 18) { Get(); x = t; allArgs = new List<Expr> (); allArgs.Add(e); @@ -1667,7 +1669,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { else allArgs.Add(index0); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -1675,7 +1677,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { allArgs.Add(e1); } - if (la.kind == 50) { + if (la.kind == 51) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -1689,7 +1691,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { allArgs.Add(e1); store = true; } } - Expect(18); + Expect(19); if (store) e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs); else if (bvExtract) @@ -1714,7 +1716,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void AtomExpression(out Expr/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat bf; List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig; List<TypeVariable>/*!*/ typeParams; IdentifierExpr/*!*/ id; @@ -1724,12 +1726,12 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { List<Block/*!*/>/*!*/ blocks; switch (la.kind) { - case 82: { + case 83: { Get(); e = new LiteralExpr(t, false); break; } - case 83: { + case 84: { Get(); e = new LiteralExpr(t, true); break; @@ -1744,6 +1746,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new LiteralExpr(t, bd); break; } + case 7: { + Float(out bf); + e = new LiteralExpr(t, bf); + break; + } case 2: { BvLit(out bn, out n); e = new LiteralExpr(t, bn, n); @@ -1752,65 +1759,65 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { case 1: { Ident(out x); id = new IdentifierExpr(x, x.val); e = id; - if (la.kind == 9) { + if (la.kind == 10) { Get(); if (StartOf(9)) { Expressions(out es); e = new NAryExpr(x, new FunctionCall(id), es); - } else if (la.kind == 10) { + } else if (la.kind == 11) { e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); - } else SynErr(123); - Expect(10); + } else SynErr(124); + Expect(11); } break; } - case 84: { + case 85: { Get(); x = t; - Expect(9); - Expression(out e); Expect(10); + Expression(out e); + Expect(11); e = new OldExpr(x, e); break; } - case 14: { + case 15: { Get(); x = t; - Expect(9); - Expression(out e); Expect(10); + Expression(out e); + Expect(11); e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr>{ e }); break; } - case 15: { + case 16: { Get(); x = t; - Expect(9); - Expression(out e); Expect(10); + Expression(out e); + Expect(11); e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e }); break; } - case 9: { + case 10: { Get(); if (StartOf(9)) { Expression(out e); if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + "are not allowed"); - } else if (la.kind == 88 || la.kind == 89) { + } else if (la.kind == 89 || la.kind == 90) { Forall(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ForallExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 90 || la.kind == 91) { + } else if (la.kind == 91 || la.kind == 92) { Exists(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ExistsExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 92 || la.kind == 93) { + } else if (la.kind == 93 || la.kind == 94) { Lambda(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); @@ -1818,20 +1825,20 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { SemErr("triggers not allowed in lambda expressions"); if (typeParams.Count + ds.Count > 0) e = new LambdaExpr(x, typeParams, ds, kv, e); - } else SynErr(124); - Expect(10); + } else SynErr(125); + Expect(11); break; } - case 40: { + case 41: { IfThenElseExpression(out e); break; } - case 85: { + case 86: { CodeExpression(out locals, out blocks); e = new CodeExpr(locals, blocks); break; } - default: SynErr(125); break; + default: SynErr(126); break; } } @@ -1843,7 +1850,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 6) { Get(); s = t.val; - } else SynErr(126); + } else SynErr(127); try { n = BigDec.FromString(s); } catch (FormatException) { @@ -1853,6 +1860,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } + void Float(out BigFloat n) { + string s = ""; + Expect(7); + s = t.val; + try { + n = BigFloat.FromString(s); + } catch (FormatException e) { + this.SemErr("incorrectly formatted floating point, " + e.Message); + n = BigFloat.ZERO; + } + + } + void BvLit(out BigNum n, out int m) { Expect(2); int pos = t.val.IndexOf("bv"); @@ -1870,11 +1890,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void Forall() { - if (la.kind == 88) { + if (la.kind == 89) { Get(); - } else if (la.kind == 89) { + } else if (la.kind == 90) { Get(); - } else SynErr(127); + } else SynErr(128); } void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds, @@ -1885,35 +1905,35 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { kv = null; ds = new List<Variable> (); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out tok, out typeParams); - if (la.kind == 1 || la.kind == 27) { + if (la.kind == 1 || la.kind == 28) { BoundVars(q, out ds); } - } else if (la.kind == 1 || la.kind == 27) { + } else if (la.kind == 1 || la.kind == 28) { BoundVars(q, out ds); - } else SynErr(128); + } else SynErr(129); QSep(); - while (la.kind == 27) { + while (la.kind == 28) { AttributeOrTrigger(ref kv, ref trig); } Expression(out body); } void Exists() { - if (la.kind == 90) { + if (la.kind == 91) { Get(); - } else if (la.kind == 91) { + } else if (la.kind == 92) { Get(); - } else SynErr(129); + } else SynErr(130); } void Lambda() { - if (la.kind == 92) { + if (la.kind == 93) { Get(); - } else if (la.kind == 93) { + } else if (la.kind == 94) { Get(); - } else SynErr(130); + } else SynErr(131); } void IfThenElseExpression(out Expr/*!*/ e) { @@ -1921,12 +1941,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { IToken/*!*/ tok; Expr/*!*/ e0, e1, e2; e = dummyExpr; - Expect(40); + Expect(41); tok = t; Expression(out e0); - Expect(87); + Expect(88); Expression(out e1); - Expect(41); + Expect(42); Expression(out e2); e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 }); } @@ -1935,8 +1955,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List<Variable>(); Block/*!*/ b; blocks = new List<Block/*!*/>(); - Expect(85); - while (la.kind == 7) { + Expect(86); + while (la.kind == 8) { LocalVars(locals); } SpecBlock(out b); @@ -1945,7 +1965,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { SpecBlock(out b); blocks.Add(b); } - Expect(86); + Expect(87); } void SpecBlock(out Block/*!*/ b) { @@ -1958,7 +1978,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Expr/*!*/ e; Ident(out x); - Expect(11); + Expect(12); while (StartOf(8)) { LabelOrCmd(out c, out label); if (c != null) { @@ -1970,7 +1990,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } } - if (la.kind == 38) { + if (la.kind == 39) { Get(); y = t; Idents(out xs); @@ -1979,12 +1999,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { ss.Add(s.val); } b = new Block(x,x.val,cs,new GotoCmd(y,ss)); - } else if (la.kind == 39) { + } else if (la.kind == 40) { Get(); Expression(out e); b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); - } else SynErr(131); - Expect(8); + } else SynErr(132); + Expect(9); } void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { @@ -1992,16 +2012,16 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { string key; List<object/*!*/> parameters; object/*!*/ param; - Expect(27); + Expect(28); tok = t; - if (la.kind == 11) { + if (la.kind == 12) { Get(); Expect(1); key = t.val; parameters = new List<object/*!*/>(); if (StartOf(16)) { AttributeParameter(out param); parameters.Add(param); - while (la.kind == 12) { + while (la.kind == 13) { Get(); AttributeParameter(out param); parameters.Add(param); @@ -2029,7 +2049,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } else if (StartOf(9)) { Expression(out e); es = new List<Expr> { e }; - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e); es.Add(e); @@ -2040,8 +2060,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else SynErr(132); - Expect(28); + } else SynErr(133); + Expect(29); } void AttributeParameter(out object/*!*/ o) { @@ -2055,15 +2075,15 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } else if (StartOf(9)) { Expression(out e); o = e; - } else SynErr(133); + } else SynErr(134); } void QSep() { - if (la.kind == 94) { + if (la.kind == 95) { Get(); - } else if (la.kind == 95) { + } else if (la.kind == 96) { Get(); - } else SynErr(134); + } else SynErr(135); } @@ -2079,23 +2099,23 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } 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, x,x}, - {x,x,x,x, x,x,x,T, x,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,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,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,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,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,T,x,x, x,x,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,T,x,x, x,x,x,x, x,T,x,x, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,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,x,x, x,x,x,x, x,x,x,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,T,T, T,T,x,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,T, x,T,T,x, x,T,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, 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,T, x,x,x,x, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,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,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,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T,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,T,x, x,T,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, 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,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,T,T,x, x,T,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, T,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,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, T,T,T,x, x,T,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, 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,T, x,x,x,x, T,T,T,T, T,T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,x,x, x,x,x}, + {x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,T,x, T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,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, 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,x,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,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,T,x,x, x,x,x,x, x,x,T,x, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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, T,x,x,T, T,T,x,T, x,x,T,T, T,T,T,x, 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,x,x, x,x,x,x, x,x,x,x, 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,T, T,T,T,x, 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,T, x,T,T,T, x,x,T,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,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, T,x,x,x, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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, 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,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,x, x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,T, 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,T,T, x,x,T,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,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,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,T,T, x,T,T,T, x,x,T,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,T,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, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,T,T, T,T,T,T, x,x,T,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,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, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x} }; } // end Parser @@ -2126,135 +2146,136 @@ public class Errors { case 3: s = "digits expected"; break; case 4: s = "string expected"; break; case 5: s = "decimal expected"; break; - case 6: s = "float expected"; break; - case 7: s = "\"var\" 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 = "\",\" expected"; break; - case 13: s = "\"where\" expected"; break; - case 14: s = "\"int\" expected"; break; - case 15: s = "\"real\" expected"; break; - case 16: s = "\"bool\" expected"; break; - case 17: s = "\"[\" expected"; break; - case 18: s = "\"]\" expected"; break; - case 19: s = "\"<\" expected"; break; - case 20: s = "\">\" expected"; break; - case 21: s = "\"const\" expected"; break; - case 22: s = "\"unique\" expected"; break; - case 23: s = "\"extends\" expected"; break; - case 24: s = "\"complete\" expected"; break; - case 25: s = "\"function\" expected"; break; - case 26: s = "\"returns\" expected"; break; - case 27: s = "\"{\" expected"; break; - case 28: s = "\"}\" expected"; break; - case 29: s = "\"axiom\" expected"; break; - case 30: s = "\"type\" expected"; break; - case 31: s = "\"=\" expected"; break; - case 32: s = "\"procedure\" expected"; break; - case 33: s = "\"implementation\" expected"; break; - case 34: s = "\"modifies\" expected"; break; - case 35: s = "\"free\" expected"; break; - case 36: s = "\"requires\" expected"; break; - case 37: s = "\"ensures\" 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 = "\"yield\" expected"; break; - case 50: s = "\":=\" expected"; break; - case 51: s = "\"async\" expected"; break; - case 52: s = "\"call\" expected"; break; - case 53: s = "\"par\" expected"; break; - case 54: s = "\"|\" expected"; break; - case 55: s = "\"<==>\" expected"; break; - case 56: s = "\"\\u21d4\" expected"; break; - case 57: s = "\"==>\" expected"; break; - case 58: s = "\"\\u21d2\" expected"; break; - case 59: s = "\"<==\" expected"; break; - case 60: s = "\"\\u21d0\" expected"; break; - case 61: s = "\"&&\" expected"; break; - case 62: s = "\"\\u2227\" expected"; break; - case 63: s = "\"||\" expected"; break; - case 64: s = "\"\\u2228\" expected"; break; - case 65: s = "\"==\" expected"; break; - case 66: s = "\"<=\" expected"; break; - case 67: s = "\">=\" expected"; break; - case 68: s = "\"!=\" expected"; break; - case 69: s = "\"<:\" expected"; break; - case 70: s = "\"\\u2260\" expected"; break; - case 71: s = "\"\\u2264\" expected"; break; - case 72: s = "\"\\u2265\" expected"; break; - case 73: s = "\"++\" expected"; break; - case 74: s = "\"+\" expected"; break; - case 75: s = "\"-\" expected"; break; - case 76: s = "\"div\" expected"; break; - case 77: s = "\"mod\" expected"; break; - case 78: s = "\"/\" expected"; break; - case 79: s = "\"**\" expected"; break; - case 80: s = "\"!\" expected"; break; - case 81: s = "\"\\u00ac\" expected"; break; - case 82: s = "\"false\" expected"; break; - case 83: s = "\"true\" expected"; break; - case 84: s = "\"old\" expected"; break; - case 85: s = "\"|{\" expected"; break; - case 86: s = "\"}|\" expected"; break; - case 87: s = "\"then\" expected"; break; - case 88: s = "\"forall\" expected"; break; - case 89: s = "\"\\u2200\" expected"; break; - case 90: s = "\"exists\" expected"; break; - case 91: s = "\"\\u2203\" expected"; break; - case 92: s = "\"lambda\" expected"; break; - case 93: s = "\"\\u03bb\" expected"; break; - case 94: s = "\"::\" expected"; break; - case 95: s = "\"\\u2022\" expected"; break; - case 96: s = "??? expected"; break; - case 97: s = "invalid Function"; break; + case 6: s = "dec_float expected"; break; + case 7: s = "float expected"; break; + case 8: s = "\"var\" expected"; break; + case 9: s = "\";\" expected"; break; + case 10: s = "\"(\" expected"; break; + case 11: s = "\")\" expected"; break; + case 12: s = "\":\" expected"; break; + case 13: s = "\",\" expected"; break; + case 14: s = "\"where\" expected"; break; + case 15: s = "\"int\" expected"; break; + case 16: s = "\"real\" expected"; break; + case 17: s = "\"bool\" expected"; break; + case 18: s = "\"[\" expected"; break; + case 19: s = "\"]\" expected"; break; + case 20: s = "\"<\" expected"; break; + case 21: s = "\">\" expected"; break; + case 22: s = "\"const\" expected"; break; + case 23: s = "\"unique\" expected"; break; + case 24: s = "\"extends\" expected"; break; + case 25: s = "\"complete\" expected"; break; + case 26: s = "\"function\" expected"; break; + case 27: s = "\"returns\" expected"; break; + case 28: s = "\"{\" expected"; break; + case 29: s = "\"}\" expected"; break; + case 30: s = "\"axiom\" expected"; break; + case 31: s = "\"type\" expected"; break; + case 32: s = "\"=\" expected"; break; + case 33: s = "\"procedure\" expected"; break; + case 34: s = "\"implementation\" expected"; break; + case 35: s = "\"modifies\" expected"; break; + case 36: s = "\"free\" expected"; break; + case 37: s = "\"requires\" expected"; break; + case 38: s = "\"ensures\" expected"; break; + case 39: s = "\"goto\" expected"; break; + case 40: s = "\"return\" expected"; break; + case 41: s = "\"if\" expected"; break; + case 42: s = "\"else\" expected"; break; + case 43: s = "\"while\" expected"; break; + case 44: s = "\"invariant\" expected"; break; + case 45: s = "\"*\" expected"; break; + case 46: s = "\"break\" expected"; break; + case 47: s = "\"assert\" expected"; break; + case 48: s = "\"assume\" expected"; break; + case 49: s = "\"havoc\" expected"; break; + case 50: s = "\"yield\" expected"; break; + case 51: s = "\":=\" expected"; break; + case 52: s = "\"async\" expected"; break; + case 53: s = "\"call\" expected"; break; + case 54: s = "\"par\" expected"; break; + case 55: s = "\"|\" expected"; break; + case 56: s = "\"<==>\" expected"; break; + case 57: s = "\"\\u21d4\" expected"; break; + case 58: s = "\"==>\" expected"; break; + case 59: s = "\"\\u21d2\" expected"; break; + case 60: s = "\"<==\" expected"; break; + case 61: s = "\"\\u21d0\" expected"; break; + case 62: s = "\"&&\" expected"; break; + case 63: s = "\"\\u2227\" expected"; break; + case 64: s = "\"||\" expected"; break; + case 65: s = "\"\\u2228\" expected"; break; + case 66: s = "\"==\" expected"; break; + case 67: s = "\"<=\" expected"; break; + case 68: s = "\">=\" expected"; break; + case 69: s = "\"!=\" expected"; break; + case 70: s = "\"<:\" expected"; break; + case 71: s = "\"\\u2260\" expected"; break; + case 72: s = "\"\\u2264\" expected"; break; + case 73: s = "\"\\u2265\" expected"; break; + case 74: s = "\"++\" expected"; break; + case 75: s = "\"+\" expected"; break; + case 76: s = "\"-\" expected"; break; + case 77: s = "\"div\" expected"; break; + case 78: s = "\"mod\" expected"; break; + case 79: s = "\"/\" expected"; break; + case 80: s = "\"**\" expected"; break; + case 81: s = "\"!\" expected"; break; + case 82: s = "\"\\u00ac\" expected"; break; + case 83: s = "\"false\" expected"; break; + case 84: s = "\"true\" expected"; break; + case 85: s = "\"old\" expected"; break; + case 86: s = "\"|{\" expected"; break; + case 87: s = "\"}|\" expected"; break; + case 88: s = "\"then\" expected"; break; + case 89: s = "\"forall\" expected"; break; + case 90: s = "\"\\u2200\" expected"; break; + case 91: s = "\"exists\" expected"; break; + case 92: s = "\"\\u2203\" expected"; break; + case 93: s = "\"lambda\" expected"; break; + case 94: s = "\"\\u03bb\" expected"; break; + case 95: s = "\"::\" expected"; break; + case 96: s = "\"\\u2022\" expected"; break; + case 97: s = "??? expected"; break; case 98: s = "invalid Function"; break; - case 99: s = "invalid Procedure"; break; - case 100: s = "invalid Type"; break; - case 101: s = "invalid TypeAtom"; break; - case 102: s = "invalid TypeArgs"; break; - case 103: s = "invalid Spec"; break; - case 104: s = "invalid SpecPrePost"; break; - case 105: s = "invalid LabelOrCmd"; break; - case 106: s = "invalid StructuredCmd"; break; - case 107: s = "invalid TransferCmd"; break; - case 108: s = "invalid IfCmd"; break; - case 109: s = "invalid Guard"; break; - case 110: s = "invalid LabelOrAssign"; break; - case 111: s = "invalid CallParams"; break; - case 112: s = "invalid EquivOp"; break; - case 113: s = "invalid ImpliesOp"; break; - case 114: s = "invalid ExpliesOp"; break; - case 115: s = "invalid AndOp"; break; - case 116: s = "invalid OrOp"; break; - case 117: s = "invalid RelOp"; break; - case 118: s = "invalid AddOp"; break; - case 119: s = "invalid MulOp"; break; - case 120: s = "invalid UnaryExpression"; break; - case 121: s = "invalid NegOp"; break; - case 122: s = "invalid CoercionExpression"; break; - case 123: s = "invalid AtomExpression"; break; + case 99: s = "invalid Function"; break; + case 100: s = "invalid Procedure"; break; + case 101: s = "invalid Type"; break; + case 102: s = "invalid TypeAtom"; break; + case 103: s = "invalid TypeArgs"; break; + case 104: s = "invalid Spec"; break; + case 105: s = "invalid SpecPrePost"; break; + case 106: s = "invalid LabelOrCmd"; break; + case 107: s = "invalid StructuredCmd"; break; + case 108: s = "invalid TransferCmd"; break; + case 109: s = "invalid IfCmd"; break; + case 110: s = "invalid Guard"; break; + case 111: s = "invalid LabelOrAssign"; break; + case 112: s = "invalid CallParams"; break; + case 113: s = "invalid EquivOp"; break; + case 114: s = "invalid ImpliesOp"; break; + case 115: s = "invalid ExpliesOp"; break; + case 116: s = "invalid AndOp"; break; + case 117: s = "invalid OrOp"; break; + case 118: s = "invalid RelOp"; break; + case 119: s = "invalid AddOp"; break; + case 120: s = "invalid MulOp"; break; + case 121: s = "invalid UnaryExpression"; break; + case 122: s = "invalid NegOp"; break; + case 123: s = "invalid CoercionExpression"; break; case 124: s = "invalid AtomExpression"; break; case 125: s = "invalid AtomExpression"; break; - case 126: s = "invalid Dec"; break; - case 127: s = "invalid Forall"; break; - case 128: s = "invalid QuantifierBody"; break; - case 129: s = "invalid Exists"; break; - case 130: s = "invalid Lambda"; break; - case 131: s = "invalid SpecBlock"; break; - case 132: s = "invalid AttributeOrTrigger"; break; - case 133: s = "invalid AttributeParameter"; break; - case 134: s = "invalid QSep"; break; + case 126: s = "invalid AtomExpression"; break; + case 127: s = "invalid Dec"; break; + case 128: s = "invalid Forall"; break; + case 129: s = "invalid QuantifierBody"; break; + case 130: s = "invalid Exists"; break; + case 131: s = "invalid Lambda"; break; + case 132: s = "invalid SpecBlock"; break; + case 133: s = "invalid AttributeOrTrigger"; break; + case 134: s = "invalid AttributeParameter"; break; + case 135: s = "invalid QSep"; break; default: s = "error " + n; break; } |