summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-23 12:07:20 -0800
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-23 12:07:20 -0800
commitc5c2c9465a53e4b35a20ad5efe73882dc6a5af34 (patch)
tree9336173498839860956d21178bbf622d1bc22e77
parentc7f74de7fae661883ca13bb09d557272de659e03 (diff)
removed call forall and * args to calls
Diffstat
-rw-r--r--Source/Core/AbsyCmd.cs313
-rw-r--r--Source/Core/BoogiePL.atg100
-rw-r--r--Source/Core/Duplicator.cs8
-rw-r--r--Source/Core/Parser.cs591
-rw-r--r--Source/Core/Scanner.cs104
-rw-r--r--Source/Core/StandardVisitor.cs22
-rw-r--r--Source/VCExpr/Boogie2VCExpr.cs6
-rw-r--r--Test/test0/Answer5
-rw-r--r--Test/test0/EmptyCallArgs.bpl13
-rw-r--r--Test/test1/Answer10
-rw-r--r--Test/test1/CallForallResolve.bpl23
-rw-r--r--Test/test1/EmptyCallArgs.bpl11
-rw-r--r--Test/test1/runtest.bat1
-rw-r--r--Test/test2/Answer33
-rw-r--r--Test/test2/CallForall.bpl134
-rw-r--r--Test/test2/FreeCall.bpl14
-rw-r--r--Test/test2/runtest.bat2
-rw-r--r--Test/test20/Answer3
-rw-r--r--Test/test20/PolyProcs0.bpl11
19 files changed, 409 insertions, 995 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 1220d812..af06b391 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1627,6 +1627,19 @@ namespace Microsoft.Boogie {
}
}
+ private bool isAsync = false;
+ public bool IsAsync
+ {
+ get
+ {
+ return isAsync;
+ }
+ set
+ {
+ isAsync = value;
+ }
+ }
+
protected CallCommonality(IToken tok, QKeyValue kv)
: base(tok) {
Contract.Requires(tok != null);
@@ -2170,265 +2183,6 @@ namespace Microsoft.Boogie {
}
}
- public class CallForallCmd : CallCommonality {
- string/*!*/ callee;
- public Procedure Proc;
- public List<Expr>/*!*/ Ins;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(callee != null);
- Contract.Invariant(Ins != null);
- }
-
-
- // the types of the formal in-parameters after instantiating all
- // type variables whose value could be inferred using the given
- // actual non-wildcard arguments
- public TypeSeq InstantiatedTypes;
-
- public CallForallCmd(IToken tok, string callee, List<Expr> ins)
- : base(tok, null) {
- Contract.Requires(ins != null);
- Contract.Requires(callee != null);
- Contract.Requires(tok != null);
- this.callee = callee;
- this.Ins = ins;
- }
- public CallForallCmd(IToken tok, string callee, List<Expr> ins, QKeyValue kv)
- : base(tok, kv) {
- Contract.Requires(ins != null);
- Contract.Requires(callee != null);
- Contract.Requires(tok != null);
- this.callee = callee;
- this.Ins = ins;
- }
- public override void Emit(TokenTextWriter stream, int level) {
- //Contract.Requires(stream != null);
- stream.Write(this, level, "");
- if (IsFree) {
- stream.Write("free ");
- }
- stream.Write("call ");
- EmitAttributes(stream, Attributes);
- stream.Write("forall ");
- stream.Write(TokenTextWriter.SanitizeIdentifier(callee));
- stream.Write("(");
- string sep = "";
- foreach (Expr arg in Ins) {
- stream.Write(sep);
- sep = ", ";
- if (arg == null) {
- stream.Write("*");
- } else {
- arg.Emit(stream);
- }
- }
- stream.WriteLine(");");
- base.Emit(stream, level);
- }
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- if (Proc != null) {
- // already resolved
- return;
- }
- ResolveAttributes(Attributes, rc);
- Proc = rc.LookUpProcedure(callee) as Procedure;
- if (Proc == null) {
- rc.Error(this, "call to undeclared procedure: {0}", callee);
- }
- foreach (Expr e in Ins) {
- if (e != null) {
- e.Resolve(rc);
- }
- }
- }
- public override void AddAssignedVariables(VariableSeq vars) {
- //Contract.Requires(vars != null);
- }
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- TypecheckAttributes(Attributes, tc);
- // typecheck in-parameters
- foreach (Expr e in Ins) {
- if (e != null) {
- e.Typecheck(tc);
- }
- }
-
- if (this.Proc == null) {
- // called procedure didn't resolve, so bug out
- return;
- }
-
- // match actuals with formals
- if (Ins.Count != Proc.InParams.Length) {
- tc.Error(this, "wrong number of in-parameters in call: {0}", callee);
- } else {
- // determine the lists of formal and actual arguments that need
- // to be matched (stars are left out)
- TypeSeq/*!*/ formalTypes = new TypeSeq();
- ExprSeq/*!*/ actualArgs = new ExprSeq();
- for (int i = 0; i < Ins.Count; i++)
- if (Ins[i] != null) {
- formalTypes.Add(cce.NonNull(Proc.InParams[i]).TypedIdent.Type);
- actualArgs.Add(Ins[i]);
- }
- IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst =
- Type.MatchArgumentTypes(Proc.TypeParameters,
- formalTypes, actualArgs, null, null,
- "call forall to " + callee, tc);
- Contract.Assert(cce.NonNullDictionaryAndValues(subst));
-
- InstantiatedTypes = new TypeSeq();
- foreach (Variable/*!*/ var in Proc.InParams) {
- Contract.Assert(var != null);
- InstantiatedTypes.Add(var.TypedIdent.Type.Substitute(subst));
- }
- }
-
- // if (Proc.OutParams.Length != 0)
- // {
- // tc.Error(this, "call forall is allowed only on procedures with no out-parameters: {0}", callee);
- // }
-
- if (Proc.Modifies.Length != 0) {
- tc.Error(this, "call forall is allowed only on procedures with no modifies clause: {0}", callee);
- }
- }
-
- protected override Cmd ComputeDesugaring() {
- Contract.Ensures(Contract.Result<Cmd>() != null);
- CmdSeq newBlockBody = new CmdSeq();
- Hashtable /*Variable -> Expr*/ substMap = new Hashtable/*Variable -> Expr*/();
- VariableSeq/*!*/ tempVars = new VariableSeq();
-
- // proc P(ins) returns ()
- // requires Pre;
- // //modifies ;
- // ensures Post;
- //
- // call forall P(ains);
-
- // ins : formal in-parameters of procedure
- // ains : actual in-arguments passed to call
- // cins : new variables created just for this call, one per ains
- // wildcardVars : the bound variables to be wrapped up in a quantification
-
- #region Create cins; each one is an incarnation of the corresponding in parameter
- VariableSeq cins = new VariableSeq();
- VariableSeq wildcardVars = new VariableSeq();
- Contract.Assume(this.Proc != null);
- for (int i = 0, n = this.Proc.InParams.Length; i < n; i++) {
- Variable param = cce.NonNull(this.Proc.InParams[i]);
- Type/*!*/ paramType = cce.NonNull(this.InstantiatedTypes)[i]; // might contain type variables
- bool isWildcard = this.Ins[i] == null;
- Variable cin = CreateTemporaryVariable(tempVars, param, paramType,
- isWildcard ? TempVarKind.Bound : TempVarKind.Formal);
- if (isWildcard) {
- cins.Add(null);
- wildcardVars.Add(cin);
- } else {
- cins.Add(cin);
- }
- IdentifierExpr ie = new IdentifierExpr(cin.tok, cin);
- substMap.Add(param, ie);
- }
- #endregion
-
- #region call forall P(ains) becomes: (open outlining one level to see)
- #region cins := ains
- for (int i = 0, n = this.Ins.Count; i < n; i++) {
- if (this.Ins[i] != null) {
- IdentifierExpr/*!*/ cin_exp = new IdentifierExpr(cce.NonNull(cins[i]).tok, cce.NonNull(cins[i]));
- AssignCmd assign = Cmd.SimpleAssign(Token.NoToken, cin_exp, cce.NonNull(this.Ins[i]));
- newBlockBody.Add(assign);
- }
- }
- #endregion
-
- #region assert Pre[ins := cins]
- Substitution s = Substituter.SubstitutionFromHashtable(substMap);
- Expr preConjunction = null;
- for (int i = 0; i < this.Proc.Requires.Length; i++) {
- Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);
- if (!req.Free && !IsFree) {
- Expr pre = Substituter.Apply(s, req.Condition);
- if (preConjunction == null) {
- preConjunction = pre;
- } else {
- preConjunction = Expr.And(preConjunction, pre);
- }
- }
- }
- if (preConjunction == null) {
- preConjunction = Expr.True;
- }
- #endregion
-
- #region Create couts
- VariableSeq/*!*/ couts = new VariableSeq();
- foreach (Variable/*!*/ param in this.Proc.OutParams) {
- Contract.Assert(param != null);
- Variable cout = CreateTemporaryVariable(tempVars, param,
- param.TypedIdent.Type, TempVarKind.Bound);
- couts.Add(cout);
- IdentifierExpr ie = new IdentifierExpr(cout.tok, cout);
- substMap.Add(param, ie);
- }
- // add the where clauses, now that we have the entire substitution map
- foreach (Variable/*!*/ param in this.Proc.OutParams) {
- Contract.Assert(param != null);
- Expr w = param.TypedIdent.WhereExpr;
- if (w != null) {
- IdentifierExpr ie = (IdentifierExpr)cce.NonNull(substMap[param]);
- Contract.Assert(ie.Decl != null);
- ie.Decl.TypedIdent.WhereExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(substMap), w);
- }
- }
- #endregion
-
- #region assume Post[ins := cins]
- s = Substituter.SubstitutionFromHashtable(substMap);
- Expr postConjunction = null;
- foreach (Ensures/*!*/ e in this.Proc.Ensures) {
- Contract.Assert(e != null);
- Expr post = Substituter.Apply(s, e.Condition);
- if (postConjunction == null) {
- postConjunction = post;
- } else {
- postConjunction = Expr.And(postConjunction, post);
- }
- }
- if (postConjunction == null) {
- postConjunction = Expr.True;
- }
- #endregion
-
- #region assume (forall wildcardVars :: Pre ==> Post);
- Expr body = postConjunction;
- if (couts.Length > 0) {
- body = new ExistsExpr(tok, couts, body);
- }
- body = Expr.Imp(preConjunction, body);
- if (wildcardVars.Length != 0) {
- TypeVariableSeq/*!*/ typeParams = Type.FreeVariablesIn(cce.NonNull(InstantiatedTypes));
- body = new ForallExpr(tok, typeParams, wildcardVars, body);
- }
- newBlockBody.Add(new AssumeCmd(tok, body));
- #endregion
- #endregion
-
- return new StateCmd(this.tok, tempVars, newBlockBody);
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitCallForallCmd(this);
- }
- }
-
public abstract class PredicateCmd : Cmd {
public QKeyValue Attributes;
public /*readonly--except in StandardVisitor*/ Expr/*!*/ Expr;
@@ -2721,6 +2475,47 @@ namespace Microsoft.Boogie {
}
}
+ public class YieldCmd : PredicateCmd
+ {
+ public YieldCmd(IToken/*!*/ tok, Expr/*!*/ expr)
+ : base(tok, expr)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
+ }
+ public YieldCmd(IToken/*!*/ tok, Expr/*!*/ expr, QKeyValue kv)
+ : base(tok, expr, kv)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
+ }
+ public override void Emit(TokenTextWriter stream, int level)
+ {
+ //Contract.Requires(stream != null);
+ stream.Write(this, level, "assume ");
+ EmitAttributes(stream, Attributes);
+ this.Expr.Emit(stream);
+ stream.WriteLine(";");
+ }
+ public override void Typecheck(TypecheckingContext tc)
+ {
+ //Contract.Requires(tc != null);
+ Expr.Typecheck(tc);
+ Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition
+ if (!Expr.Type.Unify(Type.Bool))
+ {
+ tc.Error(this, "an assumed expression must be of type bool (got: {0})", Expr.Type);
+ }
+ }
+
+ public override Absy StdDispatch(StandardVisitor visitor)
+ {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+ return visitor.VisitYieldCmd(this);
+ }
+ }
+
public class ReturnExprCmd : ReturnCmd {
public Expr/*!*/ Expr;
[ContractInvariantMethod]
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index bf76df14..67c7fd9a 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -103,7 +103,7 @@ private class BvBounds : Expr {
this.Lower = lower;
this.Upper = upper;
}
- public override Type/*!*/ ShallowType { get {Contract.Ensures(Contract.Result<Type>() != null); return Bpl.Type.Int; } }
+ public override Bpl.Type/*!*/ ShallowType { get {Contract.Ensures(Contract.Result<Bpl.Type>() != null); return Bpl.Type.Int; } }
public override void Resolve(ResolutionContext/*!*/ rc) {
// Contract.Requires(rc != null);
rc.Error(this, "bitvector bounds in illegal position");
@@ -313,7 +313,7 @@ Type<out Bpl.Type/*!*/ ty>
.
TypeArgs<TypeSeq/*!*/ ts>
-= (.Contract.Requires(ts != null); IToken/*!*/ tok; Type/*!*/ ty; .)
+= (.Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; .)
(
TypeAtom<out ty> (. ts.Add(ty); .)
[ TypeArgs<ts> ]
@@ -343,7 +343,7 @@ MapType<out Bpl.Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null;
IToken/*!*/ nnTok;
TypeSeq/*!*/ arguments = new TypeSeq();
- Type/*!*/ result;
+ Bpl.Type/*!*/ result;
TypeVariableSeq/*!*/ typeParameters = new TypeVariableSeq();
.)
[ TypeParams<out nnTok, out typeParameters> (. tok = nnTok; .) ]
@@ -447,7 +447,7 @@ Function<out DeclarationSeq/*!*/ ds>
var arguments = new VariableSeq();
TypedIdent/*!*/ tyd;
TypedIdent retTyd = null;
- Type/*!*/ retTy;
+ Bpl.Type/*!*/ retTy;
QKeyValue argKv = null;
QKeyValue kv = null;
Expr definition = null;
@@ -484,7 +484,7 @@ Function<out DeclarationSeq/*!*/ ds>
}
}
if (!allUnnamed) {
- Type prevType = null;
+ Bpl.Type prevType = null;
for (int i = arguments.Length; 0 <= --i; ) {
TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;
if (curr.HasName) {
@@ -496,7 +496,7 @@ Function<out DeclarationSeq/*!*/ ds>
this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");
break;
}
- Type ty = curr.Type;
+ Bpl.Type ty = curr.Type;
var uti = ty as UnresolvedTypeIdentifier;
if (uti != null && uti.Arguments.Length == 0) {
// the given "thing" was just an identifier, so let's use it as the name of the parameter
@@ -562,7 +562,7 @@ UserDefinedTypes<.out List<Declaration/*!*/>/*!*/ ts.>
UserDefinedType<out Declaration/*!*/ decl, QKeyValue kv>
= (. Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; TokenSeq/*!*/ paramTokens = new TokenSeq ();
- Type/*!*/ body = dummyType; bool synonym = false; .)
+ Bpl.Type/*!*/ body = dummyType; bool synonym = false; .)
Ident<out id>
[ WhiteSpaceIdents<out paramTokens> ]
[
@@ -855,6 +855,10 @@ LabelOrCmd<out Cmd c, out IToken label>
{ Attribute<ref kv> }
Proposition<out e> (. c = new AssumeCmd(x, e, kv); .)
";"
+ | "yield" (. x = t; .)
+ { Attribute<ref kv> }
+ Proposition<out e> (. c = new YieldCmd(x, e, kv); .)
+ ";"
| "havoc" (. x = t; .)
Idents<out xs> ";" (. ids = new IdentifierExprSeq();
foreach(IToken/*!*/ y in xs){
@@ -927,92 +931,34 @@ CallCmd<out Cmd/*!*/ c>
Expr en; List<Expr> args;
c = dummyCmd;
bool isFree = false;
+ bool isAsync = false;
.)
+ [ "async" (. isAsync = true; .)
+ ]
[ "free" (. isFree = true; .)
]
"call" (. x = t; .)
{ Attribute<ref kv> }
( Ident<out first>
( "("
- [ CallForallArg<out en> (. es.Add(en); .)
- { "," CallForallArg<out en> (. es.Add(en); .)
+ [ Expression<out en> (. es.Add(en); .)
+ { "," Expression<out en> (. es.Add(en); .)
}
]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
|
(. ids.Add(new IdentifierExpr(first, first.val)); .)
- [ "," CallOutIdent<out p> (.
- if (p==null) {
- ids.Add(null);
- } else {
- ids.Add(new IdentifierExpr(p, p.val));
- }
- .)
- { "," CallOutIdent<out p> (.
- if (p==null) {
- ids.Add(null);
- } else {
- ids.Add(new IdentifierExpr(p, p.val));
- }
- .)
+ [ "," Ident<out p> (. ids.Add(new IdentifierExpr(p, p.val)); .)
+ { "," Ident<out p> (. ids.Add(new IdentifierExpr(p, p.val)); .)
}
] ":="
Ident<out first> "("
- [ CallForallArg<out en> (. es.Add(en); .)
- { "," CallForallArg<out en> (. es.Add(en); .)
+ [ Expression<out en> (. es.Add(en); .)
+ { "," Expression<out en> (. es.Add(en); .)
}
]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
)
- | "forall"
- Ident<out first> "(" (. args = new List<Expr>(); .)
- [ CallForallArg<out en> (. args.Add(en); .)
- { "," CallForallArg<out en> (. args.Add(en); .)
- }
- ]
- ")" (. c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree; .)
- | "*"
- (. ids.Add(null); .)
- [ "," CallOutIdent<out p> (.
- if (p==null) {
- ids.Add(null);
- } else {
- ids.Add(new IdentifierExpr(p, p.val));
- }
- .)
- { "," CallOutIdent<out p> (.
- if (p==null) {
- ids.Add(null);
- } else {
- ids.Add(new IdentifierExpr(p, p.val));
- }
- .)
- }
- ] ":="
- Ident<out first> "("
- [ CallForallArg<out en> (. es.Add(en); .)
- { "," CallForallArg<out en> (. es.Add(en); .)
- }
- ]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; .)
- )
- .
-
-CallOutIdent<out IToken id>
-= (. id = null;
- IToken/*!*/ p;
- .)
- ( "*"
- | Ident<out p> (. id = p; .)
- )
- .
-
-CallForallArg<out Expr exprOptional>
-= (. exprOptional = null;
- Expr/*!*/ e;
- .)
- ( "*"
- | Expression<out e> (. exprOptional = e; .)
)
.
@@ -1214,7 +1160,7 @@ NegOp = "!" | '\u00ac'.
CoercionExpression<out Expr/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
- Type/*!*/ coercedTo;
+ Bpl.Type/*!*/ coercedTo;
BigNum bn;
.)
ArrayExpression<out e>
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 36f54402..fe189f83 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -113,14 +113,6 @@ namespace Microsoft.Boogie {
clone.Outs = new List<IdentifierExpr>(clone.Outs);
return base.VisitCallCmd(clone);
}
- public override Cmd VisitCallForallCmd(CallForallCmd node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- CallForallCmd/*!*/ clone = (CallForallCmd)node.Clone();
- Contract.Assert(clone != null);
- clone.Ins = new List<Expr>(clone.Ins);
- return base.VisitCallForallCmd(clone);
- }
public override Choice VisitChoice(Choice node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Choice>() != null);
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 5810fe49..a6af2c45 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -25,7 +25,7 @@ public class Parser {
public const int _string = 4;
public const int _decimal = 5;
public const int _float = 6;
- public const int maxT = 92;
+ public const int maxT = 94;
const bool T = true;
const bool x = false;
@@ -123,7 +123,7 @@ private class BvBounds : Expr {
this.Lower = lower;
this.Upper = upper;
}
- public override Type/*!*/ ShallowType { get {Contract.Ensures(Contract.Result<Type>() != null); return Bpl.Type.Int; } }
+ public override Bpl.Type/*!*/ ShallowType { get {Contract.Ensures(Contract.Result<Bpl.Type>() != null); return Bpl.Type.Int; } }
public override void Resolve(ResolutionContext/*!*/ rc) {
// Contract.Requires(rc != null);
rc.Error(this, "bitvector bounds in illegal position");
@@ -328,7 +328,7 @@ private class BvBounds : Expr {
var arguments = new VariableSeq();
TypedIdent/*!*/ tyd;
TypedIdent retTyd = null;
- Type/*!*/ retTy;
+ Bpl.Type/*!*/ retTy;
QKeyValue argKv = null;
QKeyValue kv = null;
Expr definition = null;
@@ -363,7 +363,7 @@ private class BvBounds : Expr {
Get();
Type(out retTy);
retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy);
- } else SynErr(93);
+ } else SynErr(95);
if (la.kind == 27) {
Get();
Expression(out tmp);
@@ -371,7 +371,7 @@ private class BvBounds : Expr {
Expect(28);
} else if (la.kind == 8) {
Get();
- } else SynErr(94);
+ } else SynErr(96);
if (retTyd == null) {
// construct a dummy type for the case of syntax error
retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
@@ -389,7 +389,7 @@ private class BvBounds : Expr {
}
}
if (!allUnnamed) {
- Type prevType = null;
+ Bpl.Type prevType = null;
for (int i = arguments.Length; 0 <= --i; ) {
TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;
if (curr.HasName) {
@@ -401,7 +401,7 @@ private class BvBounds : Expr {
this.errors.SemErr(curr.tok, "the type of the last parameter is unspecified");
break;
}
- Type ty = curr.Type;
+ Bpl.Type ty = curr.Type;
var uti = ty as UnresolvedTypeIdentifier;
if (uti != null && uti.Arguments.Length == 0) {
// the given "thing" was just an identifier, so let's use it as the name of the parameter
@@ -494,7 +494,7 @@ private class BvBounds : Expr {
impl = new Implementation(x, x.val, typeParams,
Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
- } else SynErr(95);
+ } else SynErr(97);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
}
@@ -606,7 +606,7 @@ private class BvBounds : Expr {
ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
} else if (la.kind == 17 || la.kind == 19) {
MapType(out ty);
- } else SynErr(96);
+ } else SynErr(98);
}
void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
@@ -647,7 +647,7 @@ private class BvBounds : Expr {
void Expression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
ImpliesExpression(false, out e0);
- while (la.kind == 52 || la.kind == 53) {
+ while (la.kind == 53 || la.kind == 54) {
EquivOp();
x = t;
ImpliesExpression(false, out e1);
@@ -670,7 +670,7 @@ private class BvBounds : Expr {
Get();
Type(out ty);
Expect(10);
- } else SynErr(97);
+ } else SynErr(99);
}
void Ident(out IToken/*!*/ x) {
@@ -683,7 +683,7 @@ private class BvBounds : Expr {
}
void TypeArgs(TypeSeq/*!*/ ts) {
- Contract.Requires(ts != null); IToken/*!*/ tok; Type/*!*/ ty;
+ Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty;
if (StartOf(5)) {
TypeAtom(out ty);
ts.Add(ty);
@@ -700,14 +700,14 @@ private class BvBounds : Expr {
} else if (la.kind == 17 || la.kind == 19) {
MapType(out ty);
ts.Add(ty);
- } else SynErr(98);
+ } else SynErr(100);
}
void MapType(out Bpl.Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null;
IToken/*!*/ nnTok;
TypeSeq/*!*/ arguments = new TypeSeq();
- Type/*!*/ result;
+ Bpl.Type/*!*/ result;
TypeVariableSeq/*!*/ typeParameters = new TypeVariableSeq();
if (la.kind == 19) {
@@ -816,7 +816,7 @@ private class BvBounds : Expr {
void UserDefinedType(out Declaration/*!*/ decl, QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; TokenSeq/*!*/ paramTokens = new TokenSeq ();
- Type/*!*/ body = dummyType; bool synonym = false;
+ Bpl.Type/*!*/ body = dummyType; bool synonym = false;
Ident(out id);
if (la.kind == 1) {
WhiteSpaceIdents(out paramTokens);
@@ -885,7 +885,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
SpecPrePost(true, pre, post);
} else if (la.kind == 36 || la.kind == 37) {
SpecPrePost(false, pre, post);
- } else SynErr(99);
+ } else SynErr(101);
}
void ImplBody(out VariableSeq/*!*/ locals, out StmtList/*!*/ stmtList) {
@@ -917,7 +917,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
Proposition(out e);
Expect(8);
post.Add(new Ensures(tok, free, e, null, kv));
- } else SynErr(100);
+ } else SynErr(102);
}
void StmtList(out StmtList/*!*/ stmtList) {
@@ -997,9 +997,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
Cmd/*!*/ cn;
QKeyValue kv = null;
- if (la.kind == 1) {
+ switch (la.kind) {
+ case 1: {
LabelOrAssign(out c, out label);
- } else if (la.kind == 46) {
+ break;
+ }
+ case 46: {
Get();
x = t;
while (la.kind == 27) {
@@ -1008,7 +1011,9 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
Proposition(out e);
c = new AssertCmd(x, e, kv);
Expect(8);
- } else if (la.kind == 47) {
+ break;
+ }
+ case 47: {
Get();
x = t;
while (la.kind == 27) {
@@ -1017,7 +1022,20 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
Proposition(out e);
c = new AssumeCmd(x, e, kv);
Expect(8);
- } else if (la.kind == 48) {
+ break;
+ }
+ case 48: {
+ Get();
+ x = t;
+ while (la.kind == 27) {
+ Attribute(ref kv);
+ }
+ Proposition(out e);
+ c = new YieldCmd(x, e, kv);
+ Expect(8);
+ break;
+ }
+ case 49: {
Get();
x = t;
Idents(out xs);
@@ -1029,11 +1047,16 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
c = new HavocCmd(x,ids);
- } else if (la.kind == 35 || la.kind == 50) {
+ break;
+ }
+ case 35: case 51: case 52: {
CallCmd(out cn);
Expect(8);
c = cn;
- } else SynErr(101);
+ break;
+ }
+ default: SynErr(103); break;
+ }
}
void StructuredCmd(out StructuredCmd/*!*/ ec) {
@@ -1049,7 +1072,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
} else if (la.kind == 45) {
BreakCmd(out bcmd);
ec = bcmd;
- } else SynErr(102);
+ } else SynErr(104);
}
void TransferCmd(out TransferCmd/*!*/ tc) {
@@ -1069,7 +1092,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
} else if (la.kind == 39) {
Get();
tc = new ReturnCmd(t);
- } else SynErr(103);
+ } else SynErr(105);
Expect(8);
}
@@ -1094,7 +1117,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
Get();
StmtList(out els);
elseOption = els;
- } else SynErr(104);
+ } else SynErr(106);
}
ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
}
@@ -1157,7 +1180,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
} else if (StartOf(9)) {
Expression(out ee);
e = ee;
- } else SynErr(105);
+ } else SynErr(107);
Expect(10);
}
@@ -1174,7 +1197,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
if (la.kind == 11) {
Get();
c = null; label = x;
- } else if (la.kind == 12 || la.kind == 17 || la.kind == 49) {
+ } else if (la.kind == 12 || la.kind == 17 || la.kind == 50) {
lhss = new List<AssignLhs/*!*/>();
lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
while (la.kind == 17) {
@@ -1192,7 +1215,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
lhss.Add(lhs);
}
- Expect(49);
+ Expect(50);
x = t; /* use location of := */
Expression(out e0);
rhss = new List<Expr/*!*/> ();
@@ -1204,7 +1227,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
Expect(8);
c = new AssignCmd(x, lhss, rhss);
- } else SynErr(106);
+ } else SynErr(108);
}
void CallCmd(out Cmd/*!*/ c) {
@@ -1215,122 +1238,62 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
Expr en; List<Expr> args;
c = dummyCmd;
bool isFree = false;
+ bool isAsync = false;
+ if (la.kind == 51) {
+ Get();
+ isAsync = true;
+ }
if (la.kind == 35) {
Get();
isFree = true;
}
- Expect(50);
+ Expect(52);
x = t;
while (la.kind == 27) {
Attribute(ref kv);
}
- if (la.kind == 1) {
- Ident(out first);
- if (la.kind == 9) {
- Get();
- if (StartOf(10)) {
- CallForallArg(out en);
- es.Add(en);
- while (la.kind == 12) {
- Get();
- CallForallArg(out en);
- es.Add(en);
- }
- }
- Expect(10);
- c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
- } else if (la.kind == 12 || la.kind == 49) {
- ids.Add(new IdentifierExpr(first, first.val));
- if (la.kind == 12) {
- Get();
- CallOutIdent(out p);
- if (p==null) {
- ids.Add(null);
- } else {
- ids.Add(new IdentifierExpr(p, p.val));
- }
-
- while (la.kind == 12) {
- Get();
- CallOutIdent(out p);
- if (p==null) {
- ids.Add(null);
- } else {
- ids.Add(new IdentifierExpr(p, p.val));
- }
-
- }
- }
- Expect(49);
- Ident(out first);
- Expect(9);
- if (StartOf(10)) {
- CallForallArg(out en);
- es.Add(en);
- while (la.kind == 12) {
- Get();
- CallForallArg(out en);
- es.Add(en);
- }
- }
- Expect(10);
- c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
- } else SynErr(107);
- } else if (la.kind == 51) {
+ Ident(out first);
+ if (la.kind == 9) {
Get();
- Ident(out first);
- Expect(9);
- args = new List<Expr>();
- if (StartOf(10)) {
- CallForallArg(out en);
- args.Add(en);
+ if (StartOf(9)) {
+ Expression(out en);
+ es.Add(en);
while (la.kind == 12) {
Get();
- CallForallArg(out en);
- args.Add(en);
+ Expression(out en);
+ es.Add(en);
}
}
Expect(10);
- c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree;
- } else if (la.kind == 44) {
- Get();
- ids.Add(null);
+ c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
+ } else if (la.kind == 12 || la.kind == 50) {
+ ids.Add(new IdentifierExpr(first, first.val));
if (la.kind == 12) {
Get();
- CallOutIdent(out p);
- if (p==null) {
- ids.Add(null);
- } else {
- ids.Add(new IdentifierExpr(p, p.val));
- }
-
+ Ident(out p);
+ ids.Add(new IdentifierExpr(p, p.val));
while (la.kind == 12) {
Get();
- CallOutIdent(out p);
- if (p==null) {
- ids.Add(null);
- } else {
- ids.Add(new IdentifierExpr(p, p.val));
- }
-
+ Ident(out p);
+ ids.Add(new IdentifierExpr(p, p.val));
}
}
- Expect(49);
+ Expect(50);
Ident(out first);
Expect(9);
- if (StartOf(10)) {
- CallForallArg(out en);
+ if (StartOf(9)) {
+ Expression(out en);
es.Add(en);
while (la.kind == 12) {
Get();
- CallForallArg(out en);
+ Expression(out en);
es.Add(en);
}
}
Expect(10);
- c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
- } else SynErr(108);
+ c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
+ } else SynErr(109);
}
void MapAssignIndex(out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes) {
@@ -1351,30 +1314,6 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
Expect(18);
}
- void CallForallArg(out Expr exprOptional) {
- exprOptional = null;
- Expr/*!*/ e;
-
- if (la.kind == 44) {
- Get();
- } else if (StartOf(9)) {
- Expression(out e);
- exprOptional = e;
- } else SynErr(109);
- }
-
- void CallOutIdent(out IToken id) {
- id = null;
- IToken/*!*/ p;
-
- if (la.kind == 44) {
- Get();
- } else if (la.kind == 1) {
- Ident(out p);
- id = p;
- } else SynErr(110);
- }
-
void Expressions(out ExprSeq/*!*/ es) {
Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new ExprSeq();
Expression(out e);
@@ -1389,8 +1328,8 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
LogicalExpression(out e0);
- if (StartOf(11)) {
- if (la.kind == 54 || la.kind == 55) {
+ if (StartOf(10)) {
+ if (la.kind == 55 || la.kind == 56) {
ImpliesOp();
x = t;
ImpliesExpression(true, out e1);
@@ -1402,7 +1341,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
x = t;
LogicalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
- while (la.kind == 56 || la.kind == 57) {
+ while (la.kind == 57 || la.kind == 58) {
ExpliesOp();
x = t;
LogicalExpression(out e1);
@@ -1413,23 +1352,23 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
void EquivOp() {
- if (la.kind == 52) {
+ if (la.kind == 53) {
Get();
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
Get();
- } else SynErr(111);
+ } else SynErr(110);
}
void LogicalExpression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(12)) {
- if (la.kind == 58 || la.kind == 59) {
+ if (StartOf(11)) {
+ if (la.kind == 59 || la.kind == 60) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
- while (la.kind == 58 || la.kind == 59) {
+ while (la.kind == 59 || la.kind == 60) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1440,7 +1379,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
x = t;
RelationalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
- while (la.kind == 60 || la.kind == 61) {
+ while (la.kind == 61 || la.kind == 62) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1451,25 +1390,25 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
void ImpliesOp() {
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
- } else if (la.kind == 55) {
+ } else if (la.kind == 56) {
Get();
- } else SynErr(112);
+ } else SynErr(111);
}
void ExpliesOp() {
- if (la.kind == 56) {
+ if (la.kind == 57) {
Get();
- } else if (la.kind == 57) {
+ } else if (la.kind == 58) {
Get();
- } else SynErr(113);
+ } else SynErr(112);
}
void RelationalExpression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
BvTerm(out e0);
- if (StartOf(13)) {
+ if (StartOf(12)) {
RelOp(out x, out op);
BvTerm(out e1);
e0 = Expr.Binary(x, op, e0, e1);
@@ -1477,25 +1416,25 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
void AndOp() {
- if (la.kind == 58) {
+ if (la.kind == 59) {
Get();
- } else if (la.kind == 59) {
+ } else if (la.kind == 60) {
Get();
- } else SynErr(114);
+ } else SynErr(113);
}
void OrOp() {
- if (la.kind == 60) {
+ if (la.kind == 61) {
Get();
- } else if (la.kind == 61) {
+ } else if (la.kind == 62) {
Get();
- } else SynErr(115);
+ } else SynErr(114);
}
void BvTerm(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
Term(out e0);
- while (la.kind == 70) {
+ while (la.kind == 71) {
Get();
x = t;
Term(out e1);
@@ -1506,7 +1445,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
switch (la.kind) {
- case 62: {
+ case 63: {
Get();
x = t; op=BinaryOperator.Opcode.Eq;
break;
@@ -1521,49 +1460,49 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
x = t; op=BinaryOperator.Opcode.Gt;
break;
}
- case 63: {
+ case 64: {
Get();
x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 64: {
+ case 65: {
Get();
x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- case 65: {
+ case 66: {
Get();
x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 66: {
+ case 67: {
Get();
x = t; op=BinaryOperator.Opcode.Subtype;
break;
}
- case 67: {
+ case 68: {
Get();
x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 68: {
+ case 69: {
Get();
x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 69: {
+ case 70: {
Get();
x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- default: SynErr(116); break;
+ default: SynErr(115); 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 == 71 || la.kind == 72) {
+ while (la.kind == 72 || la.kind == 73) {
AddOp(out x, out op);
Factor(out e1);
e0 = Expr.Binary(x, op, e0, e1);
@@ -1573,7 +1512,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
void Factor(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
Power(out e0);
- while (StartOf(14)) {
+ while (StartOf(13)) {
MulOp(out x, out op);
Power(out e1);
e0 = Expr.Binary(x, op, e0, e1);
@@ -1582,19 +1521,19 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
- if (la.kind == 71) {
+ if (la.kind == 72) {
Get();
x = t; op=BinaryOperator.Opcode.Add;
- } else if (la.kind == 72) {
+ } else if (la.kind == 73) {
Get();
x = t; op=BinaryOperator.Opcode.Sub;
- } else SynErr(117);
+ } else SynErr(116);
}
void Power(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
UnaryExpression(out e0);
- if (la.kind == 76) {
+ if (la.kind == 77) {
Get();
x = t;
Power(out e1);
@@ -1607,48 +1546,48 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
if (la.kind == 44) {
Get();
x = t; op=BinaryOperator.Opcode.Mul;
- } else if (la.kind == 73) {
+ } else if (la.kind == 74) {
Get();
x = t; op=BinaryOperator.Opcode.Div;
- } else if (la.kind == 74) {
+ } else if (la.kind == 75) {
Get();
x = t; op=BinaryOperator.Opcode.Mod;
- } else if (la.kind == 75) {
+ } else if (la.kind == 76) {
Get();
x = t; op=BinaryOperator.Opcode.RealDiv;
- } else SynErr(118);
+ } else SynErr(117);
}
void UnaryExpression(out Expr/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
e = dummyExpr;
- if (la.kind == 72) {
+ if (la.kind == 73) {
Get();
x = t;
UnaryExpression(out e);
e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e);
- } else if (la.kind == 77 || la.kind == 78) {
+ } else if (la.kind == 78 || la.kind == 79) {
NegOp();
x = t;
UnaryExpression(out e);
e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
- } else if (StartOf(15)) {
+ } else if (StartOf(14)) {
CoercionExpression(out e);
- } else SynErr(119);
+ } else SynErr(118);
}
void NegOp() {
- if (la.kind == 77) {
+ if (la.kind == 78) {
Get();
- } else if (la.kind == 78) {
+ } else if (la.kind == 79) {
Get();
- } else SynErr(120);
+ } else SynErr(119);
}
void CoercionExpression(out Expr/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
- Type/*!*/ coercedTo;
+ Bpl.Type/*!*/ coercedTo;
BigNum bn;
ArrayExpression(out e);
@@ -1667,7 +1606,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else SynErr(121);
+ } else SynErr(120);
}
}
@@ -1683,7 +1622,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
x = t; allArgs = new ExprSeq ();
allArgs.Add(e);
store = false; bvExtract = false;
- if (StartOf(16)) {
+ if (StartOf(15)) {
if (StartOf(9)) {
Expression(out index0);
if (index0 is BvBounds)
@@ -1699,7 +1638,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
allArgs.Add(e1);
}
- if (la.kind == 49) {
+ if (la.kind == 50) {
Get();
Expression(out e1);
if (bvExtract || e1 is BvBounds)
@@ -1748,12 +1687,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
List<Block/*!*/>/*!*/ blocks;
switch (la.kind) {
- case 79: {
+ case 80: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 80: {
+ case 81: {
Get();
e = new LiteralExpr(t, true);
break;
@@ -1783,12 +1722,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
e = new NAryExpr(x, new FunctionCall(id), es);
} else if (la.kind == 10) {
e = new NAryExpr(x, new FunctionCall(id), new ExprSeq());
- } else SynErr(122);
+ } else SynErr(121);
Expect(10);
}
break;
}
- case 81: {
+ case 82: {
Get();
x = t;
Expect(9);
@@ -1822,19 +1761,19 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
if (e is BvBounds)
this.SemErr("parentheses around bitvector bounds " +
"are not allowed");
- } else if (la.kind == 51 || la.kind == 85) {
+ } else if (la.kind == 86 || la.kind == 87) {
Forall();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
e = new ForallExpr(x, typeParams, ds, kv, trig, e);
- } else if (la.kind == 86 || la.kind == 87) {
+ } else if (la.kind == 88 || la.kind == 89) {
Exists();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
- } else if (la.kind == 88 || la.kind == 89) {
+ } else if (la.kind == 90 || la.kind == 91) {
Lambda();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
@@ -1842,7 +1781,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
SemErr("triggers not allowed in lambda expressions");
if (typeParams.Length + ds.Length > 0)
e = new LambdaExpr(x, typeParams, ds, kv, e);
- } else SynErr(123);
+ } else SynErr(122);
Expect(10);
break;
}
@@ -1850,12 +1789,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
IfThenElseExpression(out e);
break;
}
- case 82: {
+ case 83: {
CodeExpression(out locals, out blocks);
e = new CodeExpr(locals, blocks);
break;
}
- default: SynErr(124); break;
+ default: SynErr(123); break;
}
}
@@ -1867,7 +1806,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
} else if (la.kind == 6) {
Get();
s = t.val;
- } else SynErr(125);
+ } else SynErr(124);
try {
n = BigDec.FromString(s);
} catch (FormatException) {
@@ -1894,11 +1833,11 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
void Forall() {
- if (la.kind == 51) {
+ if (la.kind == 86) {
Get();
- } else if (la.kind == 85) {
+ } else if (la.kind == 87) {
Get();
- } else SynErr(126);
+ } else SynErr(125);
}
void QuantifierBody(IToken/*!*/ q, out TypeVariableSeq/*!*/ typeParams, out VariableSeq/*!*/ ds,
@@ -1916,7 +1855,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
} else if (la.kind == 1 || la.kind == 27) {
BoundVars(q, out ds);
- } else SynErr(127);
+ } else SynErr(126);
QSep();
while (la.kind == 27) {
AttributeOrTrigger(ref kv, ref trig);
@@ -1925,19 +1864,19 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
void Exists() {
- if (la.kind == 86) {
+ if (la.kind == 88) {
Get();
- } else if (la.kind == 87) {
+ } else if (la.kind == 89) {
Get();
- } else SynErr(128);
+ } else SynErr(127);
}
void Lambda() {
- if (la.kind == 88) {
+ if (la.kind == 90) {
Get();
- } else if (la.kind == 89) {
+ } else if (la.kind == 91) {
Get();
- } else SynErr(129);
+ } else SynErr(128);
}
void IfThenElseExpression(out Expr/*!*/ e) {
@@ -1948,7 +1887,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Expect(40);
tok = t;
Expression(out e0);
- Expect(84);
+ Expect(85);
Expression(out e1);
Expect(41);
Expression(out e2);
@@ -1959,7 +1898,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new VariableSeq(); Block/*!*/ b;
blocks = new List<Block/*!*/>();
- Expect(82);
+ Expect(83);
while (la.kind == 7) {
LocalVars(locals);
}
@@ -1969,7 +1908,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
SpecBlock(out b);
blocks.Add(b);
}
- Expect(83);
+ Expect(84);
}
void SpecBlock(out Block/*!*/ b) {
@@ -2007,7 +1946,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Get();
Expression(out e);
b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
- } else SynErr(130);
+ } else SynErr(129);
Expect(8);
}
@@ -2022,7 +1961,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Get();
Expect(1);
key = t.val; parameters = new List<object/*!*/>();
- if (StartOf(17)) {
+ if (StartOf(16)) {
AttributeParameter(out param);
parameters.Add(param);
while (la.kind == 12) {
@@ -2064,7 +2003,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
trig.AddLast(new Trigger(tok, true, es, null));
}
- } else SynErr(131);
+ } else SynErr(130);
Expect(28);
}
@@ -2079,15 +2018,15 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
} else if (StartOf(9)) {
Expression(out e);
o = e;
- } else SynErr(132);
+ } else SynErr(131);
}
void QSep() {
- if (la.kind == 90) {
+ if (la.kind == 92) {
Get();
- } else if (la.kind == 91) {
+ } else if (la.kind == 93) {
Get();
- } else SynErr(133);
+ } else SynErr(132);
}
@@ -2103,24 +2042,23 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
static readonly bool[,]/*!*/ set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,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,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, 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,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,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,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,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,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,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,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x}
};
} // end Parser
@@ -2193,92 +2131,91 @@ public class Errors {
case 45: s = "\"break\" expected"; break;
case 46: s = "\"assert\" expected"; break;
case 47: s = "\"assume\" expected"; break;
- case 48: s = "\"havoc\" expected"; break;
- case 49: s = "\":=\" expected"; break;
- case 50: s = "\"call\" expected"; break;
- case 51: s = "\"forall\" expected"; break;
- case 52: s = "\"<==>\" expected"; break;
- case 53: s = "\"\\u21d4\" expected"; break;
- case 54: s = "\"==>\" expected"; break;
- case 55: s = "\"\\u21d2\" expected"; break;
- case 56: s = "\"<==\" expected"; break;
- case 57: s = "\"\\u21d0\" expected"; break;
- case 58: s = "\"&&\" expected"; break;
- case 59: s = "\"\\u2227\" expected"; break;
- case 60: s = "\"||\" expected"; break;
- case 61: s = "\"\\u2228\" expected"; break;
- case 62: s = "\"==\" expected"; break;
- case 63: s = "\"<=\" expected"; break;
- case 64: s = "\">=\" expected"; break;
- case 65: s = "\"!=\" expected"; break;
- case 66: s = "\"<:\" expected"; break;
- case 67: s = "\"\\u2260\" expected"; break;
- case 68: s = "\"\\u2264\" expected"; break;
- case 69: s = "\"\\u2265\" expected"; break;
- case 70: s = "\"++\" expected"; break;
- case 71: s = "\"+\" expected"; break;
- case 72: s = "\"-\" expected"; break;
- case 73: s = "\"div\" expected"; break;
- case 74: s = "\"mod\" expected"; break;
- case 75: s = "\"/\" expected"; break;
- case 76: s = "\"**\" expected"; break;
- case 77: s = "\"!\" expected"; break;
- case 78: s = "\"\\u00ac\" expected"; break;
- case 79: s = "\"false\" expected"; break;
- case 80: s = "\"true\" expected"; break;
- case 81: s = "\"old\" expected"; break;
- case 82: s = "\"|{\" expected"; break;
- case 83: s = "\"}|\" expected"; break;
- case 84: s = "\"then\" expected"; break;
- case 85: s = "\"\\u2200\" expected"; break;
- case 86: s = "\"exists\" expected"; break;
- case 87: s = "\"\\u2203\" expected"; break;
- case 88: s = "\"lambda\" expected"; break;
- case 89: s = "\"\\u03bb\" expected"; break;
- case 90: s = "\"::\" expected"; break;
- case 91: s = "\"\\u2022\" expected"; break;
- case 92: s = "??? expected"; break;
- case 93: s = "invalid Function"; break;
- case 94: s = "invalid Function"; break;
- case 95: s = "invalid Procedure"; break;
- case 96: s = "invalid Type"; break;
- case 97: s = "invalid TypeAtom"; break;
- case 98: s = "invalid TypeArgs"; break;
- case 99: s = "invalid Spec"; break;
- case 100: s = "invalid SpecPrePost"; break;
- case 101: s = "invalid LabelOrCmd"; break;
- case 102: s = "invalid StructuredCmd"; break;
- case 103: s = "invalid TransferCmd"; break;
- case 104: s = "invalid IfCmd"; break;
- case 105: s = "invalid Guard"; break;
- case 106: s = "invalid LabelOrAssign"; break;
- case 107: s = "invalid CallCmd"; break;
- case 108: s = "invalid CallCmd"; break;
- case 109: s = "invalid CallForallArg"; break;
- case 110: s = "invalid CallOutIdent"; break;
- case 111: s = "invalid EquivOp"; break;
- case 112: s = "invalid ImpliesOp"; break;
- case 113: s = "invalid ExpliesOp"; break;
- case 114: s = "invalid AndOp"; break;
- case 115: s = "invalid OrOp"; break;
- case 116: s = "invalid RelOp"; break;
- case 117: s = "invalid AddOp"; break;
- case 118: s = "invalid MulOp"; break;
- case 119: s = "invalid UnaryExpression"; break;
- case 120: s = "invalid NegOp"; break;
- case 121: s = "invalid CoercionExpression"; break;
+ case 48: s = "\"yield\" expected"; break;
+ case 49: s = "\"havoc\" expected"; break;
+ case 50: s = "\":=\" expected"; break;
+ case 51: s = "\"async\" expected"; break;
+ case 52: s = "\"call\" expected"; break;
+ case 53: s = "\"<==>\" expected"; break;
+ case 54: s = "\"\\u21d4\" expected"; break;
+ case 55: s = "\"==>\" expected"; break;
+ case 56: s = "\"\\u21d2\" expected"; break;
+ case 57: s = "\"<==\" expected"; break;
+ case 58: s = "\"\\u21d0\" expected"; break;
+ case 59: s = "\"&&\" expected"; break;
+ case 60: s = "\"\\u2227\" expected"; break;
+ case 61: s = "\"||\" expected"; break;
+ case 62: s = "\"\\u2228\" expected"; break;
+ case 63: s = "\"==\" expected"; break;
+ case 64: s = "\"<=\" expected"; break;
+ case 65: s = "\">=\" expected"; break;
+ case 66: s = "\"!=\" expected"; break;
+ case 67: s = "\"<:\" expected"; break;
+ case 68: s = "\"\\u2260\" expected"; break;
+ case 69: s = "\"\\u2264\" expected"; break;
+ case 70: s = "\"\\u2265\" expected"; break;
+ case 71: s = "\"++\" expected"; break;
+ case 72: s = "\"+\" expected"; break;
+ case 73: s = "\"-\" expected"; break;
+ case 74: s = "\"div\" expected"; break;
+ case 75: s = "\"mod\" expected"; break;
+ case 76: s = "\"/\" expected"; break;
+ case 77: s = "\"**\" expected"; break;
+ case 78: s = "\"!\" expected"; break;
+ case 79: s = "\"\\u00ac\" expected"; break;
+ case 80: s = "\"false\" expected"; break;
+ case 81: s = "\"true\" expected"; break;
+ case 82: s = "\"old\" expected"; break;
+ case 83: s = "\"|{\" expected"; break;
+ case 84: s = "\"}|\" expected"; break;
+ case 85: s = "\"then\" expected"; break;
+ case 86: s = "\"forall\" expected"; break;
+ case 87: s = "\"\\u2200\" expected"; break;
+ case 88: s = "\"exists\" expected"; break;
+ case 89: s = "\"\\u2203\" expected"; break;
+ case 90: s = "\"lambda\" expected"; break;
+ case 91: s = "\"\\u03bb\" expected"; break;
+ case 92: s = "\"::\" expected"; break;
+ case 93: s = "\"\\u2022\" expected"; break;
+ case 94: s = "??? expected"; break;
+ case 95: s = "invalid Function"; break;
+ case 96: s = "invalid Function"; break;
+ case 97: s = "invalid Procedure"; break;
+ case 98: s = "invalid Type"; break;
+ case 99: s = "invalid TypeAtom"; break;
+ case 100: s = "invalid TypeArgs"; break;
+ case 101: s = "invalid Spec"; break;
+ case 102: s = "invalid SpecPrePost"; break;
+ case 103: s = "invalid LabelOrCmd"; break;
+ case 104: s = "invalid StructuredCmd"; break;
+ case 105: s = "invalid TransferCmd"; break;
+ case 106: s = "invalid IfCmd"; break;
+ case 107: s = "invalid Guard"; break;
+ case 108: s = "invalid LabelOrAssign"; break;
+ case 109: s = "invalid CallCmd"; break;
+ case 110: s = "invalid EquivOp"; break;
+ case 111: s = "invalid ImpliesOp"; break;
+ case 112: s = "invalid ExpliesOp"; break;
+ case 113: s = "invalid AndOp"; break;
+ case 114: s = "invalid OrOp"; break;
+ case 115: s = "invalid RelOp"; break;
+ case 116: s = "invalid AddOp"; break;
+ case 117: s = "invalid MulOp"; break;
+ case 118: s = "invalid UnaryExpression"; break;
+ case 119: s = "invalid NegOp"; break;
+ case 120: s = "invalid CoercionExpression"; break;
+ case 121: s = "invalid AtomExpression"; break;
case 122: s = "invalid AtomExpression"; break;
case 123: s = "invalid AtomExpression"; break;
- case 124: s = "invalid AtomExpression"; break;
- case 125: s = "invalid Dec"; break;
- case 126: s = "invalid Forall"; break;
- case 127: s = "invalid QuantifierBody"; break;
- case 128: s = "invalid Exists"; break;
- case 129: s = "invalid Lambda"; break;
- case 130: s = "invalid SpecBlock"; break;
- case 131: s = "invalid AttributeOrTrigger"; break;
- case 132: s = "invalid AttributeParameter"; break;
- case 133: s = "invalid QSep"; break;
+ case 124: s = "invalid Dec"; break;
+ case 125: s = "invalid Forall"; break;
+ case 126: s = "invalid QuantifierBody"; break;
+ case 127: s = "invalid Exists"; break;
+ case 128: s = "invalid Lambda"; break;
+ case 129: s = "invalid SpecBlock"; break;
+ case 130: s = "invalid AttributeOrTrigger"; break;
+ case 131: s = "invalid AttributeParameter"; break;
+ case 132: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index 60c15b41..873a5724 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 92;
- const int noSym = 92;
+ const int maxT = 94;
+ const int noSym = 94;
[ContractInvariantMethod]
@@ -516,17 +516,19 @@ public class Scanner {
case "break": t.kind = 45; break;
case "assert": t.kind = 46; break;
case "assume": t.kind = 47; break;
- case "havoc": t.kind = 48; break;
- case "call": t.kind = 50; break;
- case "forall": t.kind = 51; break;
- case "div": t.kind = 73; break;
- case "mod": t.kind = 74; break;
- case "false": t.kind = 79; break;
- case "true": t.kind = 80; break;
- case "old": t.kind = 81; break;
- case "then": t.kind = 84; break;
- case "exists": t.kind = 86; break;
- case "lambda": t.kind = 88; break;
+ case "yield": t.kind = 48; break;
+ case "havoc": t.kind = 49; break;
+ case "async": t.kind = 51; break;
+ case "call": t.kind = 52; break;
+ case "div": t.kind = 74; break;
+ case "mod": t.kind = 75; break;
+ case "false": t.kind = 80; break;
+ case "true": t.kind = 81; break;
+ case "old": t.kind = 82; break;
+ case "then": t.kind = 85; break;
+ case "forall": t.kind = 86; break;
+ case "exists": t.kind = 88; break;
+ case "lambda": t.kind = 90; break;
default: break;
}
}
@@ -646,64 +648,64 @@ public class Scanner {
case 25:
{t.kind = 27; break;}
case 26:
- {t.kind = 49; break;}
+ {t.kind = 50; break;}
case 27:
- {t.kind = 52; break;}
- case 28:
{t.kind = 53; break;}
- case 29:
+ case 28:
{t.kind = 54; break;}
- case 30:
+ case 29:
{t.kind = 55; break;}
+ case 30:
+ {t.kind = 56; break;}
case 31:
- {t.kind = 57; break;}
+ {t.kind = 58; break;}
case 32:
if (ch == '&') {AddCh(); goto case 33;}
else {goto case 0;}
case 33:
- {t.kind = 58; break;}
- case 34:
{t.kind = 59; break;}
- case 35:
+ case 34:
{t.kind = 60; break;}
- case 36:
+ case 35:
{t.kind = 61; break;}
+ case 36:
+ {t.kind = 62; break;}
case 37:
- {t.kind = 64; break;}
- case 38:
{t.kind = 65; break;}
- case 39:
+ case 38:
{t.kind = 66; break;}
- case 40:
+ case 39:
{t.kind = 67; break;}
- case 41:
+ case 40:
{t.kind = 68; break;}
- case 42:
+ case 41:
{t.kind = 69; break;}
- case 43:
+ case 42:
{t.kind = 70; break;}
+ case 43:
+ {t.kind = 71; break;}
case 44:
- {t.kind = 72; break;}
+ {t.kind = 73; break;}
case 45:
- {t.kind = 75; break;}
- case 46:
{t.kind = 76; break;}
+ case 46:
+ {t.kind = 77; break;}
case 47:
- {t.kind = 78; break;}
+ {t.kind = 79; break;}
case 48:
- {t.kind = 82; break;}
- case 49:
{t.kind = 83; break;}
+ case 49:
+ {t.kind = 84; break;}
case 50:
- {t.kind = 85; break;}
- case 51:
{t.kind = 87; break;}
- case 52:
+ case 51:
{t.kind = 89; break;}
+ case 52:
+ {t.kind = 91; break;}
case 53:
- {t.kind = 90; break;}
+ {t.kind = 92; break;}
case 54:
- {t.kind = 91; break;}
+ {t.kind = 93; break;}
case 55:
recEnd = pos; recKind = 11;
if (ch == '=') {AddCh(); goto case 26;}
@@ -735,25 +737,25 @@ public class Scanner {
else if (ch == '{') {AddCh(); goto case 48;}
else {goto case 0;}
case 62:
- recEnd = pos; recKind = 77;
+ recEnd = pos; recKind = 78;
if (ch == '=') {AddCh(); goto case 38;}
- else {t.kind = 77; break;}
+ else {t.kind = 78; break;}
case 63:
- recEnd = pos; recKind = 71;
+ recEnd = pos; recKind = 72;
if (ch == '+') {AddCh(); goto case 43;}
- else {t.kind = 71; break;}
+ else {t.kind = 72; break;}
case 64:
- recEnd = pos; recKind = 63;
+ recEnd = pos; recKind = 64;
if (ch == '=') {AddCh(); goto case 66;}
- else {t.kind = 63; break;}
+ else {t.kind = 64; break;}
case 65:
- recEnd = pos; recKind = 62;
+ recEnd = pos; recKind = 63;
if (ch == '>') {AddCh(); goto case 29;}
- else {t.kind = 62; break;}
+ else {t.kind = 63; break;}
case 66:
- recEnd = pos; recKind = 56;
+ recEnd = pos; recKind = 57;
if (ch == '>') {AddCh(); goto case 27;}
- else {t.kind = 56; break;}
+ else {t.kind = 57; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 66eee658..2071154b 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -84,6 +84,13 @@ namespace Microsoft.Boogie {
node.Expr = this.VisitExpr(node.Expr);
return node;
}
+ public virtual Cmd VisitYieldCmd(YieldCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+ node.Expr = this.VisitExpr(node.Expr);
+ return node;
+ }
public virtual AtomicRE VisitAtomicRE(AtomicRE node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<AtomicRE>() != null);
@@ -168,21 +175,6 @@ namespace Microsoft.Boogie {
node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(node.Outs[i]));
return node;
}
- public virtual Cmd VisitCallForallCmd(CallForallCmd node) {
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- List<Expr> elist = new List<Expr>(node.Ins.Count);
- foreach (Expr arg in node.Ins) {
- if (arg == null) {
- elist.Add(null);
- } else {
- elist.Add(this.VisitExpr(arg));
- }
- }
- node.Ins = elist;
- node.Proc = this.VisitProcedure(cce.NonNull(node.Proc));
- return node;
- }
public virtual CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
Contract.Requires(cmdSeq != null);
Contract.Ensures(Contract.Result<CmdSeq>() != null);
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 3035c9de..d08a4d4b 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -647,12 +647,6 @@ namespace Microsoft.Boogie.VCExprAST {
Contract.Assert(false);
throw new cce.UnreachableException();
}
- public override Cmd VisitCallForallCmd(CallForallCmd node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
//Contract.Requires(cmdSeq != null);
Contract.Ensures(Contract.Result<CmdSeq>() != null);
diff --git a/Test/test0/Answer b/Test/test0/Answer
index d71ac997..8c7ce4c7 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -291,9 +291,8 @@ Orderings.bpl(18,20): Error: the parent of a constant has to be a constant
4 name resolution errors detected in Orderings.bpl
BadQuantifier.bpl(3,15): error: invalid QuantifierBody
1 parse errors detected in BadQuantifier.bpl
-EmptyCallArgs.bpl(31,2): Error: type variable must occur in types of given arguments: a
-EmptyCallArgs.bpl(32,2): Error: type variable must occur in types of given arguments: a
-2 name resolution errors detected in EmptyCallArgs.bpl
+
+Boogie program verifier finished with 0 verified, 0 errors
----- SeparateVerification0.bpl
SeparateVerification0.bpl(13,6): Error: undeclared identifier: y
1 name resolution errors detected in SeparateVerification0.bpl
diff --git a/Test/test0/EmptyCallArgs.bpl b/Test/test0/EmptyCallArgs.bpl
index eb1c43b7..d45633e9 100644
--- a/Test/test0/EmptyCallArgs.bpl
+++ b/Test/test0/EmptyCallArgs.bpl
@@ -9,13 +9,6 @@ procedure CallP() {
var z:C;
call z := P(x, y);
- call * := P(x, y);
- call z := P(*, y);
- call z := P(x, *);
- call * := P(*, y);
- call * := P(x, *);
- call z := P(*, *);
- call * := P(*, *);
}
procedure CallQ() {
@@ -24,10 +17,4 @@ procedure CallQ() {
var z:bool;
call z := Q(x, y);
- call * := Q(x, y);
- call z := Q(*, y);
- call z := Q(x, *);
- call * := Q(*, y);
- call * := Q(x, *); // problem: type parameter cannot be inferred
- call * := Q(*, *); // problem: type parameter cannot be inferred
} \ No newline at end of file
diff --git a/Test/test1/Answer b/Test/test1/Answer
index 94bf2d9a..70b7ea80 100644
--- a/Test/test1/Answer
+++ b/Test/test1/Answer
@@ -107,8 +107,6 @@ UpdateExprTyping.bpl(36,28): Error: right-hand side in map store with wrong type
UpdateExprTyping.bpl(38,27): Error: right-hand side in map store with wrong type: ref (expected: int)
UpdateExprTyping.bpl(39,27): Error: right-hand side in map store with wrong type: int (expected: ref)
12 type checking errors detected in UpdateExprTyping.bpl
-CallForallResolve.bpl(15,2): Error: call forall is allowed only on procedures with no modifies clause: Q
-1 type checking errors detected in CallForallResolve.bpl
MapsTypeErrors.bpl(26,6): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: m
MapsTypeErrors.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to []int)
MapsTypeErrors.bpl(33,3): Error: mismatched types in assignment command (cannot assign []int to int)
@@ -127,10 +125,8 @@ MapsTypeErrors.bpl(122,4): Error: mismatched types in assignment command (cannot
15 type checking errors detected in MapsTypeErrors.bpl
Orderings.bpl(6,19): Error: parent of constant has incompatible type (int instead of C)
1 type checking errors detected in Orderings.bpl
-EmptyCallArgs.bpl(15,17): Error: invalid type for argument 0 in call to P: int (expected: bool)
-EmptyCallArgs.bpl(26,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)
-EmptyCallArgs.bpl(28,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)
-3 type checking errors detected in EmptyCallArgs.bpl
+EmptyCallArgs.bpl(19,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)
+1 type checking errors detected in EmptyCallArgs.bpl
FunBody.bpl(6,45): Error: function body with invalid type: bool (expected: int)
FunBody.bpl(8,61): Error: function body with invalid type: int (expected: alpha)
FunBody.bpl(10,58): Error: function body with invalid type: int (expected: alpha)
@@ -163,4 +159,4 @@ IntReal.bpl(32,6): Error: argument type int does not match expected type real
IntReal.bpl(33,6): Error: argument type real does not match expected type int
IntReal.bpl(45,8): Error: invalid argument types (real and int) to binary operator div
IntReal.bpl(46,8): Error: invalid argument types (real and int) to binary operator mod
-18 type checking errors detected in IntReal.bpl \ No newline at end of file
+18 type checking errors detected in IntReal.bpl
diff --git a/Test/test1/CallForallResolve.bpl b/Test/test1/CallForallResolve.bpl
deleted file mode 100644
index 374db174..00000000
--- a/Test/test1/CallForallResolve.bpl
+++ /dev/null
@@ -1,23 +0,0 @@
-procedure P(x: int) returns (y: int);
-
-procedure CallP()
-{
- call forall P(5); // P is allowed here, even if it has out parameters
-}
-
-var global: bool;
-
-procedure Q(x: int);
- modifies global;
-
-procedure CallQ()
-{
- call forall Q(5); // error: P is not allowed here, because it has a modifies clause
-}
-
-procedure R(x: int);
-
-procedure CallR()
-{
- call forall R(5); // no problem that R has no body, though
-}
diff --git a/Test/test1/EmptyCallArgs.bpl b/Test/test1/EmptyCallArgs.bpl
index 18d837a9..31e4b43f 100644
--- a/Test/test1/EmptyCallArgs.bpl
+++ b/Test/test1/EmptyCallArgs.bpl
@@ -9,13 +9,6 @@ procedure CallP() {
var z:C;
call z := P(x, y);
- call * := P(x, y);
- call z := P(*, y);
- call z := P(x, *);
- call * := P(*, x); // type error
- call * := P(x, *);
- call z := P(*, *);
- call * := P(*, *);
}
procedure CallQ() {
@@ -24,8 +17,4 @@ procedure CallQ() {
var z:bool;
call x := Q(x, y); // type error
- call * := Q(x, y);
- call x := Q(*, y); // type error
- call x := Q(x, *);
- call * := Q(*, y);
} \ No newline at end of file
diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat
index 149e6dc9..ccd04355 100644
--- a/Test/test1/runtest.bat
+++ b/Test/test1/runtest.bat
@@ -12,7 +12,6 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe
%BGEXE% %* /noVerify Family.bpl
%BGEXE% %* /noVerify AttributeTyping.bpl
%BGEXE% %* /noVerify UpdateExprTyping.bpl
-%BGEXE% %* /noVerify CallForallResolve.bpl
%BGEXE% %* /noVerify MapsTypeErrors.bpl
%BGEXE% %* /noVerify Orderings.bpl
%BGEXE% %* /noVerify EmptyCallArgs.bpl
diff --git a/Test/test2/Answer b/Test/test2/Answer
index 9625c4db..4a7fd32f 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -424,11 +424,8 @@ FreeCall.bpl(66,5): Error BP5002: A precondition for this call might not hold.
FreeCall.bpl(14,3): Related location: This is the precondition that might not hold.
Execution trace:
FreeCall.bpl(66,5): anon0
-FreeCall.bpl(87,5): Error BP5001: This assertion might not hold.
-Execution trace:
- FreeCall.bpl(85,5): anon0
-Boogie program verifier finished with 8 verified, 5 errors
+Boogie program verifier finished with 7 verified, 4 errors
-------------------- Arrays.bpl /typeEncoding:m --------------------
Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.
@@ -462,34 +459,6 @@ Boogie program verifier finished with 0 verified, 1 error
Boogie program verifier finished with 1 verified, 0 errors
--------------------- CallForall.bpl --------------------
-CallForall.bpl(17,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(17,3): anon0
-CallForall.bpl(29,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(28,3): anon0
-CallForall.bpl(41,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(40,3): anon0
-CallForall.bpl(47,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(46,3): anon0
-CallForall.bpl(75,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(75,3): anon0
-CallForall.bpl(111,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(109,3): anon0
-CallForall.bpl(118,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(117,3): anon0
-CallForall.bpl(125,3): Error BP5001: This assertion might not hold.
-Execution trace:
- CallForall.bpl(124,3): anon0
-
-Boogie program verifier finished with 10 verified, 8 errors
-
-------------------- ContractEvaluationOrder.bpl --------------------
ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold on this return path.
ContractEvaluationOrder.bpl(3,3): Related location: This is the postcondition that might not hold.
diff --git a/Test/test2/CallForall.bpl b/Test/test2/CallForall.bpl
deleted file mode 100644
index 98a62103..00000000
--- a/Test/test2/CallForall.bpl
+++ /dev/null
@@ -1,134 +0,0 @@
-function G(int) returns (int);
-axiom (forall x: int :: { G(x) } 0 <= x ==> G(x) == x);
-
-function F(int) returns (int);
-axiom (forall x: int :: { F(G(x)) } 0 <= x ==> F(G(x)) == 5);
-
-procedure Lemma(y: int)
- requires 0 <= y;
- ensures F(y) == 5;
-{
- // proof:
- assert G(y) == y;
-}
-
-procedure Main0()
-{
- assert F(2) == 5; // error: cannot prove this directly, because of the trigger
-}
-
-procedure Main1()
-{
- call Lemma(2);
- assert F(2) == 5;
-}
-
-procedure Main2()
-{
- call Lemma(3);
- assert F(2) == 5; // error: Lemma was instantiated the wrong way
-}
-
-procedure Main3()
-{
- call forall Lemma(*);
- assert F(2) == 5;
-}
-
-procedure Main4()
-{
- call forall Lemma(*);
- assert false; // error
-}
-
-procedure Main5(z: int)
-{
- call forall Lemma(*);
- assert F(z) == 5; // error: z might be negative
-}
-
-procedure Main6(z: int)
- requires 0 <= z;
-{
- call forall Lemma(*);
- assert F(z) == 5;
-}
-
-// ------------ several parameters
-
-function K(int, int) returns (int);
-axiom (forall x: int, y: int :: { K(G(x), G(y)) } 0 <= x && 0 <= y ==> K(G(x), G(y)) == 25);
-
-procedure MultivarLemma(x: int, y: int)
- requires 0 <= x;
- requires 0 <= y;
- ensures K(x,y) == 25;
-{
- // proof:
- assert G(x) == x;
- assert G(y) == y;
-}
-
-procedure Multi0(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- assert K(x,y) == 25; // error
-}
-
-procedure Multi1(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call MultivarLemma(x, y);
- assert K(x,y) == 25;
-}
-
-procedure Multi2(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(x, y);
- assert K(x,y) == 25;
-}
-
-procedure Multi3(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(*, y);
- assert K(x,y) == 25;
-}
-
-procedure Multi4(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(x, *);
- assert K(x,y) == 25;
-}
-
-procedure Multi5(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(2 + 100, *);
- assert K(102, y) == 25;
- assert false; // error
-}
-
-procedure Multi6(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(*, y);
- assert K(x+2,y+2) == 25; // error
-}
-
-procedure Multi7(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(x, *);
- assert K(x+2,y+2) == 25; // error
-}
-
-procedure Multi8(x: int, y: int)
- requires 0 <= x && 0 <= y;
-{
- call forall MultivarLemma(*, *);
- assert K(x+2,y+2) == 25; // that's the ticket!
-}
-
diff --git a/Test/test2/FreeCall.bpl b/Test/test2/FreeCall.bpl
index 06eb737e..a873a4e6 100644
--- a/Test/test2/FreeCall.bpl
+++ b/Test/test2/FreeCall.bpl
@@ -80,17 +80,3 @@ procedure FreeCall4()
free call b := UncallableReturn(-1);
}
-procedure NormalCall5()
-{
- call forall TestCallForall(*);
- assert T(true);
- assert T(false); // error
-}
-
-procedure FreeCall5()
-{
- free call forall TestCallForall(*);
- assert T(true);
- assert T(false);
- assert false;
-}
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index f32bf844..89715252 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -27,7 +27,7 @@ for %%f in (Arrays.bpl Lambda.bpl TypeEncodingM.bpl ) do (
echo -------------------- sk_hack.bpl --------------------
%BGEXE% %* /noinfer sk_hack.bpl
-for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do (
+for %%f in (ContractEvaluationOrder.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* %%f
diff --git a/Test/test20/Answer b/Test/test20/Answer
index fa33507e..5e4481ca 100644
--- a/Test/test20/Answer
+++ b/Test/test20/Answer
@@ -55,8 +55,7 @@ PolyProcs0.bpl(21,30): Error: invalid type for argument 1 in call to FieldAccess
PolyProcs0.bpl(21,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
PolyProcs0.bpl(25,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int)
PolyProcs0.bpl(26,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
-PolyProcs0.bpl(41,35): Error: invalid type for argument 1 in call forall to injective: Field int (expected: ref)
-7 type checking errors detected in PolyProcs0.bpl
+6 type checking errors detected in PolyProcs0.bpl
TypeSynonyms0.bpl(9,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
TypeSynonyms0.bpl(10,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
TypeSynonyms0.bpl(12,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
diff --git a/Test/test20/PolyProcs0.bpl b/Test/test20/PolyProcs0.bpl
index 609f1167..06d4206c 100644
--- a/Test/test20/PolyProcs0.bpl
+++ b/Test/test20/PolyProcs0.bpl
@@ -30,15 +30,4 @@ procedure injective<b>(heap : <a>[ref, Field a]a, obj0 : ref, obj1 : ref, f : Fi
requires obj0 != obj1;
ensures heap[obj0, f] != heap[obj1, f];
-procedure testCallForall(heap : <a>[ref, Field a]a) {
- var f1 : Field int; var f2 : Field bool;
-
- start:
- call forall injective(heap, *, *, f1);
- call forall injective(heap, *, *, f2);
- call forall injective(heap, *, *, *);
-
- call forall injective(heap, *, f1, *); // error: wrong argument type
-}
-
type ref;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 11:04:26 +0000