diff options
| -rw-r--r-- | Source/AIFramework/CommonFunctionSymbols.ssc | 2 | ||||
| -rw-r--r-- | Source/Core/Absy.ssc | 23 | ||||
| -rw-r--r-- | Source/Core/AbsyExpr.ssc | 8 | ||||
| -rw-r--r-- | Source/Core/AbsyQuant.ssc | 5 | ||||
| -rw-r--r-- | Source/Core/LambdaHelper.ssc | 64 | ||||
| -rw-r--r-- | Source/Core/ResolutionContext.ssc | 25 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.ssc | 5 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 62 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.ssc | 22 | ||||
| -rw-r--r-- | Source/Dafny/Parser.ssc | 611 | ||||
| -rw-r--r-- | Source/Dafny/Printer.ssc | 25 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 63 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.ssc | 188 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 125 | ||||
| -rw-r--r-- | Test/test2/Answer | 214 | ||||
| -rw-r--r-- | Test/test2/LambdaPoly.bpl | 22 | ||||
| -rw-r--r-- | Util/Emacs/boogie-mode.el | 2 | ||||
| -rw-r--r-- | Util/latex/boogie.sty | 2 |
18 files changed, 811 insertions, 657 deletions
diff --git a/Source/AIFramework/CommonFunctionSymbols.ssc b/Source/AIFramework/CommonFunctionSymbols.ssc index f014e963..e05e8dac 100644 --- a/Source/AIFramework/CommonFunctionSymbols.ssc +++ b/Source/AIFramework/CommonFunctionSymbols.ssc @@ -614,6 +614,7 @@ namespace Microsoft.AbstractInterpretationFramework private static readonly FunctionSymbol! _implies = new FunctionSymbol("==>", binproptype);
private static readonly FunctionSymbol! _exists = new FunctionSymbol("Exists", quantifiertype);
private static readonly FunctionSymbol! _forall = new FunctionSymbol("Forall", quantifiertype);
+ private static readonly FunctionSymbol! _lambda = new FunctionSymbol("Lambda", quantifiertype);
[Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! False { get { return _false; } }
@@ -624,6 +625,7 @@ namespace Microsoft.AbstractInterpretationFramework [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Implies { get { return _implies; } }
[Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Exists { get { return _exists; } }
[Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Forall { get { return _forall; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Lambda { get { return _lambda; } }
/// <summary>
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index e83ca683..6b4cae62 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -1071,28 +1071,6 @@ namespace Microsoft.Boogie }
}
- // A generic variable. It is used for the LoopInvariantsOnDemand
- public class SimpleVariable : Variable
- {
- public SimpleVariable(IToken! tok, TypedIdent! typedIdent)
- {
- base(tok, typedIdent); // here for aesthetic reasons
- }
-
- public override bool IsMutable
- {
- get
- {
- return false;
- }
- }
-
- public override void Register(ResolutionContext! rc)
- {
- rc.AddVariable(this, false);
- }
- }
-
public abstract class DeclWithFormals : NamedDeclaration
{
public TypeVariableSeq! TypeParameters;
@@ -2228,7 +2206,6 @@ namespace Microsoft.Boogie }
public override void Resolve(ResolutionContext! rc)
{
-// this.Type.Resolve(rc);
// NOTE: WhereExpr needs to be resolved by the caller, because the caller must provide a modified ResolutionContext
this.Type = this.Type.ResolveType(rc);
}
diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc index ab834cb2..776ff8b3 100644 --- a/Source/Core/AbsyExpr.ssc +++ b/Source/Core/AbsyExpr.ssc @@ -565,7 +565,7 @@ namespace Microsoft.Boogie public class IdentifierExpr : Expr
{
- public string! Name; // identifier symbol
+ public string! Name; // identifier symbol
public Variable Decl; // identifier declaration
/// <summary>
@@ -643,10 +643,10 @@ namespace Microsoft.Boogie return;
}
Decl = rc.LookUpVariable(Name);
- if (rc.StateMode == ResolutionContext.State.StateLess && Decl is GlobalVariable) {
- rc.Error(this, "cannot refer to a global variable in this context: {0}", Name);
- } else if (Decl == null) {
+ if (Decl == null) {
rc.Error(this, "undeclared identifier: {0}", Name);
+ } else if (rc.StateMode == ResolutionContext.State.StateLess && Decl is GlobalVariable) {
+ rc.Error(this, "cannot refer to a global variable in this context: {0}", Name);
}
if (Type != null) {
Type = Type.ResolveType(rc);
diff --git a/Source/Core/AbsyQuant.ssc b/Source/Core/AbsyQuant.ssc index ec98a85c..7515d37d 100644 --- a/Source/Core/AbsyQuant.ssc +++ b/Source/Core/AbsyQuant.ssc @@ -770,8 +770,7 @@ namespace Microsoft.Boogie foreach (TypeVariable! v in unmentionedParameters) {
if (!freeVars[v])
tc.Error(tr,
- "trigger does not mention {0}, which does not " +
- "occur in variables types either",
+ "trigger does not mention {0}, which does not occur in variables types either",
v);
}
}
@@ -845,7 +844,7 @@ namespace Microsoft.Boogie public override AI.IFunctionSymbol! FunctionSymbol
{
get {
- return AI.Prop.Exists;
+ return AI.Prop.Lambda;
}
}
diff --git a/Source/Core/LambdaHelper.ssc b/Source/Core/LambdaHelper.ssc index 716ea7ae..0adebd5c 100644 --- a/Source/Core/LambdaHelper.ssc +++ b/Source/Core/LambdaHelper.ssc @@ -19,6 +19,17 @@ namespace Microsoft.Boogie { node = v.Visit(node);
axioms = v.lambdaAxioms;
functions = v.lambdaFunctions;
+ if (CommandLineOptions.Clo.TraceVerify) {
+ Console.WriteLine("Desugaring of lambda expressions produced {0} functions and {1} axioms:", functions.Count, axioms.Count);
+ TokenTextWriter wr = new TokenTextWriter("<console>", Console.Out);
+ foreach (Function f in functions) {
+ f.Emit(wr, 0);
+ }
+ foreach (Expr ax in axioms) {
+ ax.Emit(wr);
+ Console.WriteLine();
+ }
+ }
return node;
}
@@ -74,9 +85,16 @@ namespace Microsoft.Boogie { ExprSeq callArgs = new ExprSeq();
ExprSeq axCallArgs = new ExprSeq();
VariableSeq dummies = new VariableSeq(lambda.Dummies);
-
+ TypeVariableSeq freeTypeVars = new TypeVariableSeq();
+ List<Type!> fnTypeVarActuals = new List<Type!>();
+ TypeVariableSeq freshTypeVars = new TypeVariableSeq(); // these are only used in the lambda@n function's definition
foreach (object o in freeVars) {
- Variable v = o as Variable;
+ // 'o' is either a Variable or a TypeVariable. Since the lambda desugaring happens only
+ // at the outermost level of a program (where there are no mutable variables) and, for
+ // procedure bodies, after the statements have been passified (when mutable variables have
+ // been replaced by immutable incarnations), we are interested only in BoundVar's and
+ // TypeVariable's.
+ BoundVariable v = o as BoundVariable;
if (v != null) {
TypedIdent ti = new TypedIdent(v.TypedIdent.tok, v.TypedIdent.Name, v.TypedIdent.Type);
Formal f = new Formal(v.tok, ti, true);
@@ -87,15 +105,20 @@ namespace Microsoft.Boogie { Expr! id = new IdentifierExpr(f.tok, b);
subst.Add(v, id);
axCallArgs.Add(id);
+ } else if (o is TypeVariable) {
+ TypeVariable tv = (TypeVariable)o;
+ freeTypeVars.Add(tv);
+ fnTypeVarActuals.Add(tv);
+ freshTypeVars.Add(new TypeVariable(tv.tok, tv.Name));
}
- // TODO: do something about type variables
}
-
+
Formal res = new Formal(tok, new TypedIdent(tok, TypedIdent.NoName, (!)lambda.Type), false);
- Function fn = new Function(tok, "lambda@" + lambdaid++, new TypeVariableSeq(), formals, res, "auto-generated lambda function", lambda.Attributes);
- IdentifierExpr callId = new IdentifierExpr(tok, fn.Name);
- FunctionCall fcall = new FunctionCall(callId);
- fcall.Func = fn;
+ Function fn = new Function(tok, "lambda@" + lambdaid++, freshTypeVars, formals, res, "auto-generated lambda function", lambda.Attributes);
+ lambdaFunctions.Add(fn);
+
+ FunctionCall fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name));
+ fcall.Func = fn; // resolve here
List<Expr!> selectArgs = new List<Expr!>();
foreach (Variable! v in lambda.Dummies) {
@@ -103,25 +126,28 @@ namespace Microsoft.Boogie { }
NAryExpr axcall = new NAryExpr(tok, fcall, axCallArgs);
axcall.Type = res.TypedIdent.Type;
- axcall.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ axcall.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals);
NAryExpr select = Expr.Select(axcall, selectArgs);
select.Type = lambda.Body.Type;
- select.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ List<Type!> selectTypeParamActuals = new List<Type!>();
+ TypeVariableSeq forallTypeVariables = new TypeVariableSeq();
+ foreach (TypeVariable! tp in lambda.TypeParameters) {
+ selectTypeParamActuals.Add(tp);
+ forallTypeVariables.Add(tp);
+ }
+ forallTypeVariables.AddRange(freeTypeVars);
+ select.TypeParameters = SimpleTypeParamInstantiation.From(lambda.TypeParameters, selectTypeParamActuals);
- Expr body = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambda.Body);
- body = Expr.Eq(select, body);
+ Expr bb = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), lambda.Body);
+ NAryExpr body = Expr.Eq(select, bb);
body.Type = Type.Bool;
- ((NAryExpr)body).TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ body.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
Trigger trig = new Trigger(select.tok, true, new ExprSeq(select));
-
- body = new ForallExpr(tok, lambda.TypeParameters, dummies, lambda.Attributes, trig, body);
-
- lambdaFunctions.Add(fn);
- lambdaAxioms.Add(body);
+ lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies, lambda.Attributes, trig, body));
NAryExpr call = new NAryExpr(tok, fcall, callArgs);
call.Type = res.TypedIdent.Type;
- call.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ call.TypeParameters = SimpleTypeParamInstantiation.From(freeTypeVars, fnTypeVarActuals);
return call;
}
diff --git a/Source/Core/ResolutionContext.ssc b/Source/Core/ResolutionContext.ssc index 618f4a3a..bb1fc7c6 100644 --- a/Source/Core/ResolutionContext.ssc +++ b/Source/Core/ResolutionContext.ssc @@ -124,14 +124,18 @@ namespace Microsoft.Boogie // user-defined types, which can be either TypeCtorDecl or TypeSynonymDecl
Hashtable /*string->NamedDeclaration*/! types = new Hashtable /*string->NamedDeclaration*/ ();
- private void CheckBvNameClashes(Absy! absy, string! name) {
+ /// <summary>
+ /// Checks if name coincides with the name of a bitvector type. If so, reports an error and
+ /// returns true; otherwise, returns false.
+ /// </summary>
+ private bool CheckBvNameClashes(Absy! absy, string! name) {
if (name.StartsWith("bv") && name.Length > 2) {
- bool isBv = true;
for (int i = 2; i < name.Length; ++i)
- if (!char.IsDigit(name[i])) isBv = false;
- if (isBv)
- Error(absy, "type name: {0} is registered for bitvectors", name);
+ if (!char.IsDigit(name[i])) return false;
+ Error(absy, "type name: {0} is registered for bitvectors", name);
+ return true;
}
+ return false;
}
public void AddType(NamedDeclaration! td)
@@ -139,7 +143,8 @@ namespace Microsoft.Boogie assert (td is TypeCtorDecl) || (td is TypeSynonymDecl);
string! name = (!)td.Name;
- CheckBvNameClashes(td, name);
+ if (CheckBvNameClashes(td, name))
+ return; // error has already been reported
if (types[name] != null)
{
@@ -174,10 +179,12 @@ namespace Microsoft.Boogie List<TypeVariable!>! typeBinders = new List<TypeVariable!>(5);
public void AddTypeBinder(TypeVariable! td) {
- CheckBvNameClashes(td, td.Name);
+ if (CheckBvNameClashes(td, td.Name)) {
+ return;
+ }
if (types.ContainsKey(td.Name)) {
- Error(td, "name is already reserved for type constructor: {0}", td.Name);
- return;
+ Error(td, "name is already reserved for type constructor: {0}", td.Name);
+ return;
}
for (int i = 0; i < typeBinders.Count; i++) {
if (typeBinders[i].Name == td.Name) {
diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc index 6e50f6db..e476e41b 100644 --- a/Source/Core/StandardVisitor.ssc +++ b/Source/Core/StandardVisitor.ssc @@ -274,11 +274,6 @@ namespace Microsoft.Boogie node = (GlobalVariable) this.VisitVariable(node);
return node;
}
- public virtual SimpleVariable! VisitSimpleVariable(SimpleVariable! node)
- {
- node = (SimpleVariable) this.VisitSimpleVariable(node);
- return node;
- }
public virtual GotoCmd! VisitGotoCmd(GotoCmd! node)
{
node.labelTargets = this.VisitBlockSeq((!)node.labelTargets);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 6e3b68da..aff1deb7 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -22,6 +22,7 @@ static List<ModuleDecl!>! theModules = new List<ModuleDecl!>(); static Expression! dummyExpr = new LiteralExpr(Token.NoToken);
+static FrameExpression! dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement! dummyStmt = new ReturnStmt(Token.NoToken);
static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg");
static Scope<string>! parseVarScope = new Scope<string>();
@@ -94,7 +95,7 @@ public static int Parse (List<ModuleDecl!>! modules) { CHARACTERS
letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
digit = "0123456789".
- special = "'_?`\\".
+ special = "'_?\\".
glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
cr = '\r'.
@@ -296,7 +297,7 @@ MethodDecl<MemberModifiers mmod, out Method! m> List<Formal!> ins = new List<Formal!>();
List<Formal!> outs = new List<Formal!>();
List<MaybeFreeExpression!> req = new List<MaybeFreeExpression!>();
- List<Expression!> mod = new List<Expression!>();
+ List<FrameExpression!> mod = new List<FrameExpression!>();
List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
List<Expression!> dec = new List<Expression!>();
Statement! bb; BlockStmt body = null;
@@ -322,12 +323,12 @@ MethodDecl<MemberModifiers mmod, out Method! m> .)
.
-MethodSpec<List<MaybeFreeExpression!\>! req, List<Expression!\>! mod, List<MaybeFreeExpression!\>! ens,
+MethodSpec<List<MaybeFreeExpression!\>! req, List<FrameExpression!\>! mod, List<MaybeFreeExpression!\>! ens,
List<Expression!\>! decreases>
-= (. Expression! e; bool isFree = false;
+= (. Expression! e; FrameExpression! fe; bool isFree = false;
.)
- ( "modifies" [ Expression<out e> (. mod.Add(e); .)
- { "," Expression<out e> (. mod.Add(e); .)
+ ( "modifies" [ FrameExpression<out fe> (. mod.Add(fe); .)
+ { "," FrameExpression<out fe> (. mod.Add(fe); .)
}
] ";"
| [ "free" (. isFree = true; .)
@@ -419,7 +420,7 @@ FunctionDecl<MemberModifiers mmod, out Function! f> List<Formal!> formals = new List<Formal!>();
Type! returnType;
List<Expression!> reqs = new List<Expression!>();
- List<Expression!> reads = new List<Expression!>();
+ List<FrameExpression!> reads = new List<FrameExpression!>();
List<Expression!> decreases = new List<Expression!>();
Expression! bb; Expression body = null;
bool isFunctionMethod = false;
@@ -446,37 +447,48 @@ FunctionDecl<MemberModifiers mmod, out Function! f> .)
.
-FunctionSpec<List<Expression!\>! reqs, List<Expression!\>! reads, List<Expression!\>! decreases>
-= (. Expression! e; .)
+FunctionSpec<List<Expression!\>! reqs, List<FrameExpression!\>! reads, List<Expression!\>! decreases>
+= (. Expression! e; FrameExpression! fe; .)
( "requires" Expression<out e> ";" (. reqs.Add(e); .)
- | "reads" [ PossiblyWildExpressions<reads> ] ";"
+ | "reads" [ PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
+ { "," PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
+ }
+ ] ";"
| "decreases" Expressions<decreases> ";"
)
.
-PossiblyWildExpressions<List<Expression!\>! args>
-= (. Expression! e; .)
- PossiblyWildExpression<out e> (. args.Add(e); .)
- { "," PossiblyWildExpression<out e> (. args.Add(e); .)
- }
- .
-
PossiblyWildExpression<out Expression! e>
= (. e = dummyExpr; .)
+ /* A decreases clause on a loop asks that no termination check be performed.
+ * Use of this feature is sound only with respect to partial correctness.
+ */
+ ( "*" (. e = new WildcardExpr(token); .)
+ | Expression<out e>
+ )
+ .
+
+PossiblyWildFrameExpression<out FrameExpression! fe>
+= (. fe = dummyFrameExpr; .)
/* A reads clause can list a wildcard, which allows the enclosing function to
* read anything. In many cases, and in particular in all cases where
* the function is defined recursively, this makes it next to impossible to make
* any use of the function. Nevertheless, as an experimental feature, the
* language allows it (and it is sound).
*/
- /* A decreases clause on a loop asks that no termination check be performed.
- * Use of this feature is sound only with respect to partial correctness.
- */
- ( "*" (. e = new WildcardExpr(token); .)
- | Expression<out e>
+ ( "*" (. fe = new FrameExpression(new WildcardExpr(token), null); .)
+ | FrameExpression<out fe>
)
.
+FrameExpression<out FrameExpression! fe>
+= (. Expression! e; Token! id; string fieldName = null; .)
+ Expression<out e>
+ [ "`" Ident<out id> (. fieldName = id.val; .)
+ ]
+ (. fe = new FrameExpression(e, fieldName); .)
+ .
+
FunctionBody<out Expression! e>
= (. e = dummyExpr; .)
"{"
@@ -676,7 +688,11 @@ WhileStmt<out Statement! stmt> "invariant"
Expression<out e> (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
";"
- | "decreases" PossiblyWildExpressions<decreases> ";"
+ | "decreases"
+ PossiblyWildExpression<out e> (. decreases.Add(e); .)
+ { "," PossiblyWildExpression<out e> (. decreases.Add(e); .)
+ }
+ ";"
}
BlockStmt<out body> (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)
.
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index dc787503..55e76d30 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -527,12 +527,12 @@ namespace Microsoft.Dafny public readonly List<Formal!>! Formals;
public readonly Type! ResultType;
public readonly List<Expression!>! Req;
- public readonly List<Expression!>! Reads;
+ public readonly List<FrameExpression!>! Reads;
public readonly List<Expression!>! Decreases;
public readonly Expression Body; // an extended expression
public Function(Token! tok, string! name, bool isStatic, bool isGhost, bool isUnlimited, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,
- List<Expression!>! req, List<Expression!>! reads, List<Expression!>! decreases, Expression body, Attributes attributes) {
+ List<Expression!>! req, List<FrameExpression!>! reads, List<Expression!>! decreases, Expression body, Attributes attributes) {
this.IsStatic = isStatic;
this.IsGhost = isGhost;
this.IsUnlimited = isUnlimited;
@@ -554,7 +554,7 @@ namespace Microsoft.Dafny public readonly List<Formal!>! Ins;
public readonly List<Formal!>! Outs;
public readonly List<MaybeFreeExpression!>! Req;
- public readonly List<Expression!>! Mod;
+ public readonly List<FrameExpression!>! Mod;
public readonly List<MaybeFreeExpression!>! Ens;
public readonly List<Expression!>! Decreases;
public readonly BlockStmt Body;
@@ -563,7 +563,7 @@ namespace Microsoft.Dafny bool isStatic, bool isGhost,
[Captured] List<TypeParameter!>! typeArgs,
[Captured] List<Formal!>! ins, [Captured] List<Formal!>! outs,
- [Captured] List<MaybeFreeExpression!>! req, [Captured] List<Expression!>! mod, [Captured] List<MaybeFreeExpression!>! ens,
+ [Captured] List<MaybeFreeExpression!>! req, [Captured] List<FrameExpression!>! mod, [Captured] List<MaybeFreeExpression!>! ens,
[Captured] List<Expression!>! decreases,
[Captured] BlockStmt body,
Attributes attributes) {
@@ -1275,4 +1275,18 @@ namespace Microsoft.Dafny IsFree = isFree;
}
}
+
+ public class FrameExpression {
+ public readonly Expression! E; // may be a WildcardExpr
+ public readonly string FieldName;
+ public Field Field; // filled in during resolution (but is null if FieldName is)
+ invariant E is WildcardExpr ==> FieldName == null && Field == null;
+
+ public FrameExpression(Expression! e, string fieldName)
+ requires e is WildcardExpr ==> fieldName == null;
+ {
+ E = e;
+ FieldName = fieldName;
+ }
+ }
}
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index e0660c65..ee979045 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -6,7 +6,7 @@ using Microsoft.Contracts; namespace Microsoft.Dafny {
public class Parser {
- const int maxT = 98;
+ const int maxT = 99;
const bool T = true;
const bool x = false;
@@ -20,6 +20,7 @@ public class Parser { static Expression! dummyExpr = new LiteralExpr(Token.NoToken);
+static FrameExpression! dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement! dummyStmt = new ReturnStmt(Token.NoToken);
static Attributes.Argument! dummyAttrArg = new Attributes.Argument("dummyAttrArg");
static Scope<string>! parseVarScope = new Scope<string>();
@@ -285,7 +286,7 @@ public static int Parse (List<ModuleDecl!>! modules) { } else if (t.kind == 19) {
MethodDecl(mmod, out m);
mm.Add(m);
- } else Error(99);
+ } else Error(100);
}
static void GenericParameters(List<TypeParameter!>! typeArgs) {
@@ -329,7 +330,7 @@ public static int Parse (List<ModuleDecl!>! modules) { List<Formal!> formals = new List<Formal!>();
Type! returnType;
List<Expression!> reqs = new List<Expression!>();
- List<Expression!> reads = new List<Expression!>();
+ List<FrameExpression!> reads = new List<FrameExpression!>();
List<Expression!> decreases = new List<Expression!>();
Expression! bb; Expression body = null;
bool isFunctionMethod = false;
@@ -363,7 +364,7 @@ public static int Parse (List<ModuleDecl!>! modules) { }
FunctionBody(out bb);
body = bb;
- } else Error(100);
+ } else Error(101);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
@@ -376,7 +377,7 @@ public static int Parse (List<ModuleDecl!>! modules) { List<Formal!> ins = new List<Formal!>();
List<Formal!> outs = new List<Formal!>();
List<MaybeFreeExpression!> req = new List<MaybeFreeExpression!>();
- List<Expression!> mod = new List<Expression!>();
+ List<FrameExpression!> mod = new List<FrameExpression!>();
List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
List<Expression!> dec = new List<Expression!>();
Statement! bb; BlockStmt body = null;
@@ -408,7 +409,7 @@ public static int Parse (List<ModuleDecl!>! modules) { }
BlockStmt(out bb);
body = (BlockStmt)bb;
- } else Error(101);
+ } else Error(102);
parseVarScope.PopMarker();
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -540,7 +541,7 @@ public static int Parse (List<ModuleDecl!>! modules) { } else if (t.kind == 1 || t.kind == 32) {
ReferenceType(out tok, out ty);
- } else Error(102);
+ } else Error(103);
}
static void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {
@@ -558,19 +559,19 @@ public static int Parse (List<ModuleDecl!>! modules) { Expect(27);
}
- static void MethodSpec(List<MaybeFreeExpression!>! req, List<Expression!>! mod, List<MaybeFreeExpression!>! ens,
+ static void MethodSpec(List<MaybeFreeExpression!>! req, List<FrameExpression!>! mod, List<MaybeFreeExpression!>! ens,
List<Expression!>! decreases) {
- Expression! e; bool isFree = false;
+ Expression! e; FrameExpression! fe; bool isFree = false;
if (t.kind == 21) {
Get();
if (StartOf(7)) {
- Expression(out e);
- mod.Add(e);
+ FrameExpression(out fe);
+ mod.Add(fe);
while (t.kind == 15) {
Get();
- Expression(out e);
- mod.Add(e);
+ FrameExpression(out fe);
+ mod.Add(fe);
}
}
Expect(13);
@@ -589,12 +590,12 @@ List<Expression!>! decreases) { Expression(out e);
Expect(13);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(103);
+ } else Error(104);
} else if (t.kind == 25) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(104);
+ } else Error(105);
}
static void BlockStmt(out Statement! block) {
@@ -613,22 +614,33 @@ List<Expression!>! decreases) { parseVarScope.PopMarker();
}
+ static void FrameExpression(out FrameExpression! fe) {
+ Expression! e; Token! id; string fieldName = null;
+ Expression(out e);
+ if (t.kind == 36) {
+ Get();
+ Ident(out id);
+ fieldName = id.val;
+ }
+ fe = new FrameExpression(e, fieldName);
+ }
+
static void Expression(out Expression! e) {
Token! x; Expression! e0; Expression! e1 = dummyExpr;
e = dummyExpr;
- if (t.kind == 45) {
+ if (t.kind == 46) {
Get();
x = token;
Expression(out e);
- Expect(57);
+ Expect(58);
Expression(out e0);
- Expect(46);
+ Expect(47);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(9)) {
EquivExpression(out e);
- } else Error(105);
+ } else Error(106);
}
static void Expressions(List<Expression!>! args) {
@@ -669,11 +681,11 @@ List<Expression!>! decreases) { GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else Error(106);
+ } else Error(107);
}
- static void FunctionSpec(List<Expression!>! reqs, List<Expression!>! reads, List<Expression!>! decreases) {
- Expression! e;
+ static void FunctionSpec(List<Expression!>! reqs, List<FrameExpression!>! reads, List<Expression!>! decreases) {
+ Expression! e; FrameExpression! fe;
if (t.kind == 23) {
Get();
Expression(out e);
@@ -682,36 +694,41 @@ List<Expression!>! decreases) { } else if (t.kind == 34) {
Get();
if (StartOf(10)) {
- PossiblyWildExpressions(reads);
+ PossiblyWildFrameExpression(out fe);
+ reads.Add(fe);
+ while (t.kind == 15) {
+ Get();
+ PossiblyWildFrameExpression(out fe);
+ reads.Add(fe);
+ }
}
Expect(13);
} else if (t.kind == 25) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(107);
+ } else Error(108);
}
static void FunctionBody(out Expression! e) {
e = dummyExpr;
Expect(6);
- if (t.kind == 36) {
+ if (t.kind == 37) {
MatchExpression(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(108);
+ } else Error(109);
Expect(7);
}
- static void PossiblyWildExpressions(List<Expression!>! args) {
- Expression! e;
- PossiblyWildExpression(out e);
- args.Add(e);
- while (t.kind == 15) {
+ static void PossiblyWildFrameExpression(out FrameExpression! fe) {
+ fe = dummyFrameExpr;
+ if (t.kind == 35) {
Get();
- PossiblyWildExpression(out e);
- args.Add(e);
- }
+ fe = new FrameExpression(new WildcardExpr(token), null);
+ } else if (StartOf(7)) {
+ FrameExpression(out fe);
+ } else Error(110);
}
static void PossiblyWildExpression(out Expression! e) {
@@ -721,17 +738,17 @@ List<Expression!>! decreases) { e = new WildcardExpr(token);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(109);
+ } else Error(111);
}
static void MatchExpression(out Expression! e) {
Token! x; MatchCaseExpr! c;
List<MatchCaseExpr!> cases = new List<MatchCaseExpr!>();
- Expect(36);
+ Expect(37);
x = token;
Expression(out e);
- while (t.kind == 37) {
+ while (t.kind == 38) {
CaseExpression(out c);
cases.Add(c);
}
@@ -743,7 +760,7 @@ List<Expression!>! decreases) { List<BoundVar!> arguments = new List<BoundVar!>();
Expression! body;
- Expect(37);
+ Expect(38);
x = token; parseVarScope.PushMarker();
Ident(out id);
if (t.kind == 26) {
@@ -759,7 +776,7 @@ List<Expression!>! decreases) { }
Expect(27);
}
- Expect(38);
+ Expect(39);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
parseVarScope.PopMarker();
@@ -776,7 +793,7 @@ List<Expression!>! decreases) { ss.Add(s);
} else if (t.kind == 9 || t.kind == 14) {
VarDeclStmts(ss);
- } else Error(110);
+ } else Error(112);
}
static void OneStmt(out Statement! s) {
@@ -784,51 +801,51 @@ List<Expression!>! decreases) { s = dummyStmt; /* to please the compiler */
switch (t.kind) {
- case 53: {
+ case 54: {
AssertStmt(out s);
break;
}
- case 54: {
+ case 55: {
AssumeStmt(out s);
break;
}
- case 55: {
+ case 56: {
UseStmt(out s);
break;
}
- case 56: {
+ case 57: {
PrintStmt(out s);
break;
}
- case 1: case 26: case 90: case 91: {
+ case 1: case 26: case 91: case 92: {
AssignStmt(out s);
break;
}
- case 44: {
+ case 45: {
HavocStmt(out s);
break;
}
- case 49: {
+ case 50: {
CallStmt(out s);
break;
}
- case 45: {
+ case 46: {
IfStmt(out s);
break;
}
- case 47: {
+ case 48: {
WhileStmt(out s);
break;
}
- case 36: {
+ case 37: {
MatchStmt(out s);
break;
}
- case 50: {
+ case 51: {
ForeachStmt(out s);
break;
}
- case 39: {
+ case 40: {
Get();
x = token;
Ident(out id);
@@ -836,7 +853,7 @@ List<Expression!>! decreases) { s = new LabelStmt(x, id.val);
break;
}
- case 40: {
+ case 41: {
Get();
x = token;
if (t.kind == 1) {
@@ -847,14 +864,14 @@ List<Expression!>! decreases) { s = new BreakStmt(x, label);
break;
}
- case 41: {
+ case 42: {
Get();
x = token;
Expect(13);
s = new ReturnStmt(x);
break;
}
- default: Error(111); break;
+ default: Error(113); break;
}
}
@@ -877,7 +894,7 @@ List<Expression!>! decreases) { static void AssertStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(53);
+ Expect(54);
x = token;
Expression(out e);
Expect(13);
@@ -886,7 +903,7 @@ List<Expression!>! decreases) { static void AssumeStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(54);
+ Expect(55);
x = token;
Expression(out e);
Expect(13);
@@ -895,7 +912,7 @@ List<Expression!>! decreases) { static void UseStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(55);
+ Expect(56);
x = token;
Expression(out e);
Expect(13);
@@ -906,7 +923,7 @@ List<Expression!>! decreases) { Token! x; Attributes.Argument! arg;
List<Attributes.Argument!> args = new List<Attributes.Argument!>();
- Expect(56);
+ Expect(57);
x = token;
AttributeArg(out arg);
args.Add(arg);
@@ -927,7 +944,7 @@ List<Expression!>! decreases) { s = dummyStmt;
LhsExpr(out lhs);
- Expect(42);
+ Expect(43);
x = token;
AssignRhs(out rhs, out ty);
if (rhs != null) {
@@ -942,7 +959,7 @@ List<Expression!>! decreases) { static void HavocStmt(out Statement! s) {
Token! x; Expression! lhs;
- Expect(44);
+ Expect(45);
x = token;
LhsExpr(out lhs);
Expect(13);
@@ -955,10 +972,10 @@ List<Expression!>! decreases) { List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();
- Expect(49);
+ Expect(50);
x = token;
CallStmtSubExpr(out e);
- if (t.kind == 15 || t.kind == 42) {
+ if (t.kind == 15 || t.kind == 43) {
if (t.kind == 15) {
Get();
e = ConvertToLocal(e);
@@ -977,7 +994,7 @@ List<Expression!>! decreases) { Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
- Expect(42);
+ Expect(43);
CallStmtSubExpr(out e);
} else {
Get();
@@ -1011,19 +1028,19 @@ List<Expression!>! decreases) { Statement! s;
Statement els = null;
- Expect(45);
+ Expect(46);
x = token;
Guard(out guard);
BlockStmt(out thn);
- if (t.kind == 46) {
+ if (t.kind == 47) {
Get();
- if (t.kind == 45) {
+ if (t.kind == 46) {
IfStmt(out s);
els = s;
} else if (t.kind == 6) {
BlockStmt(out s);
els = s;
- } else Error(112);
+ } else Error(114);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -1036,24 +1053,30 @@ List<Expression!>! decreases) { List<Expression!> decreases = new List<Expression!>();
Statement! body;
- Expect(47);
+ Expect(48);
x = token;
Guard(out guard);
assume guard == null || Owner.None(guard);
- while (t.kind == 22 || t.kind == 25 || t.kind == 48) {
- if (t.kind == 22 || t.kind == 48) {
+ while (t.kind == 22 || t.kind == 25 || t.kind == 49) {
+ if (t.kind == 22 || t.kind == 49) {
isFree = false;
if (t.kind == 22) {
Get();
isFree = true;
}
- Expect(48);
+ Expect(49);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(13);
} else {
Get();
- PossiblyWildExpressions(decreases);
+ PossiblyWildExpression(out e);
+ decreases.Add(e);
+ while (t.kind == 15) {
+ Get();
+ PossiblyWildExpression(out e);
+ decreases.Add(e);
+ }
Expect(13);
}
}
@@ -1064,11 +1087,11 @@ List<Expression!>! decreases) { static void MatchStmt(out Statement! s) {
Token x; Expression! e; MatchCaseStmt! c;
List<MatchCaseStmt!> cases = new List<MatchCaseStmt!>();
- Expect(36);
+ Expect(37);
x = token;
Expression(out e);
Expect(6);
- while (t.kind == 37) {
+ while (t.kind == 38) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1085,7 +1108,7 @@ List<Expression!>! decreases) { AssignStmt bodyAssign = null;
parseVarScope.PushMarker();
- Expect(50);
+ Expect(51);
x = token;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
@@ -1096,20 +1119,20 @@ List<Expression!>! decreases) { Get();
Type(out ty);
}
- Expect(51);
+ Expect(52);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (t.kind == 52) {
+ if (t.kind == 53) {
Get();
Expression(out range);
}
Expect(27);
Expect(6);
- while (t.kind == 53 || t.kind == 54 || t.kind == 55) {
- if (t.kind == 53) {
+ while (t.kind == 54 || t.kind == 55 || t.kind == 56) {
+ if (t.kind == 54) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (t.kind == 54) {
+ } else if (t.kind == 55) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1120,10 +1143,10 @@ List<Expression!>! decreases) { if (StartOf(12)) {
AssignStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (t.kind == 44) {
+ } else if (t.kind == 45) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(113);
+ } else Error(115);
Expect(7);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1142,14 +1165,14 @@ List<Expression!>! decreases) { Token! x; Expression! ee; Type! tt;
e = null; ty = null;
- if (t.kind == 43) {
+ if (t.kind == 44) {
Get();
ReferenceType(out x, out tt);
ty = tt;
} else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(114);
+ } else Error(116);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -1157,10 +1180,10 @@ List<Expression!>! decreases) { Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 90 || t.kind == 91) {
+ } else if (t.kind == 26 || t.kind == 91 || t.kind == 92) {
ObjectExpression(out e);
- } else Error(115);
- while (t.kind == 85 || t.kind == 87) {
+ } else Error(117);
+ while (t.kind == 86 || t.kind == 88) {
SelectOrCallSuffix(ref e);
}
}
@@ -1176,7 +1199,7 @@ List<Expression!>! decreases) { Type(out ty);
optionalType = ty;
}
- if (t.kind == 42) {
+ if (t.kind == 43) {
Get();
AssignRhs(out rhs, out newType);
}
@@ -1201,7 +1224,7 @@ List<Expression!>! decreases) { } else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(116);
+ } else Error(118);
Expect(27);
}
@@ -1210,7 +1233,7 @@ List<Expression!>! decreases) { List<BoundVar!> arguments = new List<BoundVar!>();
List<Statement!> body = new List<Statement!>();
- Expect(37);
+ Expect(38);
x = token; parseVarScope.PushMarker();
Ident(out id);
if (t.kind == 26) {
@@ -1226,7 +1249,7 @@ List<Expression!>! decreases) { }
Expect(27);
}
- Expect(38);
+ Expect(39);
parseVarScope.PushMarker();
while (StartOf(8)) {
Stmt(body);
@@ -1240,11 +1263,11 @@ List<Expression!>! decreases) { e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 90 || t.kind == 91) {
+ } else if (t.kind == 26 || t.kind == 91 || t.kind == 92) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(117);
- while (t.kind == 85 || t.kind == 87) {
+ } else Error(119);
+ while (t.kind == 86 || t.kind == 88) {
SelectOrCallSuffix(ref e);
}
}
@@ -1257,13 +1280,13 @@ List<Expression!>! decreases) { } else if (StartOf(7)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else Error(118);
+ } else Error(120);
}
static void EquivExpression(out Expression! e0) {
Token! x; Expression! e1;
ImpliesExpression(out e0);
- while (t.kind == 58 || t.kind == 59) {
+ while (t.kind == 59 || t.kind == 60) {
EquivOp();
x = token;
ImpliesExpression(out e1);
@@ -1274,7 +1297,7 @@ List<Expression!>! decreases) { static void ImpliesExpression(out Expression! e0) {
Token! x; Expression! e1;
LogicalExpression(out e0);
- if (t.kind == 60 || t.kind == 61) {
+ if (t.kind == 61 || t.kind == 62) {
ImpliesOp();
x = token;
ImpliesExpression(out e1);
@@ -1283,23 +1306,23 @@ List<Expression!>! decreases) { }
static void EquivOp() {
- if (t.kind == 58) {
+ if (t.kind == 59) {
Get();
- } else if (t.kind == 59) {
+ } else if (t.kind == 60) {
Get();
- } else Error(119);
+ } else Error(121);
}
static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(13)) {
- if (t.kind == 62 || t.kind == 63) {
+ if (t.kind == 63 || t.kind == 64) {
AndOp();
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (t.kind == 62 || t.kind == 63) {
+ while (t.kind == 63 || t.kind == 64) {
AndOp();
x = token;
RelationalExpression(out e1);
@@ -1310,7 +1333,7 @@ List<Expression!>! decreases) { x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (t.kind == 64 || t.kind == 65) {
+ while (t.kind == 65 || t.kind == 66) {
OrOp();
x = token;
RelationalExpression(out e1);
@@ -1321,11 +1344,11 @@ List<Expression!>! decreases) { }
static void ImpliesOp() {
- if (t.kind == 60) {
+ if (t.kind == 61) {
Get();
- } else if (t.kind == 61) {
+ } else if (t.kind == 62) {
Get();
- } else Error(120);
+ } else Error(122);
}
static void RelationalExpression(out Expression! e0) {
@@ -1339,25 +1362,25 @@ List<Expression!>! decreases) { }
static void AndOp() {
- if (t.kind == 62) {
+ if (t.kind == 63) {
Get();
- } else if (t.kind == 63) {
+ } else if (t.kind == 64) {
Get();
- } else Error(121);
+ } else Error(123);
}
static void OrOp() {
- if (t.kind == 64) {
+ if (t.kind == 65) {
Get();
- } else if (t.kind == 65) {
+ } else if (t.kind == 66) {
Get();
- } else Error(122);
+ } else Error(124);
}
static void Term(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 75 || t.kind == 76) {
+ while (t.kind == 76 || t.kind == 77) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1367,7 +1390,7 @@ List<Expression!>! decreases) { static void RelOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (t.kind) {
- case 66: {
+ case 67: {
Get();
x = token; op = BinaryExpr.Opcode.Eq;
break;
@@ -1382,59 +1405,59 @@ List<Expression!>! decreases) { x = token; op = BinaryExpr.Opcode.Gt;
break;
}
- case 67: {
+ case 68: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 68: {
+ case 69: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- case 69: {
+ case 70: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 70: {
+ case 71: {
Get();
x = token; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 51: {
+ case 52: {
Get();
x = token; op = BinaryExpr.Opcode.In;
break;
}
- case 71: {
+ case 72: {
Get();
x = token; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 72: {
+ case 73: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 73: {
+ case 74: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 74: {
+ case 75: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(123); break;
+ default: Error(125); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 35 || t.kind == 77 || t.kind == 78) {
+ while (t.kind == 35 || t.kind == 78 || t.kind == 79) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1443,23 +1466,23 @@ List<Expression!>! decreases) { static void AddOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 75) {
+ if (t.kind == 76) {
Get();
x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 76) {
+ } else if (t.kind == 77) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(124);
+ } else Error(126);
}
static void UnaryExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 76) {
+ if (t.kind == 77) {
Get();
x = token;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 79 || t.kind == 80) {
+ } else if (t.kind == 80 || t.kind == 81) {
NegOp();
x = token;
UnaryExpression(out e);
@@ -1468,7 +1491,7 @@ List<Expression!>! decreases) { SelectExpression(out e);
} else if (StartOf(15)) {
ConstAtomExpression(out e);
- } else Error(125);
+ } else Error(127);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
@@ -1476,21 +1499,21 @@ List<Expression!>! decreases) { if (t.kind == 35) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 77) {
+ } else if (t.kind == 78) {
Get();
x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 78) {
+ } else if (t.kind == 79) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(126);
+ } else Error(128);
}
static void NegOp() {
- if (t.kind == 79) {
+ if (t.kind == 80) {
Get();
- } else if (t.kind == 80) {
+ } else if (t.kind == 81) {
Get();
- } else Error(127);
+ } else Error(129);
}
static void ConstAtomExpression(out Expression! e) {
@@ -1498,17 +1521,17 @@ List<Expression!>! decreases) { e = dummyExpr;
switch (t.kind) {
- case 81: {
+ case 82: {
Get();
e = new LiteralExpr(token, false);
break;
}
- case 82: {
+ case 83: {
Get();
e = new LiteralExpr(token, true);
break;
}
- case 83: {
+ case 84: {
Get();
e = new LiteralExpr(token);
break;
@@ -1518,11 +1541,11 @@ List<Expression!>! decreases) { e = new LiteralExpr(token, n);
break;
}
- case 84: {
+ case 85: {
Get();
x = token;
Ident(out dtName);
- Expect(85);
+ Expect(86);
Ident(out id);
elements = new List<Expression!>();
if (t.kind == 26) {
@@ -1535,7 +1558,7 @@ List<Expression!>! decreases) { e = new DatatypeValue(token, dtName.val, id.val, elements);
break;
}
- case 86: {
+ case 87: {
Get();
x = token;
Expect(26);
@@ -1544,12 +1567,12 @@ List<Expression!>! decreases) { e = new FreshExpr(x, e);
break;
}
- case 52: {
+ case 53: {
Get();
x = token;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(52);
+ Expect(53);
break;
}
case 6: {
@@ -1562,17 +1585,17 @@ List<Expression!>! decreases) { Expect(7);
break;
}
- case 87: {
+ case 88: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(7)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(88);
+ Expect(89);
break;
}
- default: Error(128); break;
+ default: Error(130); break;
}
}
@@ -1611,10 +1634,10 @@ List<Expression!>! decreases) { static void ObjectExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 90) {
+ if (t.kind == 91) {
Get();
e = new ThisExpr(token);
- } else if (t.kind == 91) {
+ } else if (t.kind == 92) {
Get();
x = token;
Expect(26);
@@ -1627,9 +1650,9 @@ List<Expression!>! decreases) { QuantifierGuts(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(129);
+ } else Error(131);
Expect(27);
- } else Error(130);
+ } else Error(132);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1637,7 +1660,7 @@ List<Expression!>! decreases) { Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 85) {
+ if (t.kind == 86) {
Get();
Ident(out id);
if (t.kind == 26) {
@@ -1650,14 +1673,14 @@ List<Expression!>! decreases) { e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 87) {
+ } else if (t.kind == 88) {
Get();
x = token;
if (StartOf(7)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 42 || t.kind == 89) {
- if (t.kind == 89) {
+ if (t.kind == 43 || t.kind == 90) {
+ if (t.kind == 90) {
Get();
anyDots = true;
if (StartOf(7)) {
@@ -1670,11 +1693,11 @@ List<Expression!>! decreases) { e1 = ee;
}
}
- } else if (t.kind == 89) {
+ } else if (t.kind == 90) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(131);
+ } else Error(133);
assert !anyDots ==> e0 != null;
if (anyDots) {
assert e0 != null || e1 != null;
@@ -1687,8 +1710,8 @@ List<Expression!>! decreases) { e = new SeqUpdateExpr(x, e, e0, e1);
}
- Expect(88);
- } else Error(132);
+ Expect(89);
+ } else Error(134);
}
static void QuantifierGuts(out Expression! q) {
@@ -1701,13 +1724,13 @@ List<Expression!>! decreases) { Triggers trigs = null;
Expression! body;
- if (t.kind == 92 || t.kind == 93) {
+ if (t.kind == 93 || t.kind == 94) {
Forall();
x = token; univ = true;
- } else if (t.kind == 94 || t.kind == 95) {
+ } else if (t.kind == 95 || t.kind == 96) {
Exists();
x = token;
- } else Error(133);
+ } else Error(135);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1731,19 +1754,19 @@ List<Expression!>! decreases) { }
static void Forall() {
- if (t.kind == 92) {
+ if (t.kind == 93) {
Get();
- } else if (t.kind == 93) {
+ } else if (t.kind == 94) {
Get();
- } else Error(134);
+ } else Error(136);
}
static void Exists() {
- if (t.kind == 94) {
+ if (t.kind == 95) {
Get();
- } else if (t.kind == 95) {
+ } else if (t.kind == 96) {
Get();
- } else Error(135);
+ } else Error(137);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -1756,16 +1779,16 @@ List<Expression!>! decreases) { es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(136);
+ } else Error(138);
Expect(7);
}
static void QSep() {
- if (t.kind == 96) {
+ if (t.kind == 97) {
Get();
- } else if (t.kind == 97) {
+ } else if (t.kind == 98) {
Get();
- } else Error(137);
+ } else Error(139);
}
static void AttributeBody(ref Attributes attrs) {
@@ -1840,108 +1863,110 @@ List<Expression!>! decreases) { case 33: s = "function expected"; break;
case 34: s = "reads expected"; break;
case 35: s = "* expected"; break;
- case 36: s = "match expected"; break;
- case 37: s = "case expected"; break;
- case 38: s = "=> expected"; break;
- case 39: s = "label expected"; break;
- case 40: s = "break expected"; break;
- case 41: s = "return expected"; break;
- case 42: s = ":= expected"; break;
- case 43: s = "new expected"; break;
- case 44: s = "havoc expected"; break;
- case 45: s = "if expected"; break;
- case 46: s = "else expected"; break;
- case 47: s = "while expected"; break;
- case 48: s = "invariant expected"; break;
- case 49: s = "call expected"; break;
- case 50: s = "foreach expected"; break;
- case 51: s = "in expected"; break;
- case 52: s = "| expected"; break;
- case 53: s = "assert expected"; break;
- case 54: s = "assume expected"; break;
- case 55: s = "use expected"; break;
- case 56: s = "print expected"; break;
- case 57: s = "then expected"; break;
- case 58: s = "<==> expected"; break;
- case 59: s = "\\u21d4 expected"; break;
- case 60: s = "==> expected"; break;
- case 61: s = "\\u21d2 expected"; break;
- case 62: s = "&& expected"; break;
- case 63: s = "\\u2227 expected"; break;
- case 64: s = "|| expected"; break;
- case 65: s = "\\u2228 expected"; break;
- case 66: s = "== expected"; break;
- case 67: s = "<= expected"; break;
- case 68: s = ">= expected"; break;
- case 69: s = "!= expected"; break;
- case 70: s = "!! expected"; break;
- case 71: s = "!in expected"; break;
- case 72: s = "\\u2260 expected"; break;
- case 73: s = "\\u2264 expected"; break;
- case 74: s = "\\u2265 expected"; break;
- case 75: s = "+ expected"; break;
- case 76: s = "- expected"; break;
- case 77: s = "/ expected"; break;
- case 78: s = "% expected"; break;
- case 79: s = "! expected"; break;
- case 80: s = "\\u00ac expected"; break;
- case 81: s = "false expected"; break;
- case 82: s = "true expected"; break;
- case 83: s = "null expected"; break;
- case 84: s = "# expected"; break;
- case 85: s = ". expected"; break;
- case 86: s = "fresh expected"; break;
- case 87: s = "[ expected"; break;
- case 88: s = "] expected"; break;
- case 89: s = ".. expected"; break;
- case 90: s = "this expected"; break;
- case 91: s = "old expected"; break;
- case 92: s = "forall expected"; break;
- case 93: s = "\\u2200 expected"; break;
- case 94: s = "exists expected"; break;
- case 95: s = "\\u2203 expected"; break;
- case 96: s = ":: expected"; break;
- case 97: s = "\\u2022 expected"; break;
- case 98: s = "??? expected"; break;
- case 99: s = "invalid ClassMemberDecl"; break;
- case 100: s = "invalid FunctionDecl"; break;
- case 101: s = "invalid MethodDecl"; break;
- case 102: s = "invalid TypeAndToken"; break;
- case 103: s = "invalid MethodSpec"; break;
+ case 36: s = "` expected"; break;
+ case 37: s = "match expected"; break;
+ case 38: s = "case expected"; break;
+ case 39: s = "=> expected"; break;
+ case 40: s = "label expected"; break;
+ case 41: s = "break expected"; break;
+ case 42: s = "return expected"; break;
+ case 43: s = ":= expected"; break;
+ case 44: s = "new expected"; break;
+ case 45: s = "havoc expected"; break;
+ case 46: s = "if expected"; break;
+ case 47: s = "else expected"; break;
+ case 48: s = "while expected"; break;
+ case 49: s = "invariant expected"; break;
+ case 50: s = "call expected"; break;
+ case 51: s = "foreach expected"; break;
+ case 52: s = "in expected"; break;
+ case 53: s = "| expected"; break;
+ case 54: s = "assert expected"; break;
+ case 55: s = "assume expected"; break;
+ case 56: s = "use expected"; break;
+ case 57: s = "print expected"; break;
+ case 58: s = "then expected"; break;
+ case 59: s = "<==> expected"; break;
+ case 60: s = "\\u21d4 expected"; break;
+ case 61: s = "==> expected"; break;
+ case 62: s = "\\u21d2 expected"; break;
+ case 63: s = "&& expected"; break;
+ case 64: s = "\\u2227 expected"; break;
+ case 65: s = "|| expected"; break;
+ case 66: s = "\\u2228 expected"; break;
+ case 67: s = "== expected"; break;
+ case 68: s = "<= expected"; break;
+ case 69: s = ">= expected"; break;
+ case 70: s = "!= expected"; break;
+ case 71: s = "!! expected"; break;
+ case 72: s = "!in expected"; break;
+ case 73: s = "\\u2260 expected"; break;
+ case 74: s = "\\u2264 expected"; break;
+ case 75: s = "\\u2265 expected"; break;
+ case 76: s = "+ expected"; break;
+ case 77: s = "- expected"; break;
+ case 78: s = "/ expected"; break;
+ case 79: s = "% expected"; break;
+ case 80: s = "! expected"; break;
+ case 81: s = "\\u00ac expected"; break;
+ case 82: s = "false expected"; break;
+ case 83: s = "true expected"; break;
+ case 84: s = "null expected"; break;
+ case 85: s = "# expected"; break;
+ case 86: s = ". expected"; break;
+ case 87: s = "fresh expected"; break;
+ case 88: s = "[ expected"; break;
+ case 89: s = "] expected"; break;
+ case 90: s = ".. expected"; break;
+ case 91: s = "this expected"; break;
+ case 92: s = "old expected"; break;
+ case 93: s = "forall expected"; break;
+ case 94: s = "\\u2200 expected"; break;
+ case 95: s = "exists expected"; break;
+ case 96: s = "\\u2203 expected"; break;
+ case 97: s = ":: expected"; break;
+ case 98: s = "\\u2022 expected"; break;
+ case 99: s = "??? expected"; break;
+ case 100: s = "invalid ClassMemberDecl"; break;
+ case 101: s = "invalid FunctionDecl"; break;
+ case 102: s = "invalid MethodDecl"; break;
+ case 103: s = "invalid TypeAndToken"; break;
case 104: s = "invalid MethodSpec"; break;
- case 105: s = "invalid Expression"; break;
- case 106: s = "invalid ReferenceType"; break;
- case 107: s = "invalid FunctionSpec"; break;
- case 108: s = "invalid FunctionBody"; break;
- case 109: s = "invalid PossiblyWildExpression"; break;
- case 110: s = "invalid Stmt"; break;
- case 111: s = "invalid OneStmt"; break;
- case 112: s = "invalid IfStmt"; break;
- case 113: s = "invalid ForeachStmt"; break;
- case 114: s = "invalid AssignRhs"; break;
- case 115: s = "invalid SelectExpression"; break;
- case 116: s = "invalid Guard"; break;
- case 117: s = "invalid CallStmtSubExpr"; break;
- case 118: s = "invalid AttributeArg"; break;
- case 119: s = "invalid EquivOp"; break;
- case 120: s = "invalid ImpliesOp"; break;
- case 121: s = "invalid AndOp"; break;
- case 122: s = "invalid OrOp"; break;
- case 123: s = "invalid RelOp"; break;
- case 124: s = "invalid AddOp"; break;
- case 125: s = "invalid UnaryExpression"; break;
- case 126: s = "invalid MulOp"; break;
- case 127: s = "invalid NegOp"; break;
- case 128: s = "invalid ConstAtomExpression"; break;
- case 129: s = "invalid ObjectExpression"; break;
- case 130: s = "invalid ObjectExpression"; break;
- case 131: s = "invalid SelectOrCallSuffix"; break;
- case 132: s = "invalid SelectOrCallSuffix"; break;
- case 133: s = "invalid QuantifierGuts"; break;
- case 134: s = "invalid Forall"; break;
- case 135: s = "invalid Exists"; break;
- case 136: s = "invalid AttributeOrTrigger"; break;
- case 137: s = "invalid QSep"; break;
+ case 105: s = "invalid MethodSpec"; break;
+ case 106: s = "invalid Expression"; break;
+ case 107: s = "invalid ReferenceType"; break;
+ case 108: s = "invalid FunctionSpec"; break;
+ case 109: s = "invalid FunctionBody"; break;
+ case 110: s = "invalid PossiblyWildFrameExpression"; break;
+ case 111: s = "invalid PossiblyWildExpression"; break;
+ case 112: s = "invalid Stmt"; break;
+ case 113: s = "invalid OneStmt"; break;
+ case 114: s = "invalid IfStmt"; break;
+ case 115: s = "invalid ForeachStmt"; break;
+ case 116: s = "invalid AssignRhs"; break;
+ case 117: s = "invalid SelectExpression"; break;
+ case 118: s = "invalid Guard"; break;
+ case 119: s = "invalid CallStmtSubExpr"; break;
+ case 120: s = "invalid AttributeArg"; break;
+ case 121: s = "invalid EquivOp"; break;
+ case 122: s = "invalid ImpliesOp"; break;
+ case 123: s = "invalid AndOp"; break;
+ case 124: s = "invalid OrOp"; break;
+ case 125: s = "invalid RelOp"; break;
+ case 126: s = "invalid AddOp"; break;
+ case 127: s = "invalid UnaryExpression"; break;
+ case 128: s = "invalid MulOp"; break;
+ case 129: s = "invalid NegOp"; break;
+ case 130: s = "invalid ConstAtomExpression"; break;
+ case 131: s = "invalid ObjectExpression"; break;
+ case 132: s = "invalid ObjectExpression"; break;
+ case 133: s = "invalid SelectOrCallSuffix"; break;
+ case 134: s = "invalid SelectOrCallSuffix"; break;
+ case 135: s = "invalid QuantifierGuts"; break;
+ case 136: s = "invalid Forall"; break;
+ case 137: s = "invalid Exists"; break;
+ case 138: s = "invalid AttributeOrTrigger"; break;
+ case 139: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
@@ -1949,24 +1974,24 @@ List<Expression!>! decreases) { }
static bool[,]! set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,x, x,x,x,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,x, x,x,x,x, x,x,x,x, x,x,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, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,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,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, 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,T,x, x,x,T,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,T,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, T,x,x,T, T,T,T,T, T,x,T,T, x,x,T,T, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,x,T,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,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,T,T, x,x,x,x, x,x,x,x},
- {x,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,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,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,T, x,x,T,T, x,x,x,x, x,x,x,x},
- {x,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,T,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, 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,T, T,T,T,T, T,x,T,T, x,x,T,T, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,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,T,T, x,x,x,x, x,x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,T, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,T,T, T,x,T,x, x,x,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,x, x,x,x,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,x, x,x,x,x, x,x,x,x, x,x,x,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, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,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,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, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,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,T,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,T,x,x, T,T,T,T, T,T,x,T, T,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,T,x, x,T,x,x, x,x,T,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, T,T,T,x, x,T,T,x, T,x,T,T, 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,T, T,x,x,x, x,x,x,x, x},
+ {x,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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,x,T, T,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,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,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,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,T,x,x, T,T,T,T, T,T,x,T, T,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,T,T,x, T,x,T,T, 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,T, T,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,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,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,x,T, T,x,x,T, T,x,x,x, x,x,x,x, x}
};
diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc index a49d1a7e..755c10b2 100644 --- a/Source/Dafny/Printer.ssc +++ b/Source/Dafny/Printer.ssc @@ -188,7 +188,7 @@ namespace Microsoft.Dafny { int ind = indent + IndentAmount;
PrintSpec("requires", f.Req, ind);
- PrintSpecLine("reads", f.Reads, ind);
+ PrintFrameSpecLine("reads", f.Reads, ind);
PrintSpecLine("decreases", f.Decreases, ind);
if (f.Body != null) {
Indent(indent);
@@ -242,7 +242,7 @@ namespace Microsoft.Dafny { int ind = indent + IndentAmount;
PrintSpec("requires", method.Req, ind);
- PrintSpecLine("modifies", method.Mod, ind);
+ PrintFrameSpecLine("modifies", method.Mod, ind);
PrintSpec("ensures", method.Ens, ind);
PrintSpecLine("decreases", method.Decreases, ind);
@@ -292,6 +292,15 @@ namespace Microsoft.Dafny { }
}
+ void PrintFrameSpecLine(string! kind, List<FrameExpression!>! ee, int indent) {
+ if (ee.Count != 0) {
+ Indent(indent);
+ wr.Write("{0} ", kind);
+ PrintFrameExpressionList(ee);
+ wr.WriteLine(";");
+ }
+ }
+
void PrintSpec(string! kind, List<MaybeFreeExpression!>! ee, int indent) {
foreach (MaybeFreeExpression e in ee) {
Indent(indent);
@@ -851,5 +860,17 @@ namespace Microsoft.Dafny { PrintExpression(e);
}
}
+
+ void PrintFrameExpressionList(List<FrameExpression!>! fexprs) {
+ string sep = "";
+ foreach (FrameExpression fe in fexprs) {
+ wr.Write(sep);
+ sep = ", ";
+ PrintExpression(fe.E);
+ if (fe.FieldName != null) {
+ wr.Write("`{0}", fe.FieldName);
+ }
+ }
+ }
}
}
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 5b672b17..0222b606 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -424,20 +424,8 @@ namespace Microsoft.Dafny { Error(r, "Precondition must be a boolean (got {0})", r.Type);
}
}
- foreach (Expression r in f.Reads) {
- ResolveExpression(r, false, true);
- Type t = r.Type;
- assert t != null; // follows from postcondition of ResolveExpression
- if (t is CollectionType) {
- t = ((CollectionType)t).Arg;
- }
- if (t is ObjectType) {
- // fine
- } else if (UserDefinedType.DenotesClass(t) != null) {
- // fine
- } else {
- Error(r, "a reads-clause expression must denote an object or a collection of objects (instead got {0})", r.Type);
- }
+ foreach (FrameExpression fr in f.Reads) {
+ ResolveFrameExpression(fr, "reads");
}
foreach (Expression r in f.Decreases) {
ResolveExpression(r, false, true);
@@ -454,6 +442,37 @@ namespace Microsoft.Dafny { scope.PopMarker();
}
+ void ResolveFrameExpression(FrameExpression! fe, string! kind) {
+ ResolveExpression(fe.E, false, true);
+ Type t = fe.E.Type;
+ assert t != null; // follows from postcondition of ResolveExpression
+ if (t is CollectionType) {
+ t = ((CollectionType)t).Arg;
+ }
+ if (t is ObjectType) {
+ // fine, as long as there's no field name
+ if (fe.FieldName != null) {
+ Error(fe.E, "type '{0}' does not contain a field named '{1}'", t, fe.FieldName);
+ }
+ } else if (UserDefinedType.DenotesClass(t) != null) {
+ // fine type
+ if (fe.FieldName != null) {
+ UserDefinedType ctype;
+ MemberDecl member = ResolveMember(fe.E.tok, t, fe.FieldName, out ctype);
+ if (member == null) {
+ // error has already been reported by ResolveMember
+ } else if (!(member is Field)) {
+ Error(fe.E, "member {0} in class {1} does not refer to a field", fe.FieldName, ((!)ctype).Name);
+ } else {
+ assert ctype != null && ctype.ResolvedClass != null; // follows from postcondition of ResolveMember
+ fe.Field = (Field)member;
+ }
+ }
+ } else {
+ Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type);
+ }
+ }
+
/// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
@@ -497,20 +516,8 @@ namespace Microsoft.Dafny { Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);
}
}
- foreach (Expression e in m.Mod) {
- ResolveExpression(e, false, true);
- Type t = e.Type;
- assert t != null; // follows from postcondition of ResolveExpression
- if (t is CollectionType) {
- t = ((CollectionType)t).Arg;
- }
- if (t is ObjectType) {
- // fine
- } else if (UserDefinedType.DenotesClass(t) != null) {
- // fine
- } else {
- Error(e, "a modifies-clause expression must denote an object or a collection of objects (instead got {0})", e.Type);
- }
+ foreach (FrameExpression fe in m.Mod) {
+ ResolveFrameExpression(fe, "modifies");
}
foreach (Expression e in m.Decreases) {
ResolveExpression(e, false, true);
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc index 56c6f0be..cf759f84 100644 --- a/Source/Dafny/Scanner.ssc +++ b/Source/Dafny/Scanner.ssc @@ -30,21 +30,21 @@ public class Scanner { [Microsoft.Contracts.Verify(false)]
static Scanner() {
- start[0] = 54;
- start[33] = 32;
+ start[0] = 55;
+ start[33] = 33;
start[34] = 3;
- start[35] = 45;
- start[37] = 43;
- start[38] = 26;
+ start[35] = 46;
+ start[37] = 44;
+ start[38] = 27;
start[39] = 1;
start[40] = 12;
start[41] = 13;
start[42] = 14;
- start[43] = 40;
+ start[43] = 41;
start[44] = 8;
- start[45] = 41;
- start[46] = 46;
- start[47] = 42;
+ start[45] = 42;
+ start[46] = 47;
+ start[47] = 43;
start[48] = 2;
start[49] = 2;
start[50] = 2;
@@ -58,7 +58,7 @@ public class Scanner { start[58] = 9;
start[59] = 7;
start[60] = 10;
- start[61] = 15;
+ start[61] = 16;
start[62] = 11;
start[63] = 1;
start[65] = 1;
@@ -87,11 +87,11 @@ public class Scanner { start[88] = 1;
start[89] = 1;
start[90] = 1;
- start[91] = 47;
+ start[91] = 48;
start[92] = 1;
- start[93] = 48;
+ start[93] = 49;
start[95] = 1;
- start[96] = 1;
+ start[96] = 15;
start[97] = 1;
start[98] = 1;
start[99] = 1;
@@ -119,21 +119,21 @@ public class Scanner { start[121] = 1;
start[122] = 1;
start[123] = 5;
- start[124] = 18;
+ start[124] = 19;
start[125] = 6;
- start[172] = 44;
- start[8226] = 53;
- start[8658] = 25;
- start[8660] = 22;
- start[8704] = 50;
- start[8707] = 51;
- start[8743] = 28;
- start[8744] = 30;
- start[8800] = 37;
- start[8804] = 38;
- start[8805] = 39;
+ start[172] = 45;
+ start[8226] = 54;
+ start[8658] = 26;
+ start[8660] = 23;
+ start[8704] = 51;
+ start[8707] = 52;
+ start[8743] = 29;
+ start[8744] = 31;
+ start[8800] = 38;
+ start[8804] = 39;
+ start[8805] = 40;
}
- const int noSym = 98;
+ const int noSym = 99;
static short[] start = new short[16385];
@@ -297,33 +297,33 @@ public class Scanner { case "object": t.kind = 32; break;
case "function": t.kind = 33; break;
case "reads": t.kind = 34; break;
- case "match": t.kind = 36; break;
- case "case": t.kind = 37; break;
- case "label": t.kind = 39; break;
- case "break": t.kind = 40; break;
- case "return": t.kind = 41; break;
- case "new": t.kind = 43; break;
- case "havoc": t.kind = 44; break;
- case "if": t.kind = 45; break;
- case "else": t.kind = 46; break;
- case "while": t.kind = 47; break;
- case "invariant": t.kind = 48; break;
- case "call": t.kind = 49; break;
- case "foreach": t.kind = 50; break;
- case "in": t.kind = 51; break;
- case "assert": t.kind = 53; break;
- case "assume": t.kind = 54; break;
- case "use": t.kind = 55; break;
- case "print": t.kind = 56; break;
- case "then": t.kind = 57; break;
- case "false": t.kind = 81; break;
- case "true": t.kind = 82; break;
- case "null": t.kind = 83; break;
- case "fresh": t.kind = 86; break;
- case "this": t.kind = 90; break;
- case "old": t.kind = 91; break;
- case "forall": t.kind = 92; break;
- case "exists": t.kind = 94; break;
+ case "match": t.kind = 37; break;
+ case "case": t.kind = 38; break;
+ case "label": t.kind = 40; break;
+ case "break": t.kind = 41; break;
+ case "return": t.kind = 42; break;
+ case "new": t.kind = 44; break;
+ case "havoc": t.kind = 45; break;
+ case "if": t.kind = 46; break;
+ case "else": t.kind = 47; break;
+ case "while": t.kind = 48; break;
+ case "invariant": t.kind = 49; break;
+ case "call": t.kind = 50; break;
+ case "foreach": t.kind = 51; break;
+ case "in": t.kind = 52; break;
+ case "assert": t.kind = 54; break;
+ case "assume": t.kind = 55; break;
+ case "use": t.kind = 56; break;
+ case "print": t.kind = 57; break;
+ case "then": t.kind = 58; break;
+ case "false": t.kind = 82; break;
+ case "true": t.kind = 83; break;
+ case "null": t.kind = 84; break;
+ case "fresh": t.kind = 87; break;
+ case "this": t.kind = 91; break;
+ case "old": t.kind = 92; break;
+ case "forall": t.kind = 93; break;
+ case "exists": t.kind = 95; break;
default: break;
}
@@ -341,7 +341,7 @@ public class Scanner { switch (state) {
case 0: {t.kind = noSym; goto done;} // NextCh already done
case 1:
- if ((ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch >= '_' && ch <= 'z')) {buf.Append(ch); NextCh(); goto case 1;}
+ if ((ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z')) {buf.Append(ch); NextCh(); goto case 1;}
else {t.kind = 1; t.val = buf.ToString(); CheckLiteral(); return t;}
case 2:
if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 2;}
@@ -361,14 +361,14 @@ public class Scanner { case 8:
{t.kind = 15; goto done;}
case 9:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 17;}
- else if (ch == ':') {buf.Append(ch); NextCh(); goto case 52;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 18;}
+ else if (ch == ':') {buf.Append(ch); NextCh(); goto case 53;}
else {t.kind = 16; goto done;}
case 10:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 19;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
else {t.kind = 17; goto done;}
case 11:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 31;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 32;}
else {t.kind = 18; goto done;}
case 12:
{t.kind = 26; goto done;}
@@ -377,38 +377,38 @@ public class Scanner { case 14:
{t.kind = 35; goto done;}
case 15:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 16;}
- else if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 36; goto done;}
case 16:
- {t.kind = 38; goto done;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 17;}
+ else if (ch == '=') {buf.Append(ch); NextCh(); goto case 24;}
+ else {t.kind = noSym; goto done;}
case 17:
- {t.kind = 42; goto done;}
+ {t.kind = 39; goto done;}
case 18:
- if (ch == '|') {buf.Append(ch); NextCh(); goto case 29;}
- else {t.kind = 52; goto done;}
+ {t.kind = 43; goto done;}
case 19:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
- else {t.kind = 67; goto done;}
+ if (ch == '|') {buf.Append(ch); NextCh(); goto case 30;}
+ else {t.kind = 53; goto done;}
case 20:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 21;}
- else {t.kind = noSym; goto done;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 21;}
+ else {t.kind = 68; goto done;}
case 21:
- {t.kind = 58; goto done;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 22;}
+ else {t.kind = noSym; goto done;}
case 22:
{t.kind = 59; goto done;}
case 23:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
- else {t.kind = 66; goto done;}
- case 24:
{t.kind = 60; goto done;}
+ case 24:
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 25;}
+ else {t.kind = 67; goto done;}
case 25:
{t.kind = 61; goto done;}
case 26:
- if (ch == '&') {buf.Append(ch); NextCh(); goto case 27;}
- else {t.kind = noSym; goto done;}
- case 27:
{t.kind = 62; goto done;}
+ case 27:
+ if (ch == '&') {buf.Append(ch); NextCh(); goto case 28;}
+ else {t.kind = noSym; goto done;}
case 28:
{t.kind = 63; goto done;}
case 29:
@@ -416,21 +416,21 @@ public class Scanner { case 30:
{t.kind = 65; goto done;}
case 31:
- {t.kind = 68; goto done;}
+ {t.kind = 66; goto done;}
case 32:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 33;}
- else if (ch == '!') {buf.Append(ch); NextCh(); goto case 34;}
- else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 35;}
- else {t.kind = 79; goto done;}
- case 33:
{t.kind = 69; goto done;}
+ case 33:
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 34;}
+ else if (ch == '!') {buf.Append(ch); NextCh(); goto case 35;}
+ else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 36;}
+ else {t.kind = 80; goto done;}
case 34:
{t.kind = 70; goto done;}
case 35:
- if (ch == 'n') {buf.Append(ch); NextCh(); goto case 36;}
- else {t.kind = noSym; goto done;}
- case 36:
{t.kind = 71; goto done;}
+ case 36:
+ if (ch == 'n') {buf.Append(ch); NextCh(); goto case 37;}
+ else {t.kind = noSym; goto done;}
case 37:
{t.kind = 72; goto done;}
case 38:
@@ -446,27 +446,29 @@ public class Scanner { case 43:
{t.kind = 78; goto done;}
case 44:
- {t.kind = 80; goto done;}
+ {t.kind = 79; goto done;}
case 45:
- {t.kind = 84; goto done;}
+ {t.kind = 81; goto done;}
case 46:
- if (ch == '.') {buf.Append(ch); NextCh(); goto case 49;}
- else {t.kind = 85; goto done;}
+ {t.kind = 85; goto done;}
case 47:
- {t.kind = 87; goto done;}
+ if (ch == '.') {buf.Append(ch); NextCh(); goto case 50;}
+ else {t.kind = 86; goto done;}
case 48:
{t.kind = 88; goto done;}
case 49:
{t.kind = 89; goto done;}
case 50:
- {t.kind = 93; goto done;}
+ {t.kind = 90; goto done;}
case 51:
- {t.kind = 95; goto done;}
+ {t.kind = 94; goto done;}
case 52:
{t.kind = 96; goto done;}
case 53:
{t.kind = 97; goto done;}
- case 54: {t.kind = 0; goto done;}
+ case 54:
+ {t.kind = 98; goto done;}
+ case 55: {t.kind = 0; goto done;}
}
done:
t.val = buf.ToString();
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 7a802ecd..c079db7e 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -740,7 +740,7 @@ namespace Microsoft.Dafny { Bpl.Expr heapOF = Bpl.Expr.SelectTok(m.tok, etran.HeapExpr, o, f);
Bpl.Expr oldHeapOF = Bpl.Expr.SelectTok(m.tok, etran.Old.HeapExpr, o, f);
- Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.Old.TheFrame(m.tok), o);
+ Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.Old.TheFrame(m.tok), o, f);
Bpl.Expr body = Bpl.Expr.Or(inEnclosingFrame, Bpl.Expr.Eq(heapOF, oldHeapOF));
Bpl.Trigger tr = new Bpl.Trigger(m.tok, true, new Bpl.ExprSeq(heapOF));
Bpl.Expr qq = new Bpl.ForallExpr(m.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, body);
@@ -804,22 +804,51 @@ namespace Microsoft.Dafny { }
// set up the information used to verify the method's modifies clause
- ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
- // Declare a local variable $_Frame: [ref]bool
- Bpl.IdentifierExpr theFrame = etran.TheFrame(m.tok); // this is a throw-away expression, used only to extract the name and type of the $_Frame variable
+ DefineFrame(m.tok, m.Mod, builder, localVariables);
+ }
+
+ void DefineFrame(Token! tok, List<FrameExpression!>! frameClause, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! localVariables)
+ requires predef != null;
+ {
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);
+ // Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool
+ Bpl.IdentifierExpr theFrame = etran.TheFrame(tok); // this is a throw-away expression, used only to extract the name and type of the $_Frame variable
assert theFrame.Type != null; // follows from the postcondition of TheFrame
- Bpl.LocalVariable frame = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, theFrame.Name, theFrame.Type));
+ Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, theFrame.Name, theFrame.Type));
localVariables.Add(frame);
- // $_Frame := (lambda $o: ref :: $o != null && $Heap[$o,alloc] ==> $o in ModifiesClause);
- Bpl.BoundVariable oVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$o", predef.RefType));
- Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(m.tok, oVar);
- Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(m.tok, o));
- Bpl.Expr consequent = InRWClause(m.tok, o, m.Mod, etran, null, null);
- Bpl.Expr lambda = new Bpl.LambdaExpr(m.tok, new Bpl.TypeVariableSeq(), new Bpl.VariableSeq(oVar), null, Bpl.Expr.Imp(ante, consequent));
+ // $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause);
+ Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
+ Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
+ Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o));
+ Bpl.Expr consequent = InRWClause(tok, o, f, frameClause, etran, null, null);
+ Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null,
+ Bpl.Expr.Imp(ante, consequent));
- builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));
+ builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));
}
-
+
+ void CheckFrameSubset(Token! tok, List<FrameExpression!>! calleeFrame,
+ Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap,
+ ExpressionTranslator! etran, Bpl.StmtListBuilder! builder, string! errorMessage)
+ requires predef != null;
+ {
+ // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in calleeFrame ==> $_Frame[o,f]);
+ Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
+ Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
+ Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o));
+ Bpl.Expr oInCallee = InRWClause(tok, o, f, calleeFrame, etran, receiverReplacement, substMap);
+ Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.TheFrame(tok), o, f);
+ Bpl.Expr q = new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar),
+ Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), inEnclosingFrame));
+ builder.Add(Assert(tok, q, errorMessage));
+ }
+
/// <summary>
/// Generates:
/// axiom (forall h0: HeapType, h1: HeapType, formals... ::
@@ -861,7 +890,7 @@ namespace Microsoft.Dafny { Bpl.Expr unchanged = Bpl.Expr.Eq(Bpl.Expr.SelectTok(f.tok, h0, o, field), Bpl.Expr.SelectTok(f.tok, h1, o, field));
Bpl.Expr heapSucc = FunctionCall(f.tok, BuiltinFunction.HeapSucc, null, h0, h1);
- Bpl.Expr r0 = InRWClause(f.tok, o, f.Reads, etran0, null, null);
+ Bpl.Expr r0 = InRWClause(f.tok, o, field, f.Reads, etran0, null, null);
Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),
Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged));
@@ -921,7 +950,7 @@ namespace Microsoft.Dafny { }
}
- Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, List<Expression!>! rw, ExpressionTranslator! etran,
+ Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, Bpl.Expr! f, List<FrameExpression!>! rw, ExpressionTranslator! etran,
Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap)
requires predef != null;
// requires o to denote an expression of type RefType
@@ -929,8 +958,8 @@ namespace Microsoft.Dafny { requires receiverReplacement == null <==> substMap == null;
{
Bpl.Expr disjunction = null;
- foreach (Expression rwComponent in rw) {
- Expression e = rwComponent;
+ foreach (FrameExpression rwComponent in rw) {
+ Expression e = rwComponent.E;
if (substMap != null) {
assert receiverReplacement != null;
e = Substitute(e, receiverReplacement, substMap);
@@ -955,6 +984,9 @@ namespace Microsoft.Dafny { disjunct = Bpl.Expr.Eq(o, etran.TrExpr(e));
}
disjunct = Bpl.Expr.And(IsTotal(e, etran), disjunct);
+ if (rwComponent.Field != null) {
+ disjunct = Bpl.Expr.And(disjunct, Bpl.Expr.Eq(f, new Bpl.IdentifierExpr(rwComponent.E.tok, GetField(rwComponent.Field))));
+ }
if (disjunction == null) {
disjunction = disjunct;
} else {
@@ -1016,10 +1048,13 @@ namespace Microsoft.Dafny { // absolutely well-defined.
// check well-formedness of the decreases clauses
foreach (Expression p in f.Decreases) {
- CheckWellformed(p, f, Position.Positive, locals, builder, etran);
+ // Note, in this well-formedness check, function is passed in as null. This will cause there to be
+ // no reads checks or decreases checks. This seems like a good idea, and I hope it is also sound.
+ CheckWellformed(p, null, Position.Positive, locals, builder, etran);
}
// check well-formedness of the body
if (f.Body != null) {
+ DefineFrame(f.tok, f.Reads, builder, locals);
CheckWellformed(f.Body, f, Position.Positive, locals, builder, etran);
}
@@ -1201,7 +1236,7 @@ namespace Microsoft.Dafny { CheckWellformed(e.Obj, func, Position.Neither, locals, builder, etran);
CheckNonNull(expr.tok, e.Obj, builder, etran);
if (func != null) {
- builder.Add(Assert(expr.tok, InRWClause(expr.tok, etran.TrExpr(e.Obj), func.Reads, etran, null, null), "insufficient reads clause to read field"));
+ builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field"));
}
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
@@ -1258,14 +1293,7 @@ namespace Microsoft.Dafny { }
if (func != null) {
// check that the callee reads only what the caller is already allowed to read
- // emit: assert (forall o: ref :: o != null && o in callee.reads ==> o in caller.reads);
- Bpl.BoundVariable oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$o", predef.RefType));
- Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);
- Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
- Bpl.Expr oInCallee = InRWClause(expr.tok, o, e.Function.Reads, etran, e.Receiver, substMap);
- Bpl.Expr oInCaller = InRWClause(expr.tok, o, func.Reads, etran, null, null);
- Bpl.Expr q = new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInCallee), oInCaller));
- builder.Add(Assert(expr.tok, q, "insufficient reads clause to invoke function"));
+ CheckFrameSubset(expr.tok, e.Function.Reads, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function");
// finally, check that the decreases measure goes down
ModuleDecl module = ((!)e.Function.EnclosingClass).Module;
@@ -1273,11 +1301,11 @@ namespace Microsoft.Dafny { if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(func)) {
List<Expression!> contextDecreases = func.Decreases;
if (contextDecreases.Count == 0) {
- contextDecreases = func.Reads; // use its reads clause instead
+ contextDecreases = ProjectOutSpecificFields(func.Reads); // use its reads clause instead
}
List<Expression!> calleeDecreases = e.Function.Decreases;
if (calleeDecreases.Count == 0) {
- calleeDecreases = e.Function.Reads; // use its reads clause instead
+ calleeDecreases = ProjectOutSpecificFields(e.Function.Reads); // use its reads clause instead
}
CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);
}
@@ -1380,6 +1408,14 @@ namespace Microsoft.Dafny { }
}
+ List<Expression!>! ProjectOutSpecificFields(List<FrameExpression!>! fexprs) {
+ List<Expression!> exprs = new List<Expression!>();
+ foreach (FrameExpression fe in fexprs) {
+ exprs.Add(fe.E);
+ }
+ return exprs;
+ }
+
Bpl.Constant! GetClass(TopLevelDecl! cl)
requires predef != null;
{
@@ -1642,14 +1678,14 @@ namespace Microsoft.Dafny { /// S2. the post-state of the two-state interval
/// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
/// </summary>
- Bpl.Expr! FrameCondition(Token! tok, List<Expression!>! modifiesClause, ExpressionTranslator! etranPre, ExpressionTranslator! etran)
+ Bpl.Expr! FrameCondition(Token! tok, List<FrameExpression!>! modifiesClause, ExpressionTranslator! etranPre, ExpressionTranslator! etran)
requires predef != null;
{
// generate:
// (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] }
// o != null && old($Heap)[o,alloc] ==>
// $Heap[o,f] == PreHeap[o,f] ||
- // o in modifiesClause)
+ // (o,f) in modifiesClause)
Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
@@ -1661,7 +1697,7 @@ namespace Microsoft.Dafny { Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.Old.IsAlloced(tok, o));
Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
- consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, modifiesClause, etran.Old, null, null));
+ consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etran.Old, null, null));
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
@@ -1897,16 +1933,7 @@ namespace Microsoft.Dafny { }
// Check modifies clause
- {
- // assert (forall o: ref :: o != null && $Heap[o,alloc] && o in CalleeModifiesClause ==> $_Frame[o]);
- Bpl.BoundVariable oVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$o", predef.RefType));
- Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(stmt.Tok, oVar);
- Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(stmt.Tok, o));
- Bpl.Expr calleeModifies = InRWClause(stmt.Tok, o, s.Method.Mod, etran, s.Receiver, substMap);
- Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o);
- Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(Bpl.Expr.And(ante, calleeModifies), inEnclosingFrame));
- builder.Add(Assert(stmt.Tok, qq, "call may violate caller's modifies clause"));
- }
+ CheckFrameSubset(stmt.Tok, s.Method.Mod, s.Receiver, substMap, etran, builder, "call may violate caller's modifies clause");
// Check termination
ModuleDecl module = ((!)s.Method.EnclosingClass).Module;
@@ -2120,11 +2147,11 @@ namespace Microsoft.Dafny { ForeachStmt s = (ForeachStmt)stmt;
// assert/assume (forall o: ref :: o != null && o in S && Range(o) ==> Expr);
// assert (forall o: ref :: o != null && o in S && Range(o) ==> IsTotal(RHS));
- // assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o]); // this checks the enclosing modifies clause
+ // assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]); // this checks the enclosing modifies clause
// var oldHeap := $Heap;
// havoc $Heap;
// assume $HeapSucc(oldHeap, $Heap);
- // assume (forall o: ref, f: Field :: $Heap[o,f] = oldHeap[o,f] || (f = F && o != null && o in S && Range(o)));
+ // assume (forall<alpha> o: ref, f: Field alpha :: $Heap[o,f] = oldHeap[o,f] || (f = F && o != null && o in S && Range(o)));
// assume (forall o: ref :: o != null && o in S && Range(o) ==> $Heap[o,F] = RHS[$Heap := oldHeap]);
// Note, $Heap[o,alloc] is intentionally omitted from the antecedent of the quantifier in the previous line. That
// allocatedness property should hold automatically, because the set/seq quantified is a program expression, which
@@ -2199,8 +2226,8 @@ namespace Microsoft.Dafny { builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined")); // totality check
}
- // Here comes: assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o]);
- Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o));
+ // Here comes: assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);
+ Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));
Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
builder.Add(Assert(s.BodyAssign.Tok, qq, "foreach assignment may update an object not in the enclosing method's modifies clause"));
@@ -2500,7 +2527,7 @@ namespace Microsoft.Dafny { FieldSelectExpr fse = (FieldSelectExpr)lhs;
assert fse.Field != null;
// check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj];
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(fse.Obj)), "assignment may update an object not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(fse.Obj), GetField(fse)), "assignment may update an object not in the enclosing method's modifies clause"));
Bpl.IdentifierExpr h = (Bpl.IdentifierExpr!)etran.HeapExpr; // TODO: is this cast always justified?
bRhs = etran.CondApplyBox(tok, bRhs, (!)((ExprRhs)rhs).Expr.Type, fse.Field.Type);
@@ -2584,7 +2611,9 @@ namespace Microsoft.Dafny { public Bpl.IdentifierExpr! TheFrame(Token! tok)
ensures result.Type != null;
{
- Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(predef.RefType), Bpl.Type.Bool);
+ Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta");
+ Bpl.Type fieldAlpha = predef.FieldName(tok, alpha);
+ Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.TypeSeq(predef.RefType, fieldAlpha), Bpl.Type.Bool);
return new Bpl.IdentifierExpr(tok, "$_Frame", ty);
}
diff --git a/Test/test2/Answer b/Test/test2/Answer index b6f1e7c2..a9329010 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -3,17 +3,17 @@ FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold at this return statement.
FormulaTerm.bpl(4,3): Related location: This is the postcondition that might not hold.
Execution trace:
- FormulaTerm.bpl(8,1): start
+ FormulaTerm.bpl(8,1): start
Boogie program verifier finished with 11 verified, 1 error
-------------------- FormulaTerm2.bpl --------------------
FormulaTerm2.bpl(39,5): Error BP5001: This assertion might not hold.
Execution trace:
- FormulaTerm2.bpl(36,3): start
+ FormulaTerm2.bpl(36,3): start
FormulaTerm2.bpl(47,5): Error BP5001: This assertion might not hold.
Execution trace:
- FormulaTerm2.bpl(45,3): start
+ FormulaTerm2.bpl(45,3): start
Boogie program verifier finished with 2 verified, 2 errors
@@ -21,21 +21,21 @@ Boogie program verifier finished with 2 verified, 2 errors Passification.bpl(44,3): Error BP5003: A postcondition might not hold at this return statement.
Passification.bpl(36,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Passification.bpl(39,1): A
+ Passification.bpl(39,1): A
Passification.bpl(116,3): Error BP5001: This assertion might not hold.
Execution trace:
- Passification.bpl(106,1): L0
- Passification.bpl(111,1): L1
- Passification.bpl(115,1): L2
+ Passification.bpl(106,1): L0
+ Passification.bpl(111,1): L1
+ Passification.bpl(115,1): L2
Passification.bpl(151,3): Error BP5001: This assertion might not hold.
Execution trace:
- Passification.bpl(144,1): L0
- Passification.bpl(150,1): L2
+ Passification.bpl(144,1): L0
+ Passification.bpl(150,1): L2
Passification.bpl(165,3): Error BP5001: This assertion might not hold.
Execution trace:
- Passification.bpl(158,1): L0
- Passification.bpl(161,1): L1
- Passification.bpl(164,1): L2
+ Passification.bpl(158,1): L0
+ Passification.bpl(161,1): L1
+ Passification.bpl(164,1): L2
Boogie program verifier finished with 7 verified, 4 errors
@@ -47,23 +47,23 @@ Boogie program verifier finished with 4 verified, 0 errors Ensures.bpl(30,5): Error BP5003: A postcondition might not hold at this return statement.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Ensures.bpl(28,3): start
+ Ensures.bpl(28,3): start
Ensures.bpl(35,5): Error BP5003: A postcondition might not hold at this return statement.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Ensures.bpl(34,3): start
+ Ensures.bpl(34,3): start
Ensures.bpl(41,5): Error BP5003: A postcondition might not hold at this return statement.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Ensures.bpl(39,3): start
+ Ensures.bpl(39,3): start
Ensures.bpl(47,5): Error BP5003: A postcondition might not hold at this return statement.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Ensures.bpl(45,3): start
+ Ensures.bpl(45,3): start
Ensures.bpl(72,5): Error BP5003: A postcondition might not hold at this return statement.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Ensures.bpl(70,3): start
+ Ensures.bpl(70,3): start
Boogie program verifier finished with 5 verified, 5 errors
@@ -71,7 +71,7 @@ Boogie program verifier finished with 5 verified, 5 errors Old.bpl(29,5): Error BP5003: A postcondition might not hold at this return statement.
Old.bpl(26,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Old.bpl(28,3): start
+ Old.bpl(28,3): start
Boogie program verifier finished with 7 verified, 1 error
@@ -84,75 +84,75 @@ OldIllegal.bpl(14,23): Error: old expressions allowed only in two-state contexts Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement.
Arrays.bpl(38,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Arrays.bpl(42,3): start
+ Arrays.bpl(42,3): start
Arrays.bpl(127,5): Error BP5003: A postcondition might not hold at this return statement.
Arrays.bpl(119,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Arrays.bpl(123,3): start
+ Arrays.bpl(123,3): start
Boogie program verifier finished with 8 verified, 2 errors
-------------------- Axioms.bpl --------------------
Axioms.bpl(19,5): Error BP5001: This assertion might not hold.
Execution trace:
- Axioms.bpl(18,3): start
+ Axioms.bpl(18,3): start
Boogie program verifier finished with 2 verified, 1 error
-------------------- Quantifiers.bpl --------------------
Quantifiers.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(19,3): start
+ Quantifiers.bpl(19,3): start
Quantifiers.bpl(43,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(42,3): start
+ Quantifiers.bpl(42,3): start
Quantifiers.bpl(65,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(64,3): start
+ Quantifiers.bpl(64,3): start
Quantifiers.bpl(73,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(71,3): start
+ Quantifiers.bpl(71,3): start
Quantifiers.bpl(125,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(124,3): start
+ Quantifiers.bpl(124,3): start
Quantifiers.bpl(150,5): Error BP5001: This assertion might not hold.
Execution trace:
- Quantifiers.bpl(149,3): start
+ Quantifiers.bpl(149,3): start
Boogie program verifier finished with 8 verified, 6 errors
-------------------- Call.bpl --------------------
Call.bpl(13,5): Error BP5001: This assertion might not hold.
Execution trace:
- Call.bpl(9,3): entry
+ Call.bpl(9,3): entry
Call.bpl(46,5): Error BP5001: This assertion might not hold.
Execution trace:
- Call.bpl(45,3): start
+ Call.bpl(45,3): start
Call.bpl(55,5): Error BP5003: A postcondition might not hold at this return statement.
Call.bpl(20,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Call.bpl(53,3): start
+ Call.bpl(53,3): start
Boogie program verifier finished with 2 verified, 3 errors
-------------------- AssumeEnsures.bpl --------------------
AssumeEnsures.bpl(28,9): Error BP5001: This assertion might not hold.
Execution trace:
- AssumeEnsures.bpl(26,5): entry
+ AssumeEnsures.bpl(26,5): entry
AssumeEnsures.bpl(47,9): Error BP5001: This assertion might not hold.
Execution trace:
- AssumeEnsures.bpl(46,5): entry
+ AssumeEnsures.bpl(46,5): entry
AssumeEnsures.bpl(62,9): Error BP5001: This assertion might not hold.
Execution trace:
- AssumeEnsures.bpl(60,5): entry
+ AssumeEnsures.bpl(60,5): entry
Boogie program verifier finished with 4 verified, 3 errors
-------------------- CutBackEdge.bpl --------------------
CutBackEdge.bpl(10,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- CutBackEdge.bpl(5,3): entry
- CutBackEdge.bpl(9,3): block850
+ CutBackEdge.bpl(5,3): entry
+ CutBackEdge.bpl(9,3): block850
Boogie program verifier finished with 0 verified, 1 error
@@ -163,8 +163,8 @@ Boogie program verifier finished with 2 verified, 0 errors -------------------- LoopInvAssume.bpl --------------------
LoopInvAssume.bpl(18,7): Error BP5001: This assertion might not hold.
Execution trace:
- LoopInvAssume.bpl(8,4): entry
- LoopInvAssume.bpl(16,4): exit
+ LoopInvAssume.bpl(8,4): entry
+ LoopInvAssume.bpl(16,4): exit
Boogie program verifier finished with 0 verified, 1 error
@@ -214,160 +214,172 @@ strings-where.bpl(990,36): Error: invalid argument types (any and name) to binar Structured.bpl(252,14): Error BP5003: A postcondition might not hold at this return statement.
Structured.bpl(243,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Structured.bpl(244,5): anon0
- Structured.bpl(246,5): anon6_LoopBody
- Structured.bpl(247,7): anon7_LoopBody
- Structured.bpl(248,11): anon8_Then
- Structured.bpl(252,5): anon4
- Structured.bpl(252,14): anon9_Then
+ Structured.bpl(244,5): anon0
+ Structured.bpl(246,5): anon6_LoopBody
+ Structured.bpl(247,7): anon7_LoopBody
+ Structured.bpl(248,11): anon8_Then
+ Structured.bpl(252,5): anon4
+ Structured.bpl(252,14): anon9_Then
Structured.bpl(303,3): Error BP5001: This assertion might not hold.
Execution trace:
- Structured.bpl(299,5): anon0
- Structured.bpl(300,3): anon3_Else
- Structured.bpl(303,3): anon2
+ Structured.bpl(299,5): anon0
+ Structured.bpl(300,3): anon3_Else
+ Structured.bpl(303,3): anon2
Structured.bpl(311,7): Error BP5001: This assertion might not hold.
Execution trace:
- Structured.bpl(308,3): anon0
- Structured.bpl(308,3): anon1_Then
- Structured.bpl(309,5): A
+ Structured.bpl(308,3): anon0
+ Structured.bpl(308,3): anon1_Then
+ Structured.bpl(309,5): A
Boogie program verifier finished with 15 verified, 3 errors
-------------------- Where.bpl --------------------
Where.bpl(8,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(6,3): anon0
+ Where.bpl(6,3): anon0
Where.bpl(22,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(16,5): anon0
+ Where.bpl(16,5): anon0
Where.bpl(32,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(30,3): anon0
+ Where.bpl(30,3): anon0
Where.bpl(44,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(40,5): anon0
+ Where.bpl(40,5): anon0
Where.bpl(57,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(52,3): anon0
+ Where.bpl(52,3): anon0
Where.bpl(111,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(102,5): anon0
- Where.bpl(104,3): anon3_LoopHead
- Where.bpl(104,3): anon3_LoopDone
+ Where.bpl(102,5): anon0
+ Where.bpl(104,3): anon3_LoopHead
+ Where.bpl(104,3): anon3_LoopDone
Where.bpl(128,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(121,5): anon0
- Where.bpl(122,3): anon3_LoopHead
- Where.bpl(122,3): anon3_LoopDone
+ Where.bpl(121,5): anon0
+ Where.bpl(122,3): anon3_LoopHead
+ Where.bpl(122,3): anon3_LoopDone
Where.bpl(145,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(138,5): anon0
- Where.bpl(139,3): anon3_LoopHead
- Where.bpl(139,3): anon3_LoopDone
+ Where.bpl(138,5): anon0
+ Where.bpl(139,3): anon3_LoopHead
+ Where.bpl(139,3): anon3_LoopDone
Where.bpl(162,3): Error BP5001: This assertion might not hold.
Execution trace:
- Where.bpl(155,5): anon0
- Where.bpl(156,3): anon3_LoopHead
- Where.bpl(156,3): anon3_LoopDone
+ Where.bpl(155,5): anon0
+ Where.bpl(156,3): anon3_LoopHead
+ Where.bpl(156,3): anon3_LoopDone
Boogie program verifier finished with 2 verified, 9 errors
-------------------- UpdateExpr.bpl --------------------
UpdateExpr.bpl(14,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(14,3): anon0
+ UpdateExpr.bpl(14,3): anon0
UpdateExpr.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(19,3): anon0
+ UpdateExpr.bpl(19,3): anon0
UpdateExpr.bpl(32,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(32,3): anon0
+ UpdateExpr.bpl(32,3): anon0
UpdateExpr.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(38,3): anon0
+ UpdateExpr.bpl(38,3): anon0
UpdateExpr.bpl(52,3): Error BP5001: This assertion might not hold.
Execution trace:
- UpdateExpr.bpl(51,5): anon0
+ UpdateExpr.bpl(51,5): anon0
Boogie program verifier finished with 5 verified, 5 errors
-------------------- NeverPattern.bpl --------------------
NeverPattern.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- NeverPattern.bpl(15,3): anon0
+ NeverPattern.bpl(15,3): anon0
NeverPattern.bpl(22,3): Error BP5001: This assertion might not hold.
Execution trace:
- NeverPattern.bpl(21,3): anon0
+ NeverPattern.bpl(21,3): anon0
NeverPattern.bpl(28,3): Error BP5001: This assertion might not hold.
Execution trace:
- NeverPattern.bpl(27,3): anon0
+ NeverPattern.bpl(27,3): anon0
Boogie program verifier finished with 1 verified, 3 errors
-------------------- NullaryMaps.bpl --------------------
NullaryMaps.bpl(28,3): Error BP5001: This assertion might not hold.
Execution trace:
- NullaryMaps.bpl(28,3): anon0
+ NullaryMaps.bpl(28,3): anon0
NullaryMaps.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
- NullaryMaps.bpl(28,3): anon0
+ NullaryMaps.bpl(28,3): anon0
NullaryMaps.bpl(36,3): Error BP5001: This assertion might not hold.
Execution trace:
- NullaryMaps.bpl(36,3): anon0
+ NullaryMaps.bpl(36,3): anon0
Boogie program verifier finished with 2 verified, 3 errors
-------------------- Implies.bpl --------------------
Implies.bpl(12,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(11,3): anon0
+ Implies.bpl(11,3): anon0
Implies.bpl(15,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(11,3): anon0
+ Implies.bpl(11,3): anon0
Implies.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(19,3): anon0
+ Implies.bpl(19,3): anon0
Implies.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(24,3): anon0
+ Implies.bpl(24,3): anon0
Implies.bpl(25,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(24,3): anon0
+ Implies.bpl(24,3): anon0
Implies.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(29,3): anon0
+ Implies.bpl(29,3): anon0
Implies.bpl(34,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(34,3): anon0
+ Implies.bpl(34,3): anon0
Implies.bpl(35,3): Error BP5001: This assertion might not hold.
Execution trace:
- Implies.bpl(34,3): anon0
+ Implies.bpl(34,3): anon0
Boogie program verifier finished with 0 verified, 8 errors
-------------------- IfThenElse1.bpl --------------------
IfThenElse1.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- IfThenElse1.bpl(26,3): anon0
+ IfThenElse1.bpl(26,3): anon0
IfThenElse1.bpl(33,3): Error BP5001: This assertion might not hold.
Execution trace:
- IfThenElse1.bpl(33,3): anon0
+ IfThenElse1.bpl(33,3): anon0
Boogie program verifier finished with 2 verified, 2 errors
-------------------- Lambda.bpl --------------------
Lambda.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(36,5): anon0
+ Lambda.bpl(36,5): anon0
Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(36,5): anon0
+ Lambda.bpl(36,5): anon0
Boogie program verifier finished with 4 verified, 2 errors
-------------------- LambdaPoly.bpl --------------------
+LambdaPoly.bpl(28,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ LambdaPoly.bpl(24,5): anon0
+ LambdaPoly.bpl(27,5): anon4_Then
+LambdaPoly.bpl(31,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ LambdaPoly.bpl(24,5): anon0
+ LambdaPoly.bpl(30,5): anon5_Then
+LambdaPoly.bpl(36,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ LambdaPoly.bpl(24,5): anon0
+ LambdaPoly.bpl(34,5): anon5_Else
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 1 verified, 3 errors
-------------------- sk_hack.bpl --------------------
Boogie program verifier finished with 1 verified, 0 errors
@@ -375,28 +387,28 @@ 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(17,3): anon0
CallForall.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(28,3): anon0
+ 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(40,3): anon0
CallForall.bpl(47,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(46,3): anon0
+ 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(75,3): anon0
CallForall.bpl(111,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(109,3): anon0
+ 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(117,3): anon0
CallForall.bpl(125,3): Error BP5001: This assertion might not hold.
Execution trace:
- CallForall.bpl(124,3): anon0
+ CallForall.bpl(124,3): anon0
Boogie program verifier finished with 10 verified, 8 errors
@@ -404,13 +416,13 @@ Boogie program verifier finished with 10 verified, 8 errors ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold at this return statement.
ContractEvaluationOrder.bpl(3,3): Related location: This is the postcondition that might not hold.
Execution trace:
- ContractEvaluationOrder.bpl(7,5): anon0
+ ContractEvaluationOrder.bpl(7,5): anon0
ContractEvaluationOrder.bpl(15,3): Error BP5001: This assertion might not hold.
Execution trace:
- ContractEvaluationOrder.bpl(12,5): anon0
+ ContractEvaluationOrder.bpl(12,5): anon0
ContractEvaluationOrder.bpl(24,3): Error BP5002: A precondition for this call might not hold.
ContractEvaluationOrder.bpl(30,3): Related location: This is the precondition that might not hold.
Execution trace:
- ContractEvaluationOrder.bpl(23,5): anon0
+ ContractEvaluationOrder.bpl(23,5): anon0
Boogie program verifier finished with 1 verified, 3 errors
diff --git a/Test/test2/LambdaPoly.bpl b/Test/test2/LambdaPoly.bpl index 6d56e7c5..0fec0260 100644 --- a/Test/test2/LambdaPoly.bpl +++ b/Test/test2/LambdaPoly.bpl @@ -16,3 +16,25 @@ procedure a() assert !diff(a,b)[2]; } +// ----------------------- + +procedure Polly<Cracker>(c,d: Cracker) +{ + var e: Cracker; + e := c; + + if (*) { + assert (forall<T> t: T :: (lambda<beta> b: beta, s: T :: b==c && s==t)[c,t]); + assert (forall<U> u: U :: (lambda<beta> b: beta, s: U :: b==c && s==u)[u,u]); // error + } else if (*) { + assert (lambda<V> v: V :: (lambda<beta> b: beta, s: V :: b==c && s==v)[v,v])[e]; + assert (lambda<W> w: W :: (lambda<beta> b: beta, s: W :: b==c && s==w)[w,w])[d]; // error + e := d; + } else { + assume TriggerHappy(c); + assert (exists k: Cracker :: { TriggerHappy(k) } (lambda<beta> b: beta, m: Cracker :: b==k && m==c)[c,c]); + assert (forall k: Cracker :: (lambda<beta> b: beta, m: Cracker :: b==k && m==c)[c,c]); // error + } +} + +function TriggerHappy<T>(T): bool; diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el index d4902a74..5b60dcab 100644 --- a/Util/Emacs/boogie-mode.el +++ b/Util/Emacs/boogie-mode.el @@ -35,7 +35,7 @@ "invariant" "extends" "complete"
)) . font-lock-builtin-face)
`(,(boogie-regexp-opt '(
- "assert" "assume" "break" "call" "else" "havoc" "if" "goto" "return" "while"
+ "assert" "assume" "break" "call" "then" "else" "havoc" "if" "goto" "return" "while"
"old" "forall" "exists" "lambda" "cast"
"false" "true")) . font-lock-keyword-face)
`(,(boogie-regexp-opt '("bool" "int"
diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty index 30a18b82..e07d1399 100644 --- a/Util/latex/boogie.sty +++ b/Util/latex/boogie.sty @@ -34,7 +34,7 @@ procedure,implementation,
requires,modifies,ensures,free,
% expressions
- false,true,null,old,
+ false,true,null,old,then,
% statements
assert,assume,havoc,call,if,else,while,invariant,break,return,goto,
},
|