diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 307f898cf..b5e3e143c 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -1304,6 +1304,15 @@ public Variable(IToken tok, TypedIdent typedIdent, QKeyValue kv) } public abstract bool IsMutable { get; } + + /// + /// Prevents this variable from being havoc'd. Useful in situations where Havoc commands are generated, + /// such as after While commands. + /// + /// One use-case is the definite assignment tracking variables in Dafny, that only go from false to true, + /// And can return an error if they're still false at the wrong point. + /// + public bool Monotonic { get; set; } public override void Emit(TokenTextWriter stream, int level) { diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index fb84e2a35..4c2c8c0fc 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -1,6 +1,7 @@ using System; using System.Diagnostics; using System.Collections.Generic; +using System.ComponentModel; using System.Linq; using System.Diagnostics.Contracts; using Set = Microsoft.Boogie.GSet; @@ -3333,26 +3334,14 @@ public override Absy StdDispatch(StandardVisitor visitor) public class HavocCmd : Cmd { - private List /*!*/ _vars; + public List /*!*/ VarsIncludingMonotonic { get; set; } - public List /*!*/ Vars - { - get - { - Contract.Ensures(Contract.Result>() != null); - return this._vars; - } - set - { - Contract.Requires(value != null); - this._vars = value; - } - } + public IEnumerable /*!*/ Vars => VarsIncludingMonotonic.Where(v => !v.Decl.Monotonic); [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(this._vars != null); + Contract.Invariant(this.VarsIncludingMonotonic != null); } public HavocCmd(IToken /*!*/ tok, List /*!*/ vars) @@ -3360,21 +3349,21 @@ public HavocCmd(IToken /*!*/ tok, List /*!*/ vars) { Contract.Requires(tok != null); Contract.Requires(vars != null); - this._vars = vars; + this.VarsIncludingMonotonic = vars; } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); stream.Write(this, level, "havoc "); - Vars.Emit(stream, true); + VarsIncludingMonotonic.Emit(stream, true); stream.WriteLine(";"); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); - foreach (IdentifierExpr /*!*/ ide in Vars) + foreach (IdentifierExpr /*!*/ ide in VarsIncludingMonotonic) { Contract.Assert(ide != null); ide.Resolve(rc); @@ -3392,7 +3381,7 @@ public override void AddAssignedIdentifiers(List vars) { public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); - foreach (IdentifierExpr ie in Vars) + foreach (IdentifierExpr ie in VarsIncludingMonotonic) { ie.Typecheck(tc); } diff --git a/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs b/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs index 316cd11f2..540a38697 100644 --- a/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs +++ b/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs @@ -134,10 +134,8 @@ public void Propagate(Cmd cmd, HashSet /*!*/ liveSet) index++; } } - else if (cmd is HavocCmd) + else if (cmd is HavocCmd havocCmd) { - HavocCmd /*!*/ - havocCmd = (HavocCmd) cmd; foreach (IdentifierExpr /*!*/ expr in havocCmd.Vars) { Contract.Assert(expr != null); diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index b850527c2..61fa4e0fc 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -265,10 +265,14 @@ LocalVars<.List/*!*/ ds.> = (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); QKeyValue kv = null; + bool monotonic = false; .) + [ "monotonic" (. monotonic = true; .) ] "var" { Attribute } - IdsTypeWheres ";" + IdsTypeWheres ";" . ProcFormals<.bool incoming, bool allowWhereClauses, out List/*!*/ ds.> diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index ff6ecb84f..a7f34904f 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -36,7 +36,7 @@ public class Parser { public const int _decimal = 5; public const int _dec_float = 6; public const int _float = 7; - public const int maxT = 125; + public const int maxT = 126; const bool _T = true; const bool _x = false; @@ -246,7 +246,7 @@ void BoogiePL() { while (StartOf(1)) { switch (la.kind) { - case 23: { + case 24: { Consts(out ds); foreach(Bpl.Declaration/*!*/ v in ds){ Contract.Assert(v != null); @@ -255,7 +255,7 @@ void BoogiePL() { break; } - case 28: case 29: { + case 29: case 30: { Function(out ds); foreach(Bpl.Declaration/*!*/ d in ds){ Contract.Assert(d != null); @@ -264,12 +264,12 @@ void BoogiePL() { break; } - case 31: case 32: { + case 32: case 33: { Axiom(out ax); Pgm.AddTopLevelDeclaration(ax); break; } - case 33: { + case 34: { UserDefinedTypes(out ts); foreach(Declaration/*!*/ td in ts){ Contract.Assert(td != null); @@ -278,7 +278,7 @@ void BoogiePL() { break; } - case 35: { + case 36: { Datatype(out dt); Pgm.AddTopLevelDeclaration(dt); break; @@ -294,7 +294,7 @@ void BoogiePL() { } case 8: { Get(); - if (la.kind == 36) { + if (la.kind == 37) { YieldInvariantDecl(out yi); Pgm.AddTopLevelDeclaration(yi); } else if (StartOf(2)) { @@ -304,12 +304,12 @@ void BoogiePL() { Pgm.AddTopLevelDeclaration(im); } - } else SynErr(126); + } else SynErr(127); break; } - case 37: case 38: case 39: case 43: case 44: case 45: case 46: case 47: { + case 38: case 39: case 40: case 44: case 45: case 46: case 47: case 48: { Pure(ref isPure); - if (la.kind == 47) { + if (la.kind == 48) { Procedure(isPure, out pr, out im); Pgm.AddTopLevelDeclaration(pr); if (im != null) { @@ -328,10 +328,10 @@ void BoogiePL() { } isPure = false; - } else SynErr(127); + } else SynErr(128); break; } - case 52: { + case 53: { Implementation(out nnim); Pgm.AddTopLevelDeclaration(nnim); break; @@ -347,27 +347,27 @@ void Consts(out List/*!*/ ds) { var axioms = new List(); Axiom axiom; bool u = false; QKeyValue kv = null; - Expect(23); + Expect(24); y = t; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } - if (la.kind == 24) { + if (la.kind == 25) { Get(); u = true; } IdsType(out xs); if (la.kind == 10) { Get(); - } else if (la.kind == 25) { + } else if (la.kind == 26) { Get(); - Expect(26); - while (la.kind == 31 || la.kind == 32) { + Expect(27); + while (la.kind == 32 || la.kind == 33) { Axiom(out axiom); axioms.Add(axiom); ds.Add(axiom); } - Expect(27); - } else SynErr(128); + Expect(28); + } else SynErr(129); foreach(TypedIdent/*!*/ x in xs){ Contract.Assert(x != null); var constant = new Constant(y, x, u, kv, axioms); @@ -393,65 +393,65 @@ void Function(out List/*!*/ ds) { Axiom ax; bool revealed = false; - if (la.kind == 28) { + if (la.kind == 29) { Get(); revealed = true; } - Expect(29); - while (la.kind == 26) { + Expect(30); + while (la.kind == 27) { Attribute(ref kv); } Ident(out z); - if (la.kind == 21) { + if (la.kind == 22) { TypeParams(out typeParamTok, out typeParams); } - Expect(11); + Expect(12); if (StartOf(4)) { VarOrType(out tyd, out argKv); arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); - while (la.kind == 14) { + while (la.kind == 15) { Get(); VarOrType(out tyd, out argKv); arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); } } - Expect(12); + Expect(13); argKv = null; - if (la.kind == 30) { + if (la.kind == 31) { Get(); - Expect(11); - VarOrType(out retTyd, out argKv); Expect(12); - } else if (la.kind == 13) { + VarOrType(out retTyd, out argKv); + Expect(13); + } else if (la.kind == 14) { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); - } else SynErr(129); - if (la.kind == 26) { + } else SynErr(130); + if (la.kind == 27) { Get(); Expression(out tmp); definition = tmp; - Expect(27); - if (la.kind == 25) { + Expect(28); + if (la.kind == 26) { Get(); - Expect(26); - while (la.kind == 31 || la.kind == 32) { + Expect(27); + while (la.kind == 32 || la.kind == 33) { Axiom(out ax); axioms.Add(ax); } - Expect(27); + Expect(28); } - } else if (la.kind == 25) { + } else if (la.kind == 26) { Get(); - Expect(26); - while (la.kind == 31 || la.kind == 32) { + Expect(27); + while (la.kind == 32 || la.kind == 33) { Axiom(out ax); axioms.Add(ax); } - Expect(27); + Expect(28); } else if (la.kind == 10) { Get(); - } else SynErr(130); + } else SynErr(131); if (retTyd == null) { // construct a dummy type for the case of syntax error retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int)); @@ -521,12 +521,12 @@ void Axiom(out Axiom/*!*/ m) { Expr/*!*/ e; QKeyValue kv = null; bool canHide = false; - if (la.kind == 31) { + if (la.kind == 32) { Get(); canHide = true; } - Expect(32); - while (la.kind == 26) { + Expect(33); + while (la.kind == 27) { Attribute(ref kv); } IToken/*!*/ x = t; @@ -537,13 +537,13 @@ void Axiom(out Axiom/*!*/ m) { void UserDefinedTypes(out List/*!*/ ts) { Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List (); - Expect(33); - while (la.kind == 26) { + Expect(34); + while (la.kind == 27) { Attribute(ref kv); } UserDefinedType(out decl, kv); ts.Add(decl); - while (la.kind == 14) { + while (la.kind == 15) { Get(); UserDefinedType(out decl, kv); ts.Add(decl); @@ -553,18 +553,18 @@ void UserDefinedTypes(out List/*!*/ ts) { void Datatype(out DatatypeTypeCtorDecl datatypeTypeCtorDecl) { QKeyValue kv = null; IToken/*!*/ typeParamTok, name; List typeParams = new List(); - Expect(35); - while (la.kind == 26) { + Expect(36); + while (la.kind == 27) { Attribute(ref kv); } Ident(out name); - if (la.kind == 21) { + if (la.kind == 22) { TypeParams(out typeParamTok, out typeParams); } datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, typeParams, kv); - Expect(26); - Constructors(datatypeTypeCtorDecl); Expect(27); + Constructors(datatypeTypeCtorDecl); + Expect(28); } void GlobalVars(out List/*!*/ ds) { @@ -574,7 +574,7 @@ void GlobalVars(out List/*!*/ ds) { var dsx = ds; Expect(9); - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } IdsTypeWheres(true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } ); @@ -583,14 +583,14 @@ void GlobalVars(out List/*!*/ ds) { void YieldInvariantDecl(out YieldInvariantDecl yieldInvariant) { List invariants = new List(); QKeyValue kv = null; IToken name = null; List ins; - Expect(36); - while (la.kind == 26) { + Expect(37); + while (la.kind == 27) { Attribute(ref kv); } Ident(out name); ProcFormals(true, true, out ins); Expect(10); - while (la.kind == 36) { + while (la.kind == 37) { Invariant(invariants); } yieldInvariant = new YieldInvariantDecl(name, name.val, ins, invariants, kv); @@ -615,13 +615,13 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl) if (StartOf(5)) { MoverQualifier(ref moverType); } - Expect(47); - while (la.kind == 26) { + Expect(48); + while (la.kind == 27) { Attribute(ref kv); } Ident(out name); ProcFormals(true, true, out ins); - if (la.kind == 30) { + if (la.kind == 31) { Get(); ProcFormals(false, true, out outs); } @@ -638,12 +638,12 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl) impl = new Implementation(name, name.val, new List(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(131); + } else SynErr(132); ypDecl = new YieldProcedureDecl(name, name.val, moverType, ins, outs, pre, mods, post, yieldRequires, yieldEnsures, yieldPreserves, refinedAction, kv); } void Pure(ref bool isPure) { - if (la.kind == 37) { + if (la.kind == 38) { Get(); isPure = true; } @@ -661,7 +661,7 @@ void Procedure(bool isPure, out Procedure/*!*/ proc, out /*maybe null*/ Implemen QKeyValue kv = null; impl = null; - Expect(47); + Expect(48); ProcSignature(true, out x, out typeParams, out ins, out outs, out kv); if (la.kind == 10) { Get(); @@ -676,7 +676,7 @@ void Procedure(bool isPure, out Procedure/*!*/ proc, out /*maybe null*/ Implemen impl = new Implementation(x, x.val, typeParams.ConvertAll(tp => new TypeVariable(tp.tok, tp.Name)), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(132); + } else SynErr(133); proc = new Procedure(x, x.val, typeParams, ins, outs, isPure, pre, mods, post, kv); } @@ -698,20 +698,20 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, datatypeTypeCtorDecl = null; impl = null; - if (la.kind == 38) { + if (la.kind == 39) { Get(); isAsync = true; } if (StartOf(5)) { MoverQualifier(ref moverType); } - Expect(39); - while (la.kind == 26) { + Expect(40); + while (la.kind == 27) { Attribute(ref kv); } Ident(out name); ProcFormals(true, true, out ins); - if (la.kind == 30) { + if (la.kind == 31) { Get(); ProcFormals(false, true, out outs); } @@ -728,7 +728,7 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, impl = new Implementation(name, name.val, new List(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(133); + } else SynErr(134); if (isPure) { if (moverType == MoverType.None) { @@ -767,7 +767,7 @@ void Implementation(out Implementation/*!*/ impl) { StmtList/*!*/ stmtList; QKeyValue kv; - Expect(52); + Expect(53); 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); @@ -781,7 +781,7 @@ void Attribute(ref QKeyValue kv) { void IdsTypeWheres(bool allowWhereClauses, string context, System.Action action ) { IdsTypeWhere(allowWhereClauses, context, action); - while (la.kind == 14) { + while (la.kind == 15) { Get(); IdsTypeWhere(allowWhereClauses, context, action); } @@ -790,12 +790,19 @@ void IdsTypeWheres(bool allowWhereClauses, string context, System.Action/*!*/ ds) { Contract.Ensures(Contract.ValueAtReturn(out ds) != null); QKeyValue kv = null; + bool monotonic = false; + if (la.kind == 11) { + Get(); + monotonic = true; + } Expect(9); - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } - IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } ); + IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv) { +Monotonic = monotonic +}); } ); Expect(10); } @@ -805,16 +812,16 @@ void ProcFormals(bool incoming, bool allowWhereClauses, out List/*!*/ var dsx = ds; var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals"; - Expect(11); + Expect(12); if (StartOf(12)) { AttributesIdsTypeWheres(allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }); } - Expect(12); + Expect(13); } void AttributesIdsTypeWheres(bool allowWhereClauses, string context, System.Action action ) { AttributesIdsTypeWhere(allowWhereClauses, context, action); - while (la.kind == 14) { + while (la.kind == 15) { Get(); AttributesIdsTypeWhere(allowWhereClauses, context, action); } @@ -832,7 +839,7 @@ void BoundVars(out List/*!*/ ds) { void IdsType(out List/*!*/ tyds) { Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List/*!*/ ids; Bpl.Type/*!*/ ty; Idents(out ids); - Expect(13); + Expect(14); Type(out ty); tyds = new List(); foreach(Token/*!*/ id in ids){ @@ -846,7 +853,7 @@ void Idents(out List/*!*/ xs) { Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List(); Ident(out id); xs.Add(id); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Ident(out id); xs.Add(id); @@ -864,14 +871,14 @@ void Type(out Bpl.Type/*!*/ ty) { TypeArgs(args); } ty = new UnresolvedTypeIdentifier (tok, tok.val, args); - } else if (la.kind == 19 || la.kind == 21) { + } else if (la.kind == 20 || la.kind == 22) { MapType(out ty); - } else SynErr(134); + } else SynErr(135); } void AttributesIdsTypeWhere(bool allowWhereClauses, string context, System.Action action ) { QKeyValue kv = null; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } IdsTypeWhere(allowWhereClauses, context, delegate(TypedIdent tyd) { action(tyd, kv); }); @@ -880,9 +887,9 @@ void AttributesIdsTypeWhere(bool allowWhereClauses, string context, System.Actio void IdsTypeWhere(bool allowWhereClauses, string context, System.Action action ) { List/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne; Idents(out ids); - Expect(13); + Expect(14); Type(out ty); - if (la.kind == 15) { + if (la.kind == 16) { Get(); Expression(out nne); if (!allowWhereClauses) { @@ -902,7 +909,7 @@ void IdsTypeWhere(bool allowWhereClauses, string context, System.Action/*!*/ ts) { if (StartOf(15)) { TypeArgs(ts); } - } else if (la.kind == 19 || la.kind == 21) { + } else if (la.kind == 20 || la.kind == 22) { MapType(out ty); ts.Add(ty); - } else SynErr(137); + } else SynErr(138); } void MapType(out Bpl.Type/*!*/ ty) { @@ -1011,16 +1018,16 @@ void MapType(out Bpl.Type/*!*/ ty) { Bpl.Type/*!*/ result; List/*!*/ typeParameters = new List(); - if (la.kind == 21) { + if (la.kind == 22) { TypeParams(out nnTok, out typeParameters); tok = nnTok; } - Expect(19); + Expect(20); if (tok == null) tok = t; if (StartOf(15)) { Types(arguments); } - Expect(20); + Expect(21); Type(out result); ty = new MapType(tok, typeParameters, arguments, result); @@ -1028,10 +1035,10 @@ void MapType(out Bpl.Type/*!*/ ty) { void TypeParams(out IToken/*!*/ tok, out List/*!*/ typeParams) { Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List/*!*/ typeParamToks; - Expect(21); + Expect(22); tok = t; Idents(out typeParamToks); - Expect(22); + Expect(23); typeParams = new List (); foreach(Token/*!*/ id in typeParamToks){ Contract.Assert(id != null); @@ -1043,7 +1050,7 @@ void Types(List/*!*/ ts) { Contract.Requires(ts != null); Bpl.Type/*!*/ ty; Type(out ty); ts.Add(ty); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Type(out ty); ts.Add(ty); @@ -1057,12 +1064,12 @@ void VarOrType(out TypedIdent/*!*/ tyd, out QKeyValue kv) { IToken/*!*/ tok; kv = null; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Type(out ty); tok = ty.tok; - if (la.kind == 13) { + if (la.kind == 14) { Get(); var uti = ty as UnresolvedTypeIdentifier; if (uti != null && uti.Arguments.Count == 0) { @@ -1088,7 +1095,7 @@ void UserDefinedType(out Declaration/*!*/ decl, QKeyValue kv) { if (StartOf(14)) { WhiteSpaceIdents(out paramTokens); } - if (la.kind == 34) { + if (la.kind == 35) { Get(); Type(out body); synonym = true; @@ -1117,7 +1124,7 @@ void WhiteSpaceIdents(out List/*!*/ xs) { void Constructors(DatatypeTypeCtorDecl datatypeTypeCtorDecl) { Constructor(datatypeTypeCtorDecl); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Constructor(datatypeTypeCtorDecl); } @@ -1126,11 +1133,11 @@ void Constructors(DatatypeTypeCtorDecl datatypeTypeCtorDecl) { void Constructor(DatatypeTypeCtorDecl datatypeTypeCtorDecl) { IToken name; List fields = new List(); Ident(out name); - Expect(11); + Expect(12); if (StartOf(12)) { AttributesIdsTypeWheres(false, "datatype constructor", delegate(TypedIdent ti, QKeyValue kv) { fields.Add(new Formal(ti.tok, ti, true, kv)); }); } - Expect(12); + Expect(13); if (!datatypeTypeCtorDecl.AddConstructor(name, name.val, fields)) { this.SemErr($"constructor name {name.val} used more than once in datatype"); } @@ -1139,9 +1146,9 @@ void Constructor(DatatypeTypeCtorDecl datatypeTypeCtorDecl) { void Invariant(List invariants) { Expr e; IToken tok = null; QKeyValue kv = null; - Expect(36); + Expect(37); tok = t; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); @@ -1150,53 +1157,53 @@ void Invariant(List invariants) { } void MoverQualifier(ref MoverType moverType) { - if (la.kind == 43) { + if (la.kind == 44) { Get(); moverType = MoverType.Left; - } else if (la.kind == 44) { + } else if (la.kind == 45) { Get(); moverType = MoverType.Right; - } else if (la.kind == 45) { + } else if (la.kind == 46) { Get(); moverType = MoverType.Both; - } else if (la.kind == 46) { + } else if (la.kind == 47) { Get(); moverType = MoverType.Atomic; - } else SynErr(138); + } else SynErr(139); } void SpecAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List mods, List creates, List requires, List yieldRequires, List asserts) { - if (la.kind == 41) { + if (la.kind == 42) { SpecRefinedAction(ref refinedAction); IToken m; - if (la.kind == 42) { + if (la.kind == 43) { Get(); Ident(out m); invariantAction = new ActionDeclRef(m, m.val); } Expect(10); - } else if (la.kind == 54) { + } else if (la.kind == 55) { SpecModifies(mods); - } else if (la.kind == 40) { + } else if (la.kind == 41) { SpecCreates(creates); - } else if (la.kind == 49) { + } else if (la.kind == 50) { SpecYieldRequires(requires, yieldRequires); - } else if (la.kind == 48) { + } else if (la.kind == 49) { SpecAsserts(asserts); - } else SynErr(139); + } else SynErr(140); } void ImplBody(out List/*!*/ locals, out StmtList/*!*/ stmtList) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List(); - Expect(26); - while (la.kind == 9) { + Expect(27); + while (la.kind == 9 || la.kind == 11) { LocalVars(locals); } StmtList(out stmtList); } void SpecCreates(List creates) { - Expect(40); + Expect(41); List cs; Idents(out cs); foreach(IToken c in cs) { creates.Add(new ActionDeclRef(c, c.val)); } @@ -1205,8 +1212,8 @@ void SpecCreates(List creates) { void SpecRefinedAction(ref ActionDeclRef refinedAction) { IToken m; QKeyValue kv = null; - Expect(41); - while (la.kind == 26) { + Expect(42); + while (la.kind == 27) { Attribute(ref kv); } Ident(out m); @@ -1220,7 +1227,7 @@ void SpecRefinedAction(ref ActionDeclRef refinedAction) { void SpecModifies(List mods) { List ms; - Expect(54); + Expect(55); if (StartOf(14)) { Idents(out ms); foreach(IToken m in ms) { mods.Add(new IdentifierExpr(m, m.val)); } @@ -1230,26 +1237,26 @@ void SpecModifies(List mods) { void SpecYieldRequires(List pre, List yieldRequires ) { Expr e; Cmd cmd; Token tok; QKeyValue kv = null; - Expect(49); + Expect(50); tok = t; if (StartOf(16)) { - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); pre.Add(new Requires(tok, false, e, null, kv)); - } else if (la.kind == 38 || la.kind == 53 || la.kind == 71) { + } else if (la.kind == 39 || la.kind == 54 || la.kind == 72) { CallCmd(out cmd); yieldRequires.Add((CallCmd)cmd); - } else SynErr(140); + } else SynErr(141); Expect(10); } void SpecAsserts(List asserts ) { Expr e; Token tok; QKeyValue kv = null; - Expect(48); + Expect(49); tok = t; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); @@ -1258,18 +1265,18 @@ void SpecAsserts(List asserts ) { } void SpecYieldPrePost(ref ActionDeclRef refinedAction, List pre, List post, List yieldRequires, List yieldEnsures, List yieldPreserves, List mods) { - if (la.kind == 41) { + if (la.kind == 42) { SpecRefinedAction(ref refinedAction); Expect(10); - } else if (la.kind == 49) { - SpecYieldRequires(pre, yieldRequires); } else if (la.kind == 50) { - SpecYieldEnsures(post, yieldEnsures); + SpecYieldRequires(pre, yieldRequires); } else if (la.kind == 51) { + SpecYieldEnsures(post, yieldEnsures); + } else if (la.kind == 52) { SpecYieldPreserves(yieldPreserves); - } else if (la.kind == 54) { + } else if (la.kind == 55) { SpecModifies(mods); - } else SynErr(141); + } else SynErr(142); } void CallCmd(out Cmd c) { @@ -1279,15 +1286,15 @@ void CallCmd(out Cmd c) { bool isFree = false; c = null; - if (la.kind == 38) { + if (la.kind == 39) { Get(); isAsync = true; } - if (la.kind == 53) { + if (la.kind == 54) { Get(); isFree = true; } - Expect(71); + Expect(72); x = t; CallParams(isAsync, isFree, x, out c); @@ -1295,24 +1302,24 @@ void CallCmd(out Cmd c) { void SpecYieldEnsures(List post, List yieldEnsures ) { Expr e; Cmd cmd; Token tok; QKeyValue kv = null; - Expect(50); + Expect(51); tok = t; if (StartOf(16)) { - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); post.Add(new Ensures(tok, false, e, null, kv)); - } else if (la.kind == 38 || la.kind == 53 || la.kind == 71) { + } else if (la.kind == 39 || la.kind == 54 || la.kind == 72) { CallCmd(out cmd); yieldEnsures.Add((CallCmd)cmd); - } else SynErr(142); + } else SynErr(143); Expect(10); } void SpecYieldPreserves(List yieldPreserves ) { Cmd cmd; Token tok; - Expect(51); + Expect(52); tok = t; CallCmd(out cmd); yieldPreserves.Add((CallCmd)cmd); @@ -1324,52 +1331,52 @@ void ProcSignature(bool allowWhereClausesOnFormals, out IToken/*!*/ name, out Li 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(); outs = new List(); kv = null; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Ident(out name); - if (la.kind == 21) { + if (la.kind == 22) { TypeParams(out typeParamTok, out typeParams); } ProcFormals(true, allowWhereClausesOnFormals, out ins); - if (la.kind == 30) { + if (la.kind == 31) { Get(); ProcFormals(false, allowWhereClausesOnFormals, out outs); } } void Spec(List pre, List mods, List post) { - if (la.kind == 54) { + if (la.kind == 55) { SpecModifies(mods); - } else if (la.kind == 53) { + } else if (la.kind == 54) { Get(); SpecPrePost(true, pre, post); - } else if (la.kind == 49 || la.kind == 50) { + } else if (la.kind == 50 || la.kind == 51) { SpecPrePost(false, pre, post); - } else SynErr(143); + } else SynErr(144); } void SpecPrePost(bool free, List/*!*/ pre, List/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; - if (la.kind == 49) { + if (la.kind == 50) { Get(); tok = t; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); Expect(10); pre.Add(new Requires(tok, free, e, null, kv)); - } else if (la.kind == 50) { + } else if (la.kind == 51) { Get(); tok = t; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); Expect(10); post.Add(new Ensures(tok, free, e, null, kv)); - } else SynErr(144); + } else SynErr(145); } void StmtList(out StmtList/*!*/ stmtList) { @@ -1405,7 +1412,7 @@ void StmtList(out StmtList/*!*/ stmtList) { cs = new List(); } - } else if (la.kind == 57 || la.kind == 59 || la.kind == 61) { + } else if (la.kind == 58 || la.kind == 60 || la.kind == 62) { StructuredCmd(out ecn); ec = ecn; if (startToken == null) { startToken = ec.tok; cs = new List(); } @@ -1425,7 +1432,7 @@ void StmtList(out StmtList/*!*/ stmtList) { } } - Expect(27); + Expect(28); IToken/*!*/ endCurly = t; if (startToken == null && bigblocks.Count == 0) { startToken = t; cs = new List(); @@ -1450,8 +1457,8 @@ void LabelOrCmd(out Cmd c, out IToken label) { HideRevealCmd.Modes mode; IdentifierExpr hideRevealId = null; - if (la.kind == 62 || la.kind == 63) { - if (la.kind == 62) { + if (la.kind == 63 || la.kind == 64) { + if (la.kind == 63) { Get(); mode = HideRevealCmd.Modes.Reveal; } else { @@ -1461,40 +1468,40 @@ void LabelOrCmd(out Cmd c, out IToken label) { if (la.kind == 1) { Get(); hideRevealId = new IdentifierExpr(t, t.val); - } else if (la.kind == 60) { + } else if (la.kind == 61) { Get(); - } else SynErr(145); + } else SynErr(146); c = hideRevealId == null ? new HideRevealCmd(t, mode) : new HideRevealCmd(hideRevealId, mode); Expect(10); - } else if (la.kind == 64) { + } else if (la.kind == 65) { Get(); c = new ChangeScope(t, ChangeScope.Modes.Pop); Expect(10); - } else if (la.kind == 65) { + } else if (la.kind == 66) { Get(); c = new ChangeScope(t, ChangeScope.Modes.Push); Expect(10); } else if (StartOf(14)) { LabelOrAssign(out c, out label); - } else if (la.kind == 66) { + } else if (la.kind == 67) { Get(); x = t; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); c = new AssertCmd(x, e, kv); Expect(10); - } else if (la.kind == 67) { + } else if (la.kind == 68) { Get(); x = t; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); c = new AssumeCmd(x, e, kv); Expect(10); - } else if (la.kind == 68) { + } else if (la.kind == 69) { Get(); x = t; Idents(out xs); @@ -1506,30 +1513,30 @@ void LabelOrCmd(out Cmd c, out IToken label) { } c = new HavocCmd(x,ids); - } else if (la.kind == 38 || la.kind == 53 || la.kind == 71) { + } else if (la.kind == 39 || la.kind == 54 || la.kind == 72) { CallCmd(out cn); Expect(10); c = cn; - } else if (la.kind == 72) { + } else if (la.kind == 73) { ParCallCmd(out cn); c = cn; - } else SynErr(146); + } else SynErr(147); } void StructuredCmd(out StructuredCmd/*!*/ ec) { Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec)); IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd; - if (la.kind == 57) { + if (la.kind == 58) { IfCmd(out ifcmd); ec = ifcmd; - } else if (la.kind == 59) { + } else if (la.kind == 60) { WhileCmd(out wcmd); ec = wcmd; - } else if (la.kind == 61) { + } else if (la.kind == 62) { BreakCmd(out bcmd); ec = bcmd; - } else SynErr(147); + } else SynErr(148); } void TransferCmd(out TransferCmd/*!*/ tc) { @@ -1537,7 +1544,7 @@ void TransferCmd(out TransferCmd/*!*/ tc) { Token y; List/*!*/ xs; List ss = new List(); - if (la.kind == 55) { + if (la.kind == 56) { Get(); y = t; Idents(out xs); @@ -1546,10 +1553,10 @@ void TransferCmd(out TransferCmd/*!*/ tc) { ss.Add(s.val); } tc = new GotoCmd(y, ss); - } else if (la.kind == 56) { + } else if (la.kind == 57) { Get(); tc = new ReturnCmd(t); - } else SynErr(148); + } else SynErr(149); Expect(10); } @@ -1560,21 +1567,21 @@ void IfCmd(out IfCmd/*!*/ ifcmd) { IfCmd/*!*/ elseIf; IfCmd elseIfOption = null; StmtList/*!*/ els; StmtList elseOption = null; - Expect(57); + Expect(58); x = t; Guard(out guard); - Expect(26); + Expect(27); StmtList(out thn); - if (la.kind == 58) { + if (la.kind == 59) { Get(); - if (la.kind == 57) { + if (la.kind == 58) { IfCmd(out elseIf); elseIfOption = elseIf; - } else if (la.kind == 26) { + } else if (la.kind == 27) { Get(); StmtList(out els); elseOption = els; - } else SynErr(149); + } else SynErr(150); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); } @@ -1587,18 +1594,18 @@ void WhileCmd(out WhileCmd wcmd) { StmtList body; QKeyValue kv = null; - Expect(59); + Expect(60); x = t; Guard(out guard); Contract.Assume(guard == null || cce.Owner.None(guard)); - while (la.kind == 36 || la.kind == 53) { + while (la.kind == 37 || la.kind == 54) { isFree = false; z = la/*lookahead token*/; - if (la.kind == 53) { + if (la.kind == 54) { Get(); isFree = true; } - Expect(36); - while (la.kind == 26) { + Expect(37); + while (la.kind == 27) { Attribute(ref kv); } if (StartOf(19)) { @@ -1610,13 +1617,13 @@ void WhileCmd(out WhileCmd wcmd) { } kv = null; - } else if (la.kind == 38 || la.kind == 53 || la.kind == 71) { + } else if (la.kind == 39 || la.kind == 54 || la.kind == 72) { CallCmd(out cmd); yields.Add((CallCmd)cmd); - } else SynErr(150); + } else SynErr(151); Expect(10); } - Expect(26); + Expect(27); StmtList(out body); wcmd = new WhileCmd(x, guard, invariants, yields, body); } @@ -1625,7 +1632,7 @@ void BreakCmd(out BreakCmd/*!*/ bcmd) { Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y; string breakLabel = null; - Expect(61); + Expect(62); x = t; if (StartOf(14)) { Ident(out y); @@ -1637,15 +1644,15 @@ void BreakCmd(out BreakCmd/*!*/ bcmd) { void Guard(out Expr e) { Expr/*!*/ ee; e = null; - Expect(11); - if (la.kind == 60) { + Expect(12); + if (la.kind == 61) { Get(); e = null; } else if (StartOf(19)) { Expression(out ee); e = ee; - } else SynErr(151); - Expect(12); + } else SynErr(152); + Expect(13); } void LabelOrAssign(out Cmd c, out IToken label) { @@ -1661,18 +1668,18 @@ void LabelOrAssign(out Cmd c, out IToken label) { Ident(out id); x = t; - if (la.kind == 13) { + if (la.kind == 14) { Get(); c = null; label = x; - } else if (la.kind == 11) { + } else if (la.kind == 12) { Get(); Idents(out ids); - Expect(12); + Expect(13); lhsExpr = new NAryExpr(x, new FunctionCall(new IdentifierExpr(id, id.val)), ids.Select(id => new IdentifierExpr(id, id.val)).ToList()); - Expect(69); + Expect(70); x = t; /* use location of := */ - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Expression(out e0); @@ -1682,8 +1689,8 @@ void LabelOrAssign(out Cmd c, out IToken label) { } else if (StartOf(20)) { lhss = new List(); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 19 || la.kind == 70) { - if (la.kind == 19) { + while (la.kind == 20 || la.kind == 71) { + if (la.kind == 20) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); } else { @@ -1692,12 +1699,12 @@ void LabelOrAssign(out Cmd c, out IToken label) { } } lhss.Add(lhs); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Ident(out id); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 19 || la.kind == 70) { - if (la.kind == 19) { + while (la.kind == 20 || la.kind == 71) { + if (la.kind == 20) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); } else { @@ -1707,22 +1714,22 @@ void LabelOrAssign(out Cmd c, out IToken label) { } lhss.Add(lhs); } - Expect(69); + Expect(70); x = t; /* use location of := */ - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Expression(out e0); rhss = new List (); rhss.Add(e0); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Expression(out e0); rhss.Add(e0); } Expect(10); c = new AssignCmd(x, lhss, rhss, kv); - } else SynErr(152); + } else SynErr(153); } void ParCallCmd(out Cmd d) { @@ -1731,11 +1738,11 @@ void ParCallCmd(out Cmd d) { Cmd c = null; List callCmds = new List(); - Expect(72); + Expect(73); x = t; CallParams(false, false, x, out c); callCmds.Add((CallCmd)c); - while (la.kind == 73) { + while (la.kind == 74) { Get(); CallParams(false, false, x, out c); callCmds.Add((CallCmd)c); @@ -1748,23 +1755,23 @@ void MapAssignIndex(out IToken/*!*/ x, out List/*!*/ indexes) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List (); Expr/*!*/ e; - Expect(19); + Expect(20); x = t; if (StartOf(19)) { Expression(out e); indexes.Add(e); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Expression(out e); indexes.Add(e); } } - Expect(20); + Expect(21); } void FieldAccess(out IToken x, out FieldAccess fieldAccess) { Contract.Ensures(Contract.ValueAtReturn(out fieldAccess) != null); IToken id; - Expect(70); + Expect(71); x = t; Ident(out id); fieldAccess = new FieldAccess(id, id.val); @@ -1779,57 +1786,57 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { IToken p; c = null; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Ident(out first); - if (la.kind == 11) { + if (la.kind == 12) { Get(); if (StartOf(19)) { Expression(out en); es.Add(en); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Expression(out en); es.Add(en); } } - Expect(12); + Expect(13); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else if (la.kind == 14 || la.kind == 69) { + } else if (la.kind == 15 || la.kind == 70) { ids.Add(new IdentifierExpr(first, first.val)); - if (la.kind == 14) { + if (la.kind == 15) { Get(); Ident(out p); ids.Add(new IdentifierExpr(p, p.val)); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Ident(out p); ids.Add(new IdentifierExpr(p, p.val)); } } - Expect(69); + Expect(70); Ident(out first); - Expect(11); + Expect(12); if (StartOf(19)) { Expression(out en); es.Add(en); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Expression(out en); es.Add(en); } } - Expect(12); + Expect(13); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else SynErr(153); + } else SynErr(154); } void Expressions(out List/*!*/ es) { Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List(); Expression(out e); es.Add(e); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Expression(out e); es.Add(e); @@ -1840,7 +1847,7 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; LogicalExpression(out e0); if (StartOf(21)) { - if (la.kind == 76 || la.kind == 77) { + if (la.kind == 77 || la.kind == 78) { ImpliesOp(); x = t; ImpliesExpression(true, out e1); @@ -1852,7 +1859,7 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) { x = t; LogicalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); - while (la.kind == 78 || la.kind == 79) { + while (la.kind == 79 || la.kind == 80) { ExpliesOp(); x = t; LogicalExpression(out e1); @@ -1863,23 +1870,23 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) { } void EquivOp() { - if (la.kind == 74) { + if (la.kind == 75) { Get(); - } else if (la.kind == 75) { + } else if (la.kind == 76) { Get(); - } else SynErr(154); + } else SynErr(155); } void LogicalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; RelationalExpression(out e0); if (StartOf(22)) { - if (la.kind == 80 || la.kind == 81) { + if (la.kind == 81 || la.kind == 82) { AndOp(); x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); - while (la.kind == 80 || la.kind == 81) { + while (la.kind == 81 || la.kind == 82) { AndOp(); x = t; RelationalExpression(out e1); @@ -1890,7 +1897,7 @@ void LogicalExpression(out Expr/*!*/ e0) { x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); - while (la.kind == 82 || la.kind == 83) { + while (la.kind == 83 || la.kind == 84) { OrOp(); x = t; RelationalExpression(out e1); @@ -1901,19 +1908,19 @@ void LogicalExpression(out Expr/*!*/ e0) { } void ImpliesOp() { - if (la.kind == 76) { + if (la.kind == 77) { Get(); - } else if (la.kind == 77) { + } else if (la.kind == 78) { Get(); - } else SynErr(155); + } else SynErr(156); } void ExpliesOp() { - if (la.kind == 78) { + if (la.kind == 79) { Get(); - } else if (la.kind == 79) { + } else if (la.kind == 80) { Get(); - } else SynErr(156); + } else SynErr(157); } void RelationalExpression(out Expr/*!*/ e0) { @@ -1927,25 +1934,25 @@ void RelationalExpression(out Expr/*!*/ e0) { } void AndOp() { - if (la.kind == 80) { + if (la.kind == 81) { Get(); - } else if (la.kind == 81) { + } else if (la.kind == 82) { Get(); - } else SynErr(157); + } else SynErr(158); } void OrOp() { - if (la.kind == 82) { + if (la.kind == 83) { Get(); - } else if (la.kind == 83) { + } else if (la.kind == 84) { Get(); - } else SynErr(158); + } else SynErr(159); } void BvTerm(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; Term(out e0); - while (la.kind == 91) { + while (la.kind == 92) { Get(); x = t; Term(out e1); @@ -1956,59 +1963,59 @@ void BvTerm(out Expr/*!*/ e0) { 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 84: { + case 85: { Get(); x = t; op=BinaryOperator.Opcode.Eq; break; } - case 21: { + case 22: { Get(); x = t; op=BinaryOperator.Opcode.Lt; break; } - case 22: { + case 23: { Get(); x = t; op=BinaryOperator.Opcode.Gt; break; } - case 85: { + case 86: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 86: { + case 87: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - case 87: { + case 88: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 88: { + case 89: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 89: { + case 90: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 90: { + case 91: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - default: SynErr(159); break; + default: SynErr(160); 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 == 92 || la.kind == 93) { + while (la.kind == 93 || la.kind == 94) { AddOp(out x, out op); Factor(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -2027,19 +2034,19 @@ void Factor(out Expr/*!*/ e0) { 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 == 92) { + if (la.kind == 93) { Get(); x = t; op=BinaryOperator.Opcode.Add; - } else if (la.kind == 93) { + } else if (la.kind == 94) { Get(); x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(160); + } else SynErr(161); } void Power(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; IsConstructor(out e0); - if (la.kind == 97) { + if (la.kind == 98) { Get(); x = t; Power(out e1); @@ -2049,25 +2056,25 @@ void Power(out Expr/*!*/ e0) { 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 == 60) { + if (la.kind == 61) { Get(); x = t; op=BinaryOperator.Opcode.Mul; - } else if (la.kind == 94) { + } else if (la.kind == 95) { Get(); x = t; op=BinaryOperator.Opcode.Div; - } else if (la.kind == 95) { + } else if (la.kind == 96) { Get(); x = t; op=BinaryOperator.Opcode.Mod; - } else if (la.kind == 96) { + } else if (la.kind == 97) { Get(); x = t; op=BinaryOperator.Opcode.RealDiv; - } else SynErr(161); + } else SynErr(162); } void IsConstructor(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x, id; UnaryExpression(out e0); - if (la.kind == 98) { + if (la.kind == 99) { Get(); x = t; Ident(out id); @@ -2081,27 +2088,27 @@ void UnaryExpression(out Expr/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; - if (la.kind == 93) { + if (la.kind == 94) { Get(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); - } else if (la.kind == 99 || la.kind == 100) { + } else if (la.kind == 100 || la.kind == 101) { NegOp(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); } else if (StartOf(25)) { CoercionExpression(out e); - } else SynErr(162); + } else SynErr(163); } void NegOp() { - if (la.kind == 99) { + if (la.kind == 100) { Get(); - } else if (la.kind == 100) { + } else if (la.kind == 101) { Get(); - } else SynErr(163); + } else SynErr(164); } void CoercionExpression(out Expr/*!*/ e) { @@ -2110,7 +2117,7 @@ void CoercionExpression(out Expr/*!*/ e) { BigNum bn; ArrayExpression(out e); - while (la.kind == 13) { + while (la.kind == 14) { Get(); x = t; if (StartOf(15)) { @@ -2125,7 +2132,7 @@ void CoercionExpression(out Expr/*!*/ e) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(164); + } else SynErr(165); } } @@ -2137,8 +2144,8 @@ void ArrayExpression(out Expr/*!*/ e) { List/*!*/ allArgs = dummyExprSeq; AtomExpression(out e); - while (la.kind == 19 || la.kind == 70) { - if (la.kind == 19) { + while (la.kind == 20 || la.kind == 71) { + if (la.kind == 20) { Get(); x = t; allArgs = new List (); allArgs.Add(e); @@ -2151,7 +2158,7 @@ void ArrayExpression(out Expr/*!*/ e) { else allArgs.Add(index0); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -2159,7 +2166,7 @@ void ArrayExpression(out Expr/*!*/ e) { allArgs.Add(e1); } - if (la.kind == 69) { + if (la.kind == 70) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -2173,7 +2180,7 @@ void ArrayExpression(out Expr/*!*/ e) { allArgs.Add(e1); store = true; } } - Expect(20); + Expect(21); if (store) e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs); else if (bvExtract) @@ -2189,15 +2196,15 @@ void ArrayExpression(out Expr/*!*/ e) { if (StartOf(14)) { Ident(out id); e = new NAryExpr(x, new FieldAccess(id, id.val), new List { e }); - } else if (la.kind == 11) { + } else if (la.kind == 12) { Get(); Ident(out id); - Expect(69); + Expect(70); x = t; Expression(out e1); - Expect(12); + Expect(13); e = new NAryExpr(x, new FieldUpdate(id, id.val), new List { e, e1 }); - } else SynErr(165); + } else SynErr(166); } } } @@ -2224,18 +2231,18 @@ void AtomExpression(out Expr/*!*/ e) { List/*!*/ blocks; switch (la.kind) { - case 101: { + case 102: { Get(); e = new LiteralExpr(t, false); break; } - case 102: { + case 103: { Get(); e = new LiteralExpr(t, true); break; } - case 103: case 104: { - if (la.kind == 103) { + case 104: case 105: { + if (la.kind == 104) { Get(); } else { Get(); @@ -2243,8 +2250,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RNE); break; } - case 105: case 106: { - if (la.kind == 105) { + case 106: case 107: { + if (la.kind == 106) { Get(); } else { Get(); @@ -2252,8 +2259,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RNA); break; } - case 107: case 108: { - if (la.kind == 107) { + case 108: case 109: { + if (la.kind == 108) { Get(); } else { Get(); @@ -2261,8 +2268,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RTP); break; } - case 109: case 110: { - if (la.kind == 109) { + case 110: case 111: { + if (la.kind == 110) { Get(); } else { Get(); @@ -2270,8 +2277,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RTN); break; } - case 111: case 112: { - if (la.kind == 111) { + case 112: case 113: { + if (la.kind == 112) { Get(); } else { Get(); @@ -2304,67 +2311,67 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, t.val.Trim('"')); break; } - case 1: case 43: case 44: case 45: case 46: case 62: case 63: case 64: case 65: { + case 1: case 44: case 45: case 46: case 47: case 63: case 64: case 65: case 66: { Ident(out x); id = new IdentifierExpr(x, x.val); e = id; - if (la.kind == 11) { + if (la.kind == 12) { Get(); if (StartOf(19)) { Expressions(out es); e = new NAryExpr(x, new FunctionCall(id), es); - } else if (la.kind == 12) { + } else if (la.kind == 13) { e = new NAryExpr(x, new FunctionCall(id), new List()); - } else SynErr(166); - Expect(12); + } else SynErr(167); + Expect(13); } break; } - case 113: { + case 114: { Get(); x = t; - Expect(11); - Expression(out e); Expect(12); + Expression(out e); + Expect(13); e = new OldExpr(x, e); break; } - case 16: { + case 17: { Get(); x = t; - Expect(11); - Expression(out e); Expect(12); + Expression(out e); + Expect(13); e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List{ e }); break; } - case 17: { + case 18: { Get(); x = t; - Expect(11); - Expression(out e); Expect(12); + Expression(out e); + Expect(13); e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List{ e }); break; } - case 11: { + case 12: { Get(); if (StartOf(19)) { Expression(out e); if (e is BvBounds) this.SemErr("parentheses around bitvector bounds are not allowed"); - } else if (la.kind == 117 || la.kind == 118) { + } else if (la.kind == 118 || la.kind == 119) { 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 == 119 || la.kind == 120) { + } else if (la.kind == 120 || la.kind == 121) { 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 == 121 || la.kind == 122) { + } else if (la.kind == 122 || la.kind == 123) { Lambda(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); @@ -2374,20 +2381,20 @@ void AtomExpression(out Expr/*!*/ e) { e = new LambdaExpr(x, typeParams, ds, kv, e); } else if (la.kind == 9) { LetExpr(out e); - } else SynErr(167); - Expect(12); + } else SynErr(168); + Expect(13); break; } - case 57: { + case 58: { IfThenElseExpression(out e); break; } - case 114: { + case 115: { CodeExpression(out locals, out blocks); e = new CodeExpr(locals, blocks); break; } - default: SynErr(168); break; + default: SynErr(169); break; } } @@ -2399,7 +2406,7 @@ void Dec(out BigDec n) { } else if (la.kind == 6) { Get(); s = t.val; - } else SynErr(169); + } else SynErr(170); try { n = BigDec.FromString(s); } catch (FormatException) { @@ -2439,11 +2446,11 @@ void BvLit(out BigNum n, out int m) { } void Forall() { - if (la.kind == 117) { + if (la.kind == 118) { Get(); - } else if (la.kind == 118) { + } else if (la.kind == 119) { Get(); - } else SynErr(170); + } else SynErr(171); } void QuantifierBody(IToken/*!*/ q, out List/*!*/ typeParams, out List/*!*/ ds, @@ -2454,35 +2461,35 @@ void QuantifierBody(IToken/*!*/ q, out List/*!*/ typeParams, out L kv = null; ds = new List (); - if (la.kind == 21) { + if (la.kind == 22) { TypeParams(out tok, out typeParams); if (StartOf(12)) { BoundVars(out ds); } } else if (StartOf(12)) { BoundVars(out ds); - } else SynErr(171); + } else SynErr(172); QSep(); - while (la.kind == 26) { + while (la.kind == 27) { AttributeOrTrigger(ref kv, ref trig); } Expression(out body); } void Exists() { - if (la.kind == 119) { + if (la.kind == 120) { Get(); - } else if (la.kind == 120) { + } else if (la.kind == 121) { Get(); - } else SynErr(172); + } else SynErr(173); } void Lambda() { - if (la.kind == 121) { + if (la.kind == 122) { Get(); - } else if (la.kind == 122) { + } else if (la.kind == 123) { Get(); - } else SynErr(173); + } else SynErr(174); } void LetExpr(out Expr/*!*/ letexpr) { @@ -2498,21 +2505,21 @@ void LetExpr(out Expr/*!*/ letexpr) { tok = t; LetVar(out v); ds.Add(v); - while (la.kind == 14) { + while (la.kind == 15) { Get(); LetVar(out v); ds.Add(v); } - Expect(69); + Expect(70); Expression(out e0); rhss.Add(e0); - while (la.kind == 14) { + while (la.kind == 15) { Get(); Expression(out e0); rhss.Add(e0); } Expect(10); - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Expression(out body); @@ -2524,12 +2531,12 @@ void IfThenElseExpression(out Expr/*!*/ e) { IToken/*!*/ tok; Expr/*!*/ e0, e1, e2; e = dummyExpr; - Expect(57); + Expect(58); tok = t; Expression(out e0); - Expect(116); + Expect(117); Expression(out e1); - Expect(58); + Expect(59); Expression(out e2); e = new NAryExpr(tok, new IfThenElse(tok), new List{ e0, e1, e2 }); } @@ -2538,8 +2545,8 @@ void CodeExpression(out List/*!*/ locals, out List/*!*/ bl Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List(); Block/*!*/ b; blocks = new List(); - Expect(114); - while (la.kind == 9) { + Expect(115); + while (la.kind == 9 || la.kind == 11) { LocalVars(locals); } SpecBlock(out b); @@ -2548,7 +2555,7 @@ void CodeExpression(out List/*!*/ locals, out List/*!*/ bl SpecBlock(out b); blocks.Add(b); } - Expect(115); + Expect(116); } void SpecBlock(out Block/*!*/ b) { @@ -2561,7 +2568,7 @@ void SpecBlock(out Block/*!*/ b) { Expr/*!*/ e; Ident(out x); - Expect(13); + Expect(14); while (StartOf(18)) { LabelOrCmd(out c, out label); Contract.Assert(c == null || label == null); @@ -2572,7 +2579,7 @@ void SpecBlock(out Block/*!*/ b) { } } - if (la.kind == 55) { + if (la.kind == 56) { Get(); y = t; Idents(out xs); @@ -2581,11 +2588,11 @@ void SpecBlock(out Block/*!*/ b) { ss.Add(s.val); } b = new Block(x,x.val,cs,new GotoCmd(y,ss)); - } else if (la.kind == 56) { + } else if (la.kind == 57) { Get(); Expression(out e); b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); - } else SynErr(174); + } else SynErr(175); Expect(10); } @@ -2594,16 +2601,16 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { IToken id; List parameters; object/*!*/ param; - Expect(26); + Expect(27); tok = t; - if (la.kind == 13) { + if (la.kind == 14) { Get(); Ident(out id); parameters = new List(); if (StartOf(19)) { AttributeParameter(out param); parameters.Add(param); - while (la.kind == 14) { + while (la.kind == 15) { Get(); AttributeParameter(out param); parameters.Add(param); @@ -2631,7 +2638,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { } else if (StartOf(19)) { Expression(out e); es = new List { e }; - while (la.kind == 14) { + while (la.kind == 15) { Get(); Expression(out e); es.Add(e); @@ -2642,8 +2649,8 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else SynErr(175); - Expect(27); + } else SynErr(176); + Expect(28); } void AttributeParameter(out object/*!*/ o) { @@ -2657,22 +2664,22 @@ void AttributeParameter(out object/*!*/ o) { } else if (StartOf(19)) { Expression(out e); o = e; - } else SynErr(176); + } else SynErr(177); } void QSep() { - if (la.kind == 123) { + if (la.kind == 124) { Get(); - } else if (la.kind == 124) { + } else if (la.kind == 125) { Get(); - } else SynErr(177); + } else SynErr(178); } void LetVar(out Variable/*!*/ v) { QKeyValue kv = null; IToken id; - while (la.kind == 26) { + while (la.kind == 27) { Attribute(ref kv); } Ident(out id); @@ -2694,33 +2701,33 @@ public void Parse() { } 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,_x,_x,_x, _x,_x,_x,_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,_T, _x,_x,_x,_x, _T,_T,_x,_T, _T,_T,_x,_T, _x,_T,_T,_T, _x,_x,_x,_T, _T,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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,_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,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_T,_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,_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,_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,_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,_T,_T, _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,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, - {_x,_x,_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,_T,_T,_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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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, _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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, - {_x,_x,_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,_T,_x,_x, _x,_x,_x,_x, _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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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,_T,_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,_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,_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,_x,_x,_x, _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, _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,_T,_x,_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,_T, _T,_T,_T,_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,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_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,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_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,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_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,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_T,_x,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_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,_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,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, - {_x,_T,_T,_T, _T,_T,_T,_T, _x,_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,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_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,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_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,_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,_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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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, _x,_x,_x,_x, _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,_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, _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,_x,_x, _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,_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,_T,_T,_T, _T,_T,_T,_T, _x,_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,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_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,_T,_T,_T, _T,_T,_T,_T, _T,_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,_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,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_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,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_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,_x, _x,_x,_x,_x, _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, _T,_x,_x,_x, _x,_T,_T,_x, _T,_T,_T,_x, _T,_x,_T,_T, _T,_x,_x,_x, _T,_T,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_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, _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,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_x,_T,_x, _x,_x,_x,_T, _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,_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,_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,_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,_T, _T,_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,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_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,_T,_T, _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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_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,_T,_x, _x,_x,_x,_x, _x,_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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_T, _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,_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, _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,_x,_x, _x,_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,_x, _T,_T,_T,_T, _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,_T,_x,_x, _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, _T,_T,_T,_T, _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,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_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, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_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,_T,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _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,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_T,_x, _T,_T,_T,_x, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_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,_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,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_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,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_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,_T,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _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,_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, _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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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, _x,_x,_x,_x, _x,_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,_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,_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,_x,_x, _x,_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, _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,_T,_T,_T, _T,_T,_T,_T, _x,_x,_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,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_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,_T,_T, _T,_T,_T,_T, _T,_T,_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,_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,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_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,_T,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x} }; } // end Parser @@ -2756,173 +2763,174 @@ string GetSyntaxErrorString(int n) { case 8: s = "\"yield\" expected"; break; case 9: s = "\"var\" 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 = "\",\" expected"; break; - case 15: s = "\"where\" expected"; break; - case 16: s = "\"int\" expected"; break; - case 17: s = "\"real\" expected"; break; - case 18: s = "\"bool\" expected"; break; - case 19: s = "\"[\" expected"; break; - case 20: s = "\"]\" expected"; break; - case 21: s = "\"<\" expected"; break; - case 22: s = "\">\" expected"; break; - case 23: s = "\"const\" expected"; break; - case 24: s = "\"unique\" expected"; break; - case 25: s = "\"uses\" expected"; break; - case 26: s = "\"{\" expected"; break; - case 27: s = "\"}\" expected"; break; - case 28: s = "\"revealed\" expected"; break; - case 29: s = "\"function\" expected"; break; - case 30: s = "\"returns\" expected"; break; - case 31: s = "\"hideable\" expected"; break; - case 32: s = "\"axiom\" expected"; break; - case 33: s = "\"type\" expected"; break; - case 34: s = "\"=\" expected"; break; - case 35: s = "\"datatype\" expected"; break; - case 36: s = "\"invariant\" expected"; break; - case 37: s = "\"pure\" expected"; break; - case 38: s = "\"async\" expected"; break; - case 39: s = "\"action\" expected"; break; - case 40: s = "\"creates\" expected"; break; - case 41: s = "\"refines\" expected"; break; - case 42: s = "\"using\" expected"; break; - case 43: s = "\"left\" expected"; break; - case 44: s = "\"right\" expected"; break; - case 45: s = "\"both\" expected"; break; - case 46: s = "\"atomic\" expected"; break; - case 47: s = "\"procedure\" expected"; break; - case 48: s = "\"asserts\" expected"; break; - case 49: s = "\"requires\" expected"; break; - case 50: s = "\"ensures\" expected"; break; - case 51: s = "\"preserves\" expected"; break; - case 52: s = "\"implementation\" expected"; break; - case 53: s = "\"free\" expected"; break; - case 54: s = "\"modifies\" expected"; break; - case 55: s = "\"goto\" expected"; break; - case 56: s = "\"return\" expected"; break; - case 57: s = "\"if\" expected"; break; - case 58: s = "\"else\" expected"; break; - case 59: s = "\"while\" expected"; break; - case 60: s = "\"*\" expected"; break; - case 61: s = "\"break\" expected"; break; - case 62: s = "\"reveal\" expected"; break; - case 63: s = "\"hide\" expected"; break; - case 64: s = "\"pop\" expected"; break; - case 65: s = "\"push\" expected"; break; - case 66: s = "\"assert\" expected"; break; - case 67: s = "\"assume\" expected"; break; - case 68: s = "\"havoc\" expected"; break; - case 69: s = "\":=\" expected"; break; - case 70: s = "\"->\" expected"; break; - case 71: s = "\"call\" expected"; break; - case 72: s = "\"par\" expected"; break; - case 73: s = "\"|\" expected"; break; - case 74: s = "\"<==>\" expected"; break; - case 75: s = "\"\\u21d4\" expected"; break; - case 76: s = "\"==>\" expected"; break; - case 77: s = "\"\\u21d2\" expected"; break; - case 78: s = "\"<==\" expected"; break; - case 79: s = "\"\\u21d0\" expected"; break; - case 80: s = "\"&&\" expected"; break; - case 81: s = "\"\\u2227\" expected"; break; - case 82: s = "\"||\" expected"; break; - case 83: s = "\"\\u2228\" expected"; break; - case 84: s = "\"==\" expected"; break; - case 85: s = "\"<=\" expected"; break; - case 86: s = "\">=\" expected"; break; - case 87: s = "\"!=\" expected"; break; - case 88: s = "\"\\u2260\" expected"; break; - case 89: s = "\"\\u2264\" expected"; break; - case 90: s = "\"\\u2265\" expected"; break; - case 91: s = "\"++\" expected"; break; - case 92: s = "\"+\" expected"; break; - case 93: s = "\"-\" expected"; break; - case 94: s = "\"div\" expected"; break; - case 95: s = "\"mod\" expected"; break; - case 96: s = "\"/\" expected"; break; - case 97: s = "\"**\" expected"; break; - case 98: s = "\"is\" expected"; break; - case 99: s = "\"!\" expected"; break; - case 100: s = "\"\\u00ac\" expected"; break; - case 101: s = "\"false\" expected"; break; - case 102: s = "\"true\" expected"; break; - case 103: s = "\"roundNearestTiesToEven\" expected"; break; - case 104: s = "\"RNE\" expected"; break; - case 105: s = "\"roundNearestTiesToAway\" expected"; break; - case 106: s = "\"RNA\" expected"; break; - case 107: s = "\"roundTowardPositive\" expected"; break; - case 108: s = "\"RTP\" expected"; break; - case 109: s = "\"roundTowardNegative\" expected"; break; - case 110: s = "\"RTN\" expected"; break; - case 111: s = "\"roundTowardZero\" expected"; break; - case 112: s = "\"RTZ\" expected"; break; - case 113: s = "\"old\" expected"; break; - case 114: s = "\"|{\" expected"; break; - case 115: s = "\"}|\" expected"; break; - case 116: s = "\"then\" expected"; break; - case 117: s = "\"forall\" expected"; break; - case 118: s = "\"\\u2200\" expected"; break; - case 119: s = "\"exists\" expected"; break; - case 120: s = "\"\\u2203\" expected"; break; - case 121: s = "\"lambda\" expected"; break; - case 122: s = "\"\\u03bb\" expected"; break; - case 123: s = "\"::\" expected"; break; - case 124: s = "\"\\u2022\" expected"; break; - case 125: s = "??? expected"; break; - case 126: s = "invalid BoogiePL"; break; + case 11: s = "\"monotonic\" expected"; break; + case 12: s = "\"(\" expected"; break; + case 13: s = "\")\" expected"; break; + case 14: s = "\":\" expected"; break; + case 15: s = "\",\" expected"; break; + case 16: s = "\"where\" expected"; break; + case 17: s = "\"int\" expected"; break; + case 18: s = "\"real\" expected"; break; + case 19: s = "\"bool\" expected"; break; + case 20: s = "\"[\" expected"; break; + case 21: s = "\"]\" expected"; break; + case 22: s = "\"<\" expected"; break; + case 23: s = "\">\" expected"; break; + case 24: s = "\"const\" expected"; break; + case 25: s = "\"unique\" expected"; break; + case 26: s = "\"uses\" expected"; break; + case 27: s = "\"{\" expected"; break; + case 28: s = "\"}\" expected"; break; + case 29: s = "\"revealed\" expected"; break; + case 30: s = "\"function\" expected"; break; + case 31: s = "\"returns\" expected"; break; + case 32: s = "\"hideable\" expected"; break; + case 33: s = "\"axiom\" expected"; break; + case 34: s = "\"type\" expected"; break; + case 35: s = "\"=\" expected"; break; + case 36: s = "\"datatype\" expected"; break; + case 37: s = "\"invariant\" expected"; break; + case 38: s = "\"pure\" expected"; break; + case 39: s = "\"async\" expected"; break; + case 40: s = "\"action\" expected"; break; + case 41: s = "\"creates\" expected"; break; + case 42: s = "\"refines\" expected"; break; + case 43: s = "\"using\" expected"; break; + case 44: s = "\"left\" expected"; break; + case 45: s = "\"right\" expected"; break; + case 46: s = "\"both\" expected"; break; + case 47: s = "\"atomic\" expected"; break; + case 48: s = "\"procedure\" expected"; break; + case 49: s = "\"asserts\" expected"; break; + case 50: s = "\"requires\" expected"; break; + case 51: s = "\"ensures\" expected"; break; + case 52: s = "\"preserves\" expected"; break; + case 53: s = "\"implementation\" expected"; break; + case 54: s = "\"free\" expected"; break; + case 55: s = "\"modifies\" expected"; break; + case 56: s = "\"goto\" expected"; break; + case 57: s = "\"return\" expected"; break; + case 58: s = "\"if\" expected"; break; + case 59: s = "\"else\" expected"; break; + case 60: s = "\"while\" expected"; break; + case 61: s = "\"*\" expected"; break; + case 62: s = "\"break\" expected"; break; + case 63: s = "\"reveal\" expected"; break; + case 64: s = "\"hide\" expected"; break; + case 65: s = "\"pop\" expected"; break; + case 66: s = "\"push\" expected"; break; + case 67: s = "\"assert\" expected"; break; + case 68: s = "\"assume\" expected"; break; + case 69: s = "\"havoc\" expected"; break; + case 70: s = "\":=\" expected"; break; + case 71: s = "\"->\" expected"; break; + case 72: s = "\"call\" expected"; break; + case 73: s = "\"par\" expected"; break; + case 74: s = "\"|\" expected"; break; + case 75: s = "\"<==>\" expected"; break; + case 76: s = "\"\\u21d4\" expected"; break; + case 77: s = "\"==>\" expected"; break; + case 78: s = "\"\\u21d2\" expected"; break; + case 79: s = "\"<==\" expected"; break; + case 80: s = "\"\\u21d0\" expected"; break; + case 81: s = "\"&&\" expected"; break; + case 82: s = "\"\\u2227\" expected"; break; + case 83: s = "\"||\" expected"; break; + case 84: s = "\"\\u2228\" expected"; break; + case 85: s = "\"==\" expected"; break; + case 86: s = "\"<=\" expected"; break; + case 87: s = "\">=\" expected"; break; + case 88: s = "\"!=\" expected"; break; + case 89: s = "\"\\u2260\" expected"; break; + case 90: s = "\"\\u2264\" expected"; break; + case 91: s = "\"\\u2265\" expected"; break; + case 92: s = "\"++\" expected"; break; + case 93: s = "\"+\" expected"; break; + case 94: s = "\"-\" expected"; break; + case 95: s = "\"div\" expected"; break; + case 96: s = "\"mod\" expected"; break; + case 97: s = "\"/\" expected"; break; + case 98: s = "\"**\" expected"; break; + case 99: s = "\"is\" expected"; break; + case 100: s = "\"!\" expected"; break; + case 101: s = "\"\\u00ac\" expected"; break; + case 102: s = "\"false\" expected"; break; + case 103: s = "\"true\" expected"; break; + case 104: s = "\"roundNearestTiesToEven\" expected"; break; + case 105: s = "\"RNE\" expected"; break; + case 106: s = "\"roundNearestTiesToAway\" expected"; break; + case 107: s = "\"RNA\" expected"; break; + case 108: s = "\"roundTowardPositive\" expected"; break; + case 109: s = "\"RTP\" expected"; break; + case 110: s = "\"roundTowardNegative\" expected"; break; + case 111: s = "\"RTN\" expected"; break; + case 112: s = "\"roundTowardZero\" expected"; break; + case 113: s = "\"RTZ\" expected"; break; + case 114: s = "\"old\" expected"; break; + case 115: s = "\"|{\" expected"; break; + case 116: s = "\"}|\" expected"; break; + case 117: s = "\"then\" expected"; break; + case 118: s = "\"forall\" expected"; break; + case 119: s = "\"\\u2200\" expected"; break; + case 120: s = "\"exists\" expected"; break; + case 121: s = "\"\\u2203\" expected"; break; + case 122: s = "\"lambda\" expected"; break; + case 123: s = "\"\\u03bb\" expected"; break; + case 124: s = "\"::\" expected"; break; + case 125: s = "\"\\u2022\" expected"; break; + case 126: s = "??? expected"; break; case 127: s = "invalid BoogiePL"; break; - case 128: s = "invalid Consts"; break; - case 129: s = "invalid Function"; break; + case 128: s = "invalid BoogiePL"; break; + case 129: s = "invalid Consts"; break; case 130: s = "invalid Function"; break; - case 131: s = "invalid YieldProcedureDecl"; break; - case 132: s = "invalid Procedure"; break; - case 133: s = "invalid ActionDecl"; break; - case 134: s = "invalid Type"; break; - case 135: s = "invalid TypeAtom"; break; - case 136: s = "invalid Ident"; break; - case 137: s = "invalid TypeArgs"; break; - case 138: s = "invalid MoverQualifier"; break; - case 139: s = "invalid SpecAction"; break; - case 140: s = "invalid SpecYieldRequires"; break; - case 141: s = "invalid SpecYieldPrePost"; break; - case 142: s = "invalid SpecYieldEnsures"; break; - case 143: s = "invalid Spec"; break; - case 144: s = "invalid SpecPrePost"; break; - case 145: s = "invalid LabelOrCmd"; break; + case 131: s = "invalid Function"; break; + case 132: s = "invalid YieldProcedureDecl"; break; + case 133: s = "invalid Procedure"; break; + case 134: s = "invalid ActionDecl"; break; + case 135: s = "invalid Type"; break; + case 136: s = "invalid TypeAtom"; break; + case 137: s = "invalid Ident"; break; + case 138: s = "invalid TypeArgs"; break; + case 139: s = "invalid MoverQualifier"; break; + case 140: s = "invalid SpecAction"; break; + case 141: s = "invalid SpecYieldRequires"; break; + case 142: s = "invalid SpecYieldPrePost"; break; + case 143: s = "invalid SpecYieldEnsures"; break; + case 144: s = "invalid Spec"; break; + case 145: s = "invalid SpecPrePost"; break; case 146: s = "invalid LabelOrCmd"; break; - case 147: s = "invalid StructuredCmd"; break; - case 148: s = "invalid TransferCmd"; break; - case 149: s = "invalid IfCmd"; break; - case 150: s = "invalid WhileCmd"; break; - case 151: s = "invalid Guard"; break; - case 152: s = "invalid LabelOrAssign"; break; - case 153: s = "invalid CallParams"; break; - case 154: s = "invalid EquivOp"; break; - case 155: s = "invalid ImpliesOp"; break; - case 156: s = "invalid ExpliesOp"; break; - case 157: s = "invalid AndOp"; break; - case 158: s = "invalid OrOp"; break; - case 159: s = "invalid RelOp"; break; - case 160: s = "invalid AddOp"; break; - case 161: s = "invalid MulOp"; break; - case 162: s = "invalid UnaryExpression"; break; - case 163: s = "invalid NegOp"; break; - case 164: s = "invalid CoercionExpression"; break; - case 165: s = "invalid ArrayExpression"; break; - case 166: s = "invalid AtomExpression"; break; + case 147: s = "invalid LabelOrCmd"; break; + case 148: s = "invalid StructuredCmd"; break; + case 149: s = "invalid TransferCmd"; break; + case 150: s = "invalid IfCmd"; break; + case 151: s = "invalid WhileCmd"; break; + case 152: s = "invalid Guard"; break; + case 153: s = "invalid LabelOrAssign"; break; + case 154: s = "invalid CallParams"; break; + case 155: s = "invalid EquivOp"; break; + case 156: s = "invalid ImpliesOp"; break; + case 157: s = "invalid ExpliesOp"; break; + case 158: s = "invalid AndOp"; break; + case 159: s = "invalid OrOp"; break; + case 160: s = "invalid RelOp"; break; + case 161: s = "invalid AddOp"; break; + case 162: s = "invalid MulOp"; break; + case 163: s = "invalid UnaryExpression"; break; + case 164: s = "invalid NegOp"; break; + case 165: s = "invalid CoercionExpression"; break; + case 166: s = "invalid ArrayExpression"; break; case 167: s = "invalid AtomExpression"; break; case 168: s = "invalid AtomExpression"; break; - case 169: s = "invalid Dec"; break; - case 170: s = "invalid Forall"; break; - case 171: s = "invalid QuantifierBody"; break; - case 172: s = "invalid Exists"; break; - case 173: s = "invalid Lambda"; break; - case 174: s = "invalid SpecBlock"; break; - case 175: s = "invalid AttributeOrTrigger"; break; - case 176: s = "invalid AttributeParameter"; break; - case 177: s = "invalid QSep"; break; + case 169: s = "invalid AtomExpression"; break; + case 170: s = "invalid Dec"; break; + case 171: s = "invalid Forall"; break; + case 172: s = "invalid QuantifierBody"; break; + case 173: s = "invalid Exists"; break; + case 174: s = "invalid Lambda"; break; + case 175: s = "invalid SpecBlock"; break; + case 176: s = "invalid AttributeOrTrigger"; break; + case 177: s = "invalid AttributeParameter"; break; + case 178: s = "invalid QSep"; break; default: s = "error " + n; break; } diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index 97b05c8ab..2b39073ee 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -220,8 +220,8 @@ public override int Read() { public class Scanner { const char EOL = '\n'; const int eofSym = 0; /* pdt */ - const int maxT = 125; - const int noSym = 125; + const int maxT = 126; + const int noSym = 126; [ContractInvariantMethod] @@ -515,74 +515,75 @@ void CheckLiteral() { switch (t.val) { case "yield": t.kind = 8; break; case "var": t.kind = 9; break; - case "where": t.kind = 15; break; - case "int": t.kind = 16; break; - case "real": t.kind = 17; break; - case "bool": t.kind = 18; break; - case "const": t.kind = 23; break; - case "unique": t.kind = 24; break; - case "uses": t.kind = 25; break; - case "revealed": t.kind = 28; break; - case "function": t.kind = 29; break; - case "returns": t.kind = 30; break; - case "hideable": t.kind = 31; break; - case "axiom": t.kind = 32; break; - case "type": t.kind = 33; break; - case "datatype": t.kind = 35; break; - case "invariant": t.kind = 36; break; - case "pure": t.kind = 37; break; - case "async": t.kind = 38; break; - case "action": t.kind = 39; break; - case "creates": t.kind = 40; break; - case "refines": t.kind = 41; break; - case "using": t.kind = 42; break; - case "left": t.kind = 43; break; - case "right": t.kind = 44; break; - case "both": t.kind = 45; break; - case "atomic": t.kind = 46; break; - case "procedure": t.kind = 47; break; - case "asserts": t.kind = 48; break; - case "requires": t.kind = 49; break; - case "ensures": t.kind = 50; break; - case "preserves": t.kind = 51; break; - case "implementation": t.kind = 52; break; - case "free": t.kind = 53; break; - case "modifies": t.kind = 54; break; - case "goto": t.kind = 55; break; - case "return": t.kind = 56; break; - case "if": t.kind = 57; break; - case "else": t.kind = 58; break; - case "while": t.kind = 59; break; - case "break": t.kind = 61; break; - case "reveal": t.kind = 62; break; - case "hide": t.kind = 63; break; - case "pop": t.kind = 64; break; - case "push": t.kind = 65; break; - case "assert": t.kind = 66; break; - case "assume": t.kind = 67; break; - case "havoc": t.kind = 68; break; - case "call": t.kind = 71; break; - case "par": t.kind = 72; break; - case "div": t.kind = 94; break; - case "mod": t.kind = 95; break; - case "is": t.kind = 98; break; - case "false": t.kind = 101; break; - case "true": t.kind = 102; break; - case "roundNearestTiesToEven": t.kind = 103; break; - case "RNE": t.kind = 104; break; - case "roundNearestTiesToAway": t.kind = 105; break; - case "RNA": t.kind = 106; break; - case "roundTowardPositive": t.kind = 107; break; - case "RTP": t.kind = 108; break; - case "roundTowardNegative": t.kind = 109; break; - case "RTN": t.kind = 110; break; - case "roundTowardZero": t.kind = 111; break; - case "RTZ": t.kind = 112; break; - case "old": t.kind = 113; break; - case "then": t.kind = 116; break; - case "forall": t.kind = 117; break; - case "exists": t.kind = 119; break; - case "lambda": t.kind = 121; break; + case "monotonic": t.kind = 11; break; + case "where": t.kind = 16; break; + case "int": t.kind = 17; break; + case "real": t.kind = 18; break; + case "bool": t.kind = 19; break; + case "const": t.kind = 24; break; + case "unique": t.kind = 25; break; + case "uses": t.kind = 26; break; + case "revealed": t.kind = 29; break; + case "function": t.kind = 30; break; + case "returns": t.kind = 31; break; + case "hideable": t.kind = 32; break; + case "axiom": t.kind = 33; break; + case "type": t.kind = 34; break; + case "datatype": t.kind = 36; break; + case "invariant": t.kind = 37; break; + case "pure": t.kind = 38; break; + case "async": t.kind = 39; break; + case "action": t.kind = 40; break; + case "creates": t.kind = 41; break; + case "refines": t.kind = 42; break; + case "using": t.kind = 43; break; + case "left": t.kind = 44; break; + case "right": t.kind = 45; break; + case "both": t.kind = 46; break; + case "atomic": t.kind = 47; break; + case "procedure": t.kind = 48; break; + case "asserts": t.kind = 49; break; + case "requires": t.kind = 50; break; + case "ensures": t.kind = 51; break; + case "preserves": t.kind = 52; break; + case "implementation": t.kind = 53; break; + case "free": t.kind = 54; break; + case "modifies": t.kind = 55; break; + case "goto": t.kind = 56; break; + case "return": t.kind = 57; break; + case "if": t.kind = 58; break; + case "else": t.kind = 59; break; + case "while": t.kind = 60; break; + case "break": t.kind = 62; break; + case "reveal": t.kind = 63; break; + case "hide": t.kind = 64; break; + case "pop": t.kind = 65; break; + case "push": t.kind = 66; break; + case "assert": t.kind = 67; break; + case "assume": t.kind = 68; break; + case "havoc": t.kind = 69; break; + case "call": t.kind = 72; break; + case "par": t.kind = 73; break; + case "div": t.kind = 95; break; + case "mod": t.kind = 96; break; + case "is": t.kind = 99; break; + case "false": t.kind = 102; break; + case "true": t.kind = 103; break; + case "roundNearestTiesToEven": t.kind = 104; break; + case "RNE": t.kind = 105; break; + case "roundNearestTiesToAway": t.kind = 106; break; + case "RNA": t.kind = 107; break; + case "roundTowardPositive": t.kind = 108; break; + case "RTP": t.kind = 109; break; + case "roundTowardNegative": t.kind = 110; break; + case "RTN": t.kind = 111; break; + case "roundTowardZero": t.kind = 112; break; + case "RTZ": t.kind = 113; break; + case "old": t.kind = 114; break; + case "then": t.kind = 117; break; + case "forall": t.kind = 118; break; + case "exists": t.kind = 120; break; + case "lambda": t.kind = 122; break; default: break; } } @@ -854,129 +855,129 @@ void CheckLiteral() { case 61: {t.kind = 10; break;} case 62: - {t.kind = 11; break;} - case 63: {t.kind = 12; break;} + case 63: + {t.kind = 13; break;} case 64: - {t.kind = 14; break;} + {t.kind = 15; break;} case 65: - {t.kind = 19; break;} - case 66: {t.kind = 20; break;} + case 66: + {t.kind = 21; break;} case 67: - {t.kind = 26; break;} + {t.kind = 27; break;} case 68: - {t.kind = 69; break;} - case 69: {t.kind = 70; break;} + case 69: + {t.kind = 71; break;} case 70: - {t.kind = 74; break;} - case 71: {t.kind = 75; break;} - case 72: + case 71: {t.kind = 76; break;} - case 73: + case 72: {t.kind = 77; break;} + case 73: + {t.kind = 78; break;} case 74: - {t.kind = 79; break;} + {t.kind = 80; break;} case 75: if (ch == '&') {AddCh(); goto case 76;} else {goto case 0;} case 76: - {t.kind = 80; break;} - case 77: {t.kind = 81; break;} - case 78: + case 77: {t.kind = 82; break;} - case 79: + case 78: {t.kind = 83; break;} + case 79: + {t.kind = 84; break;} case 80: - {t.kind = 86; break;} - case 81: {t.kind = 87; break;} - case 82: + case 81: {t.kind = 88; break;} - case 83: + case 82: {t.kind = 89; break;} - case 84: + case 83: {t.kind = 90; break;} - case 85: + case 84: {t.kind = 91; break;} + case 85: + {t.kind = 92; break;} case 86: - {t.kind = 96; break;} - case 87: {t.kind = 97; break;} + case 87: + {t.kind = 98; break;} case 88: - {t.kind = 100; break;} + {t.kind = 101; break;} case 89: - {t.kind = 114; break;} - case 90: {t.kind = 115; break;} + case 90: + {t.kind = 116; break;} case 91: - {t.kind = 118; break;} + {t.kind = 119; break;} case 92: - {t.kind = 120; break;} + {t.kind = 121; break;} case 93: - {t.kind = 122; break;} - case 94: {t.kind = 123; break;} - case 95: + case 94: {t.kind = 124; break;} + case 95: + {t.kind = 125; break;} case 96: - recEnd = pos; recKind = 93; + recEnd = pos; recKind = 94; if (ch == '0') {AddCh(); goto case 16;} else if (ch == '>') {AddCh(); goto case 69;} - else {t.kind = 93; break;} + else {t.kind = 94; break;} case 97: - recEnd = pos; recKind = 13; + recEnd = pos; recKind = 14; if (ch == '=') {AddCh(); goto case 68;} else if (ch == ':') {AddCh(); goto case 94;} - else {t.kind = 13; break;} + else {t.kind = 14; break;} case 98: - recEnd = pos; recKind = 21; + recEnd = pos; recKind = 22; if (ch == '=') {AddCh(); goto case 106;} - else {t.kind = 21; break;} + else {t.kind = 22; break;} case 99: - recEnd = pos; recKind = 22; + recEnd = pos; recKind = 23; if (ch == '=') {AddCh(); goto case 80;} - else {t.kind = 22; break;} + else {t.kind = 23; break;} case 100: - recEnd = pos; recKind = 27; + recEnd = pos; recKind = 28; if (ch == '|') {AddCh(); goto case 90;} - else {t.kind = 27; break;} + else {t.kind = 28; break;} case 101: - recEnd = pos; recKind = 34; + recEnd = pos; recKind = 35; if (ch == '=') {AddCh(); goto case 107;} - else {t.kind = 34; break;} + else {t.kind = 35; break;} case 102: - recEnd = pos; recKind = 60; + recEnd = pos; recKind = 61; if (ch == '*') {AddCh(); goto case 87;} - else {t.kind = 60; break;} + else {t.kind = 61; break;} case 103: - recEnd = pos; recKind = 73; + recEnd = pos; recKind = 74; if (ch == '|') {AddCh(); goto case 78;} else if (ch == '{') {AddCh(); goto case 89;} - else {t.kind = 73; break;} + else {t.kind = 74; break;} case 104: - recEnd = pos; recKind = 99; + recEnd = pos; recKind = 100; if (ch == '=') {AddCh(); goto case 81;} - else {t.kind = 99; break;} + else {t.kind = 100; break;} case 105: - recEnd = pos; recKind = 92; + recEnd = pos; recKind = 93; if (ch == '+') {AddCh(); goto case 85;} - else {t.kind = 92; break;} + else {t.kind = 93; break;} case 106: - recEnd = pos; recKind = 85; + recEnd = pos; recKind = 86; if (ch == '=') {AddCh(); goto case 108;} - else {t.kind = 85; break;} + else {t.kind = 86; break;} case 107: - recEnd = pos; recKind = 84; + recEnd = pos; recKind = 85; if (ch == '>') {AddCh(); goto case 72;} - else {t.kind = 84; break;} + else {t.kind = 85; break;} case 108: - recEnd = pos; recKind = 78; + recEnd = pos; recKind = 79; if (ch == '>') {AddCh(); goto case 70;} - else {t.kind = 78; break;} + else {t.kind = 79; break;} } t.val = new String(tval, 0, tlen); diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 0c72da8df..4da7032d6 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -523,7 +523,7 @@ public virtual Cmd VisitHavocCmd(HavocCmd node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); - node.Vars = this.VisitIdentifierExprSeq(node.Vars); + node.VarsIncludingMonotonic = this.VisitIdentifierExprSeq(node.VarsIncludingMonotonic); return node; } @@ -1395,7 +1395,7 @@ public override GotoCmd VisitGotoCmd(GotoCmd node) public override Cmd VisitHavocCmd(HavocCmd node) { Contract.Ensures(Contract.Result() == node); - this.VisitIdentifierExprSeq(node.Vars); + this.VisitIdentifierExprSeq(node.VarsIncludingMonotonic); return node; } diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index d81beeac1..f85051060 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.2.5 + 3.2.6 net6.0 false Boogie diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a69166cb7..4c8bf88c4 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1369,7 +1369,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing // We do not need to havoc it if we have performed a modular proof of the loop (i.e., using only the loop // invariant) in the previous snapshot and, consequently, the corresponding assumption did not affect the // anything after the loop. We can achieve this by simply not updating/adding it in the incarnation map. - List havocVars = hc.Vars.Where(v => + var havocVars = hc.Vars.Where(v => !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##cached##"))) .ToList(); // First, compute the new incarnations diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index c8bf280c3..b4f2453bf 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -741,16 +741,14 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary prefixOfPredicateCmdsInit = new List(); - List prefixOfPredicateCmdsMaintained = new List(); + var prefixOfPredicateCmdsInit = new List(); + var prefixOfPredicateCmdsMaintained = new List(); for (int i = 0, n = header.Cmds.Count; i < n; i++) { - PredicateCmd predicateCmd = header.Cmds[i] as PredicateCmd; - if (predicateCmd != null) + if (header.Cmds[i] is PredicateCmd predicateCmd) { - if (predicateCmd is AssertCmd) + if (predicateCmd is AssertCmd assertCmd) { - AssertCmd assertCmd = (AssertCmd)predicateCmd; AssertCmd initAssertCmd = null; if (Options.ConcurrentHoudini) @@ -938,23 +936,19 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary varsToHavoc = VarsAssignedInLoop(g, header); - List havocExprs = new List(); - foreach (Variable v in varsToHavoc) + var varsToHavoc = VarsAssignedInLoop(g, header); + var havocExprs = new HashSet(); + foreach (var variable in varsToHavoc) { - Contract.Assert(v != null); - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - if (!havocExprs.Contains(ie)) - { - havocExprs.Add(ie); - } + Contract.Assert(variable != null); + var ie = new IdentifierExpr(Token.NoToken, variable); + havocExprs.Add(ie); } // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct // the source location for this later on - HavocCmd hc = new HavocCmd(header.tok, havocExprs); - List newCmds = new List(); - newCmds.Add(hc); + var hc = new HavocCmd(header.tok, havocExprs.ToList()); + List newCmds = new List { hc }; foreach (Cmd c in header.Cmds) { newCmds.Add(c); @@ -1073,22 +1067,18 @@ private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary varsToHavoc = VarsAssignedInLoop(g, header); - List havocExprs = new List(); + var havocExprs = new HashSet(); foreach (Variable v in varsToHavoc) { Contract.Assert(v != null); - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - if (!havocExprs.Contains(ie)) - { - havocExprs.Add(ie); - } + var ie = new IdentifierExpr(Token.NoToken, v); + havocExprs.Add(ie); } // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct // the source location for this later on - HavocCmd hc = new HavocCmd(newHeader.tok, havocExprs); - List havocCmds = new List(); - havocCmds.Add(hc); + HavocCmd hc = new HavocCmd(newHeader.tok, havocExprs.ToList()); + List havocCmds = new List { hc }; Block havocBlock = new Block(newHeader.tok, newHeader.Label + "_havoc", havocCmds, new GotoCmd(newHeader.tok, new List { newHeader })); diff --git a/Test/ast/locals.bpl b/Test/ast/locals.bpl new file mode 100644 index 000000000..d155b3ca9 --- /dev/null +++ b/Test/ast/locals.bpl @@ -0,0 +1,16 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure MonotonicIsNotHavoced() +{ + var x: int; + monotonic var assigned: bool; + x := 5; + assigned := true; + while (x > 0) + { + x := x - 1; + assigned := true; + } + assert assigned; +} \ No newline at end of file diff --git a/Test/ast/locals.bpl.expect b/Test/ast/locals.bpl.expect new file mode 100644 index 000000000..37fad75c9 --- /dev/null +++ b/Test/ast/locals.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors