diff options
48 files changed, 807 insertions, 857 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5623f091..b7b81d44 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -28,7 +28,6 @@ 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>();
static int anonymousIds = 0;
struct MemberModifiers {
@@ -292,11 +291,8 @@ DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.> .)
{ Attribute<ref attrs> }
Ident<out id>
- (. parseVarScope.PushMarker(); .)
[ FormalsOptionalIds<formals> ]
- (. parseVarScope.PopMarker();
- ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
- .)
+ (. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)
.
FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
@@ -321,7 +317,6 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.> List<IToken/*!*/> ids = new List<IToken/*!*/>();;
IToken/*!*/ id;
Expression/*!*/ e;
- parseVarScope.PushMarker();
.)
"replaces"
(. if (mmod.IsUnlimited) { SemErr(t, "coupling invariants cannot be declared 'unlimited'"); }
@@ -329,15 +324,13 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.> if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }
.)
{ Attribute<ref attrs> }
- Ident<out id> (. ids.Add(id); parseVarScope.Push(id.val, id.val); .)
- { "," Ident<out id> (. ids.Add(id); parseVarScope.Push(id.val, id.val); .)
+ Ident<out id> (. ids.Add(id); .)
+ { "," Ident<out id> (. ids.Add(id); .)
}
"by"
Expression<out e>
";"
- (. mm.Add(new CouplingInvariant(ids, e, attrs));
- parseVarScope.PopMarker();
- .)
+ (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)
.
@@ -441,7 +434,6 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m> { Attribute<ref attrs> }
Ident<out id>
[ GenericParameters<typeArgs> ]
- (. parseVarScope.PushMarker(); .)
Formals<true, true, ins>
[ "returns"
Formals<false, true, outs>
@@ -451,8 +443,7 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m> | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb, out bodyStart, out bodyEnd> (. body = (BlockStmt)bb; .)
)
- (. parseVarScope.PopMarker();
- if (isRefinement)
+ (. if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
else
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -483,8 +474,8 @@ Formals<.bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals.> = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; .)
"("
[
- GIdentType<allowGhosts, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); .)
- { "," GIdentType<allowGhosts, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); .)
+ GIdentType<allowGhosts, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
+ { "," GIdentType<allowGhosts, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
}
]
")"
@@ -494,8 +485,8 @@ FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.> = (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; .)
"("
[
- TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .)
- { "," TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .)
+ TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)
+ { "," TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)
}
]
")"
@@ -588,7 +579,6 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> { Attribute<ref attrs> }
Ident<out id>
[ GenericParameters<typeArgs> ]
- (. parseVarScope.PushMarker(); .)
Formals<true, false, formals>
":"
Type<out returnType>
@@ -597,8 +587,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> | { FunctionSpec<reqs, reads, ens, decreases> }
FunctionBody<out bb, out bodyStart, out bodyEnd> (. body = bb; .)
)
- (. parseVarScope.PopMarker();
- f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
+ (. f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
.)
@@ -677,18 +666,15 @@ CaseExpression<out MatchCaseExpr/*!*/ c> List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
Expression/*!*/ body;
.)
- "case" (. x = t; parseVarScope.PushMarker(); .)
+ "case" (. x = t; .)
Ident<out id>
[ "("
- Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val); .)
- { "," Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val); .)
+ Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
+ { "," Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
}
")" ]
"=>"
- MatchOrExpr<out body> (. c = new MatchCaseExpr(x, id.val, arguments, body);
- parseVarScope.PopMarker(); .)
+ MatchOrExpr<out body> (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
.
/* Note, '(' is start of more than one alternative in MatchOrExpr, but the first intentionally hides
@@ -707,13 +693,11 @@ BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd> = (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);
List<Statement/*!*/> body = new List<Statement/*!*/>();
.)
- (. parseVarScope.PushMarker(); .)
"{" (. bodyStart = t; .)
{ Stmt<body>
}
"}" (. bodyEnd = t;
block = new BlockStmt(bodyStart, body); .)
- (. parseVarScope.PopMarker(); .)
.
Stmt<.List<Statement/*!*/>/*!*/ ss.>
@@ -733,8 +717,9 @@ OneStmt<out Statement/*!*/ s> | AssumeStmt<out s>
| UseStmt<out s>
| PrintStmt<out s>
+ | UpdateStmt<out s>
| HavocStmt<out s>
- | "call" UpdateStmt<out s>
+ | VarDeclStatement<out s>
| IfStmt<out s>
| WhileStmt<out s>
| MatchStmt<out s>
@@ -746,8 +731,6 @@ OneStmt<out Statement/*!*/ s> ] ";" (. s = new BreakStmt(x, label); .)
| "return" (. x = t; .)
";" (. s = new ReturnStmt(x); .)
- | VarDeclStatement<out s>
- | UpdateStmt<out s>
)
.
@@ -885,9 +868,7 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives.> Expression<out e>
"=>"
(. body = new List<Statement>(); .)
- (. parseVarScope.PushMarker(); .)
{ Stmt<body> }
- (. parseVarScope.PopMarker(); .)
(. alternatives.Add(new GuardedAlternative(x, e, body)); .)
}
"}"
@@ -963,21 +944,16 @@ CaseStatement<out MatchCaseStmt/*!*/ c> List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
List<Statement/*!*/> body = new List<Statement/*!*/>();
.)
- "case" (. x = t; parseVarScope.PushMarker(); .)
+ "case" (. x = t; .)
Ident<out id>
[ "("
- Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val); .)
- { "," Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val); .)
+ Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
+ { "," Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
}
")" ]
"=>"
- (. parseVarScope.PushMarker(); .)
{ Stmt<body> }
- (. parseVarScope.PopMarker(); .)
(. c = new MatchCaseStmt(x, id.val, arguments, body); .)
- (. parseVarScope.PopMarker(); .)
.
/*------------------------------------------------------------------------*/
@@ -991,7 +967,6 @@ ForeachStmt<out Statement/*!*/ s> List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();
Statement bodyAssign = null;
.)
- (. parseVarScope.PushMarker(); .)
"foreach" (. x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
@@ -999,7 +974,6 @@ ForeachStmt<out Statement/*!*/ s> "(" Ident<out boundVar>
[ ":" Type<out ty> ]
"in" Expression<out collection>
- (. parseVarScope.Push(boundVar.val, boundVar.val); .)
[ "|" Expression<out range> ]
")"
"{"
@@ -1016,7 +990,6 @@ ForeachStmt<out Statement/*!*/ s> s = dummyStmt; // some error occurred in parsing the bodyAssign
}
.)
- (. parseVarScope.PopMarker(); .)
.
AssertStmt<out Statement/*!*/ s>
@@ -1322,10 +1295,9 @@ QuantifierGuts<out Expression/*!*/ q> ( Forall (. x = t; univ = true; .)
| Exists (. x = t; .)
)
- (. parseVarScope.PushMarker(); .)
- IdentTypeOptional<out bv> (. bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); .)
+ IdentTypeOptional<out bv> (. bvars.Add(bv); .)
{ ","
- IdentTypeOptional<out bv> (. bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); .)
+ IdentTypeOptional<out bv> (. bvars.Add(bv); .)
}
{ AttributeOrTrigger<ref attrs, ref trigs> }
[ "|"
@@ -1338,7 +1310,6 @@ QuantifierGuts<out Expression/*!*/ q> } else {
q = new ExistsExpr(x, bvars, range, body, trigs, attrs);
}
- parseVarScope.PopMarker();
.)
.
@@ -1355,10 +1326,9 @@ ComprehensionExpr<out Expression/*!*/ q> Expression body = null;
.)
"set" (. x = t; .)
- (. parseVarScope.PushMarker(); .)
- IdentTypeOptional<out bv> (. bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); .)
+ IdentTypeOptional<out bv> (. bvars.Add(bv); .)
{ ","
- IdentTypeOptional<out bv> (. bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name); .)
+ IdentTypeOptional<out bv> (. bvars.Add(bv); .)
}
"|" Expression<out range>
[
@@ -1367,7 +1337,6 @@ ComprehensionExpr<out Expression/*!*/ q> ]
(. if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }
q = new SetComprehension(x, bvars, range, body);
- parseVarScope.PopMarker();
.)
.
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 2586c67d..2fa88a69 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -20,7 +20,7 @@ public class Parser { public const int _digits = 2;
public const int _arrayToken = 3;
public const int _string = 4;
- public const int maxT = 106;
+ public const int maxT = 105;
const bool T = true;
const bool x = false;
@@ -41,7 +41,6 @@ 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>();
static int anonymousIds = 0;
struct MemberModifiers {
@@ -363,7 +362,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! DatatypeMemberDecl(ctors);
}
Expect(15);
- } else SynErr(107);
+ } else SynErr(106);
dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
dt.BodyStartTok = bodyStart;
dt.BodyEndTok = t;
@@ -398,7 +397,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! mm.Add(m);
} else if (la.kind == 20) {
CouplingInvDecl(mmod, mm);
- } else SynErr(108);
+ } else SynErr(107);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -467,7 +466,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 23) {
GenericParameters(typeArgs);
}
- parseVarScope.PushMarker();
Formals(true, false, formals);
Expect(22);
Type(out returnType);
@@ -482,8 +480,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
FunctionBody(out bb, out bodyStart, out bodyEnd);
body = bb;
- } else SynErr(109);
- parseVarScope.PopMarker();
+ } else SynErr(108);
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
@@ -511,7 +508,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! } else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(110);
+ } else SynErr(109);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
while (la.kind == 7) {
@@ -521,7 +518,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (la.kind == 23) {
GenericParameters(typeArgs);
}
- parseVarScope.PushMarker();
Formals(true, true, ins);
if (la.kind == 26) {
Get();
@@ -538,10 +534,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
BlockStmt(out bb, out bodyStart, out bodyEnd);
body = (BlockStmt)bb;
- } else SynErr(111);
- parseVarScope.PopMarker();
+ } else SynErr(110);
if (isRefinement)
- m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
+ m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
else
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
m.BodyStartTok = bodyStart;
@@ -555,7 +550,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! List<IToken/*!*/> ids = new List<IToken/*!*/>();;
IToken/*!*/ id;
Expression/*!*/ e;
- parseVarScope.PushMarker();
Expect(20);
if (mmod.IsUnlimited) { SemErr(t, "coupling invariants cannot be declared 'unlimited'"); }
@@ -566,18 +560,16 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Attribute(ref attrs);
}
Ident(out id);
- ids.Add(id); parseVarScope.Push(id.val, id.val);
+ ids.Add(id);
while (la.kind == 19) {
Get();
Ident(out id);
- ids.Add(id); parseVarScope.Push(id.val, id.val);
+ ids.Add(id);
}
Expect(21);
Expression(out e);
Expect(15);
- mm.Add(new CouplingInvariant(ids, e, attrs));
- parseVarScope.PopMarker();
-
+ mm.Add(new CouplingInvariant(ids, e, attrs));
}
void DatatypeMemberDecl(List<DatatypeCtor/*!*/>/*!*/ ctors) {
@@ -590,13 +582,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Attribute(ref attrs);
}
Ident(out id);
- parseVarScope.PushMarker();
if (la.kind == 32) {
FormalsOptionalIds(formals);
}
- parseVarScope.PopMarker();
- ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
-
+ ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
}
void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
@@ -604,11 +593,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Expect(32);
if (StartOf(7)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
- formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
+ formals.Add(new Formal(id, name, ty, true, isGhost));
while (la.kind == 19) {
Get();
TypeIdentOptional(out id, out name, out ty, out isGhost);
- formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
+ formals.Add(new Formal(id, name, ty, true, isGhost));
}
}
Expect(33);
@@ -740,7 +729,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! ReferenceType(out tok, out ty);
break;
}
- default: SynErr(112); break;
+ default: SynErr(111); break;
}
}
@@ -749,11 +738,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Expect(32);
if (la.kind == 1 || la.kind == 11) {
GIdentType(allowGhosts, out id, out ty, out isGhost);
- formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
+ formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
while (la.kind == 19) {
Get();
GIdentType(allowGhosts, out id, out ty, out isGhost);
- formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
+ formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
}
}
Expect(33);
@@ -791,19 +780,18 @@ List<Expression/*!*/>/*!*/ decreases) { Expression(out e);
Expect(15);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(113);
+ } else SynErr(112);
} else if (la.kind == 31) {
Get();
Expressions(decreases);
Expect(15);
- } else SynErr(114);
+ } else SynErr(113);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
Contract.Ensures(Contract.ValueAtReturn(out block) != null);
List<Statement/*!*/> body = new List<Statement/*!*/>();
- parseVarScope.PushMarker();
Expect(7);
bodyStart = t;
while (StartOf(9)) {
@@ -812,7 +800,6 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(8);
bodyEnd = t;
block = new BlockStmt(bodyStart, body);
- parseVarScope.PopMarker();
}
void FrameExpression(out FrameExpression/*!*/ fe) {
@@ -878,7 +865,7 @@ List<Expression/*!*/>/*!*/ decreases) { GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(115);
+ } else SynErr(114);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -910,7 +897,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
Expressions(decreases);
Expect(15);
- } else SynErr(116);
+ } else SynErr(115);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -921,7 +908,7 @@ List<Expression/*!*/>/*!*/ decreases) { MatchExpression(out e);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(117);
+ } else SynErr(116);
Expect(8);
bodyEnd = t;
}
@@ -933,7 +920,7 @@ List<Expression/*!*/>/*!*/ decreases) { fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(118);
+ } else SynErr(117);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -944,7 +931,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new WildcardExpr(t);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(119);
+ } else SynErr(118);
}
void MatchExpression(out Expression/*!*/ e) {
@@ -967,25 +954,22 @@ List<Expression/*!*/>/*!*/ decreases) { Expression/*!*/ body;
Expect(45);
- x = t; parseVarScope.PushMarker();
+ x = t;
Ident(out id);
if (la.kind == 32) {
Get();
Ident(out arg);
- arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val);
+ arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
while (la.kind == 19) {
Get();
Ident(out arg);
- arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val);
+ arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
}
Expect(33);
}
Expect(46);
MatchOrExpr(out body);
- c = new MatchCaseExpr(x, id.val, arguments, body);
- parseVarScope.PopMarker();
+ c = new MatchCaseExpr(x, id.val, arguments, body);
}
void MatchOrExpr(out Expression/*!*/ e) {
@@ -998,7 +982,7 @@ List<Expression/*!*/>/*!*/ decreases) { MatchExpression(out e);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(120);
+ } else SynErr(119);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1015,34 +999,35 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
- } else if (la.kind == 64) {
+ } else if (la.kind == 63) {
AssertStmt(out s);
- } else if (la.kind == 65) {
+ } else if (la.kind == 64) {
AssumeStmt(out s);
- } else if (la.kind == 66) {
+ } else if (la.kind == 65) {
UseStmt(out s);
- } else if (la.kind == 67) {
+ } else if (la.kind == 66) {
PrintStmt(out s);
- } else if (la.kind == 57) {
- HavocStmt(out s);
- } else if (la.kind == 47) {
- Get();
+ } else if (StartOf(11)) {
UpdateStmt(out s);
- } else if (la.kind == 58) {
+ } else if (la.kind == 56) {
+ HavocStmt(out s);
+ } else if (la.kind == 11 || la.kind == 18) {
+ VarDeclStatement(out s);
+ } else if (la.kind == 57) {
IfStmt(out s);
- } else if (la.kind == 60) {
+ } else if (la.kind == 59) {
WhileStmt(out s);
} else if (la.kind == 44) {
MatchStmt(out s);
- } else if (la.kind == 62) {
+ } else if (la.kind == 61) {
ForeachStmt(out s);
- } else if (la.kind == 48) {
+ } else if (la.kind == 47) {
Get();
x = t;
Ident(out id);
Expect(22);
s = new LabelStmt(x, id.val);
- } else if (la.kind == 49) {
+ } else if (la.kind == 48) {
Get();
x = t;
if (la.kind == 1) {
@@ -1051,21 +1036,17 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(15);
s = new BreakStmt(x, label);
- } else if (la.kind == 50) {
+ } else if (la.kind == 49) {
Get();
x = t;
Expect(15);
s = new ReturnStmt(x);
- } else if (la.kind == 11 || la.kind == 18) {
- VarDeclStatement(out s);
- } else if (StartOf(11)) {
- UpdateStmt(out s);
- } else SynErr(121);
+ } else SynErr(120);
}
void AssertStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(64);
+ Expect(63);
x = t;
Expression(out e);
Expect(15);
@@ -1074,7 +1055,7 @@ List<Expression/*!*/>/*!*/ decreases) { void AssumeStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(65);
+ Expect(64);
x = t;
Expression(out e);
Expect(15);
@@ -1083,7 +1064,7 @@ List<Expression/*!*/>/*!*/ decreases) { void UseStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(66);
+ Expect(65);
x = t;
Expression(out e);
Expect(15);
@@ -1094,7 +1075,7 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Expect(67);
+ Expect(66);
x = t;
AttributeArg(out arg);
args.Add(arg);
@@ -1107,15 +1088,6 @@ List<Expression/*!*/>/*!*/ decreases) { s = new PrintStmt(x, args);
}
- void HavocStmt(out Statement/*!*/ s) {
- Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs;
- Expect(57);
- x = t;
- Lhs(out lhs);
- Expect(15);
- s = new AssignStmt(x, lhs);
- }
-
void UpdateStmt(out Statement/*!*/ s) {
List<Expression> lhss = new List<Expression>();
List<DeterminedAssignmentRhs> rhss = new List<DeterminedAssignmentRhs>();
@@ -1128,14 +1100,14 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 15) {
Get();
rhss.Add(new ExprRhs(e));
- } else if (la.kind == 19 || la.kind == 51) {
+ } else if (la.kind == 19 || la.kind == 50) {
lhss.Add(e); lhs0 = e;
while (la.kind == 19) {
Get();
Lhs(out e);
lhss.Add(e);
}
- Expect(51);
+ Expect(50);
x = t;
Rhs(out r, lhs0);
rhss.Add(r);
@@ -1145,10 +1117,65 @@ List<Expression/*!*/>/*!*/ decreases) { rhss.Add(r);
}
Expect(15);
- } else SynErr(122);
+ } else SynErr(121);
s = new UpdateStmt(x, lhss, rhss);
}
+ void HavocStmt(out Statement/*!*/ s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs;
+ Expect(56);
+ x = t;
+ Lhs(out lhs);
+ Expect(15);
+ s = new AssignStmt(x, lhs);
+ }
+
+ void VarDeclStatement(out Statement/*!*/ s) {
+ IToken x = null, assignTok = null; bool isGhost = false;
+ VarDecl/*!*/ d;
+ DeterminedAssignmentRhs r; Expression lhs0;
+ List<VarDecl> lhss = new List<VarDecl>();
+ List<DeterminedAssignmentRhs> rhss = new List<DeterminedAssignmentRhs>();
+
+ if (la.kind == 11) {
+ Get();
+ isGhost = true; x = t;
+ }
+ Expect(18);
+ if (!isGhost) { x = t; }
+ LocalIdentTypeOptional(out d, isGhost);
+ lhss.Add(d);
+ while (la.kind == 19) {
+ Get();
+ LocalIdentTypeOptional(out d, isGhost);
+ lhss.Add(d);
+ }
+ if (la.kind == 50) {
+ Get();
+ assignTok = t; lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
+ Rhs(out r, lhs0);
+ rhss.Add(r);
+ while (la.kind == 19) {
+ Get();
+ Rhs(out r, lhs0);
+ rhss.Add(r);
+ }
+ }
+ Expect(15);
+ UpdateStmt update;
+ if (rhss.Count == 0) {
+ update = null;
+ } else {
+ var ies = new List<Expression>();
+ foreach (var lhs in lhss) {
+ ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
+ }
+ update = new UpdateStmt(assignTok, ies, rhss);
+ }
+ s = new VarDeclStmt(x, lhss, update);
+
+ }
+
void IfStmt(out Statement/*!*/ ifStmt) {
Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;
Expression guard;
@@ -1159,26 +1186,26 @@ List<Expression/*!*/>/*!*/ decreases) { List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(58);
+ Expect(57);
x = t;
if (la.kind == 32) {
Guard(out guard);
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 59) {
+ if (la.kind == 58) {
Get();
- if (la.kind == 58) {
+ if (la.kind == 57) {
IfStmt(out s);
els = s;
} else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(123);
+ } else SynErr(122);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(124);
+ } else SynErr(123);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1191,7 +1218,7 @@ List<Expression/*!*/>/*!*/ decreases) { List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(60);
+ Expect(59);
x = t;
if (la.kind == 32) {
Guard(out guard);
@@ -1203,7 +1230,7 @@ List<Expression/*!*/>/*!*/ decreases) { LoopSpec(out invariants, out decreases);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives);
- } else SynErr(125);
+ } else SynErr(124);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1231,8 +1258,7 @@ List<Expression/*!*/>/*!*/ decreases) { List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();
Statement bodyAssign = null;
- parseVarScope.PushMarker();
- Expect(62);
+ Expect(61);
x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
@@ -1243,20 +1269,19 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
Type(out ty);
}
- Expect(63);
+ Expect(62);
Expression(out collection);
- parseVarScope.Push(boundVar.val, boundVar.val);
if (la.kind == 17) {
Get();
Expression(out range);
}
Expect(33);
Expect(7);
- while (la.kind == 64 || la.kind == 65 || la.kind == 66) {
- if (la.kind == 64) {
+ while (la.kind == 63 || la.kind == 64 || la.kind == 65) {
+ if (la.kind == 63) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (la.kind == 65) {
+ } else if (la.kind == 64) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1267,10 +1292,10 @@ List<Expression/*!*/>/*!*/ decreases) { if (StartOf(11)) {
UpdateStmt(out s);
bodyAssign = s;
- } else if (la.kind == 57) {
+ } else if (la.kind == 56) {
HavocStmt(out s);
bodyAssign = s;
- } else SynErr(126);
+ } else SynErr(125);
Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1278,53 +1303,6 @@ List<Expression/*!*/>/*!*/ decreases) { s = dummyStmt; // some error occurred in parsing the bodyAssign
}
- parseVarScope.PopMarker();
- }
-
- void VarDeclStatement(out Statement/*!*/ s) {
- IToken x = null, assignTok = null; bool isGhost = false;
- VarDecl/*!*/ d;
- DeterminedAssignmentRhs r; Expression lhs0;
- List<VarDecl> lhss = new List<VarDecl>();
- List<DeterminedAssignmentRhs> rhss = new List<DeterminedAssignmentRhs>();
-
- if (la.kind == 11) {
- Get();
- isGhost = true; x = t;
- }
- Expect(18);
- if (!isGhost) { x = t; }
- LocalIdentTypeOptional(out d, isGhost);
- lhss.Add(d);
- while (la.kind == 19) {
- Get();
- LocalIdentTypeOptional(out d, isGhost);
- lhss.Add(d);
- }
- if (la.kind == 51) {
- Get();
- assignTok = t; lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
- Rhs(out r, lhs0);
- rhss.Add(r);
- while (la.kind == 19) {
- Get();
- Rhs(out r, lhs0);
- rhss.Add(r);
- }
- }
- Expect(15);
- UpdateStmt update;
- if (rhss.Count == 0) {
- update = null;
- } else {
- var ies = new List<Expression>();
- foreach (var lhs in lhss) {
- ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
- }
- update = new UpdateStmt(assignTok, ies, rhss);
- }
- s = new VarDeclStmt(x, lhss, update);
-
}
void Lhs(out Expression e) {
@@ -1332,16 +1310,16 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 53 || la.kind == 55) {
+ while (la.kind == 52 || la.kind == 54) {
Suffix(ref e);
}
} else if (StartOf(13)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 53 || la.kind == 55) {
+ while (la.kind == 52 || la.kind == 54) {
Suffix(ref e);
}
- } else SynErr(127);
+ } else SynErr(126);
}
void Rhs(out DeterminedAssignmentRhs r, Expression receiverForInitCall) {
@@ -1352,16 +1330,16 @@ List<Expression/*!*/>/*!*/ decreases) { List<Expression> args;
r = null; // to please compiler
- if (la.kind == 52) {
+ if (la.kind == 51) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 53 || la.kind == 55) {
- if (la.kind == 53) {
+ if (la.kind == 52 || la.kind == 54) {
+ if (la.kind == 52) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(54);
+ Expect(53);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
} else {
@@ -1383,7 +1361,7 @@ List<Expression/*!*/>/*!*/ decreases) { r = new TypeRhs(newToken, ty, initCall);
}
- } else if (la.kind == 56) {
+ } else if (la.kind == 55) {
Get();
x = t;
Expression(out e);
@@ -1391,7 +1369,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(128);
+ } else SynErr(127);
}
void Guard(out Expression e) {
@@ -1403,7 +1381,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(129);
+ } else SynErr(128);
Expect(33);
}
@@ -1420,11 +1398,9 @@ List<Expression/*!*/>/*!*/ decreases) { Expression(out e);
Expect(46);
body = new List<Statement>();
- parseVarScope.PushMarker();
while (StartOf(9)) {
Stmt(body);
}
- parseVarScope.PopMarker();
alternatives.Add(new GuardedAlternative(x, e, body));
}
Expect(8);
@@ -1435,14 +1411,14 @@ List<Expression/*!*/>/*!*/ decreases) { invariants = new List<MaybeFreeExpression/*!*/>();
decreases = new List<Expression/*!*/>();
- while (la.kind == 28 || la.kind == 31 || la.kind == 61) {
- if (la.kind == 28 || la.kind == 61) {
+ while (la.kind == 28 || la.kind == 31 || la.kind == 60) {
+ if (la.kind == 28 || la.kind == 60) {
isFree = false;
if (la.kind == 28) {
Get();
isFree = true;
}
- Expect(61);
+ Expect(60);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(15);
@@ -1467,29 +1443,24 @@ List<Expression/*!*/>/*!*/ decreases) { List<Statement/*!*/> body = new List<Statement/*!*/>();
Expect(45);
- x = t; parseVarScope.PushMarker();
+ x = t;
Ident(out id);
if (la.kind == 32) {
Get();
Ident(out arg);
- arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val);
+ arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
while (la.kind == 19) {
Get();
Ident(out arg);
- arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
- parseVarScope.Push(arg.val, arg.val);
+ arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
}
Expect(33);
}
Expect(46);
- parseVarScope.PushMarker();
while (StartOf(9)) {
Stmt(body);
}
- parseVarScope.PopMarker();
c = new MatchCaseStmt(x, id.val, arguments, body);
- parseVarScope.PopMarker();
}
void AttributeArg(out Attributes.Argument/*!*/ arg) {
@@ -1500,13 +1471,13 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(130);
+ } else SynErr(129);
}
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 68 || la.kind == 69) {
+ while (la.kind == 67 || la.kind == 68) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1517,7 +1488,7 @@ List<Expression/*!*/>/*!*/ decreases) { void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 70 || la.kind == 71) {
+ if (la.kind == 69 || la.kind == 70) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1526,23 +1497,23 @@ List<Expression/*!*/>/*!*/ decreases) { }
void EquivOp() {
- if (la.kind == 68) {
+ if (la.kind == 67) {
Get();
- } else if (la.kind == 69) {
+ } else if (la.kind == 68) {
Get();
- } else SynErr(131);
+ } else SynErr(130);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(14)) {
- if (la.kind == 72 || la.kind == 73) {
+ if (la.kind == 71 || la.kind == 72) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 72 || la.kind == 73) {
+ while (la.kind == 71 || la.kind == 72) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1553,7 +1524,7 @@ List<Expression/*!*/>/*!*/ decreases) { x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 74 || la.kind == 75) {
+ while (la.kind == 73 || la.kind == 74) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1564,11 +1535,11 @@ List<Expression/*!*/>/*!*/ decreases) { }
void ImpliesOp() {
- if (la.kind == 70) {
+ if (la.kind == 69) {
Get();
- } else if (la.kind == 71) {
+ } else if (la.kind == 70) {
Get();
- } else SynErr(132);
+ } else SynErr(131);
}
void RelationalExpression(out Expression/*!*/ e0) {
@@ -1582,25 +1553,25 @@ List<Expression/*!*/>/*!*/ decreases) { }
void AndOp() {
- if (la.kind == 72) {
+ if (la.kind == 71) {
Get();
- } else if (la.kind == 73) {
+ } else if (la.kind == 72) {
Get();
- } else SynErr(133);
+ } else SynErr(132);
}
void OrOp() {
- if (la.kind == 74) {
+ if (la.kind == 73) {
Get();
- } else if (la.kind == 75) {
+ } else if (la.kind == 74) {
Get();
- } else SynErr(134);
+ } else SynErr(133);
}
void Term(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (la.kind == 85 || la.kind == 86) {
+ while (la.kind == 84 || la.kind == 85) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1610,7 +1581,7 @@ List<Expression/*!*/>/*!*/ decreases) { void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (la.kind) {
- case 76: {
+ case 75: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
@@ -1625,59 +1596,59 @@ List<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 77: {
+ case 76: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 78: {
+ case 77: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 79: {
+ case 78: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 80: {
+ case 79: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 63: {
+ case 62: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 81: {
+ case 80: {
Get();
x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 82: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 83: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 84: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(135); break;
+ default: SynErr(134); break;
}
}
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 42 || la.kind == 87 || la.kind == 88) {
+ while (la.kind == 42 || la.kind == 86 || la.kind == 87) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1686,23 +1657,23 @@ List<Expression/*!*/>/*!*/ decreases) { void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 85) {
+ if (la.kind == 84) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 86) {
+ } else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(136);
+ } else SynErr(135);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
- if (la.kind == 86) {
+ if (la.kind == 85) {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (la.kind == 89 || la.kind == 90) {
+ } else if (la.kind == 88 || la.kind == 89) {
NegOp();
x = t;
UnaryExpression(out e);
@@ -1711,15 +1682,15 @@ List<Expression/*!*/>/*!*/ decreases) { EndlessExpression(out e);
} else if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 53 || la.kind == 55) {
+ while (la.kind == 52 || la.kind == 54) {
Suffix(ref e);
}
} else if (StartOf(13)) {
ConstAtomExpression(out e);
- while (la.kind == 53 || la.kind == 55) {
+ while (la.kind == 52 || la.kind == 54) {
Suffix(ref e);
}
- } else SynErr(137);
+ } else SynErr(136);
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
@@ -1727,21 +1698,21 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 42) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 87) {
+ } else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 88) {
+ } else if (la.kind == 87) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(138);
+ } else SynErr(137);
}
void NegOp() {
- if (la.kind == 89) {
+ if (la.kind == 88) {
Get();
- } else if (la.kind == 90) {
+ } else if (la.kind == 89) {
Get();
- } else SynErr(139);
+ } else SynErr(138);
}
void EndlessExpression(out Expression e) {
@@ -1749,20 +1720,20 @@ List<Expression/*!*/>/*!*/ decreases) { Expression e0, e1;
e = dummyExpr;
- if (la.kind == 58) {
+ if (la.kind == 57) {
Get();
x = t;
Expression(out e);
- Expect(98);
+ Expect(97);
Expression(out e0);
- Expect(59);
+ Expect(58);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(17)) {
QuantifierGuts(out e);
} else if (la.kind == 37) {
ComprehensionExpr(out e);
- } else SynErr(140);
+ } else SynErr(139);
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -1772,7 +1743,7 @@ List<Expression/*!*/>/*!*/ decreases) { Ident(out id);
idents.Add(id);
- while (la.kind == 55) {
+ while (la.kind == 54) {
Get();
Ident(out id);
idents.Add(id);
@@ -1794,7 +1765,7 @@ List<Expression/*!*/>/*!*/ decreases) { List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 55) {
+ if (la.kind == 54) {
Get();
Ident(out id);
if (la.kind == 32) {
@@ -1807,24 +1778,24 @@ List<Expression/*!*/>/*!*/ decreases) { e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (la.kind == 53) {
+ } else if (la.kind == 52) {
Get();
x = t;
if (StartOf(8)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 99) {
+ if (la.kind == 98) {
Get();
anyDots = true;
if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 51) {
+ } else if (la.kind == 50) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 19 || la.kind == 54) {
+ } else if (la.kind == 19 || la.kind == 53) {
while (la.kind == 19) {
Get();
Expression(out ee);
@@ -1835,12 +1806,12 @@ List<Expression/*!*/>/*!*/ decreases) { multipleIndices.Add(ee);
}
- } else SynErr(141);
- } else if (la.kind == 99) {
+ } else SynErr(140);
+ } else if (la.kind == 98) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(142);
+ } else SynErr(141);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -1863,8 +1834,8 @@ List<Expression/*!*/>/*!*/ decreases) { }
}
- Expect(54);
- } else SynErr(143);
+ Expect(53);
+ } else SynErr(142);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -1873,17 +1844,17 @@ List<Expression/*!*/>/*!*/ decreases) { e = dummyExpr;
switch (la.kind) {
- case 91: {
+ case 90: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 92: {
+ case 91: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 93: {
+ case 92: {
Get();
e = new LiteralExpr(t);
break;
@@ -1893,12 +1864,12 @@ List<Expression/*!*/>/*!*/ decreases) { e = new LiteralExpr(t, n);
break;
}
- case 94: {
+ case 93: {
Get();
e = new ThisExpr(t);
break;
}
- case 95: {
+ case 94: {
Get();
x = t;
Expect(32);
@@ -1907,7 +1878,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new FreshExpr(x, e);
break;
}
- case 96: {
+ case 95: {
Get();
x = t;
Expect(32);
@@ -1916,7 +1887,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new AllocatedExpr(x, e);
break;
}
- case 97: {
+ case 96: {
Get();
x = t;
Expect(32);
@@ -1943,14 +1914,14 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(8);
break;
}
- case 53: {
+ case 52: {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(54);
+ Expect(53);
break;
}
case 32: {
@@ -1961,7 +1932,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(33);
break;
}
- default: SynErr(144); break;
+ default: SynErr(143); break;
}
}
@@ -1986,20 +1957,19 @@ List<Expression/*!*/>/*!*/ decreases) { Expression range = null;
Expression/*!*/ body;
- if (la.kind == 100 || la.kind == 101) {
+ if (la.kind == 99 || la.kind == 100) {
Forall();
x = t; univ = true;
- } else if (la.kind == 102 || la.kind == 103) {
+ } else if (la.kind == 101 || la.kind == 102) {
Exists();
x = t;
- } else SynErr(145);
- parseVarScope.PushMarker();
+ } else SynErr(144);
IdentTypeOptional(out bv);
- bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
+ bvars.Add(bv);
while (la.kind == 19) {
Get();
IdentTypeOptional(out bv);
- bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
+ bvars.Add(bv);
}
while (la.kind == 7) {
AttributeOrTrigger(ref attrs, ref trigs);
@@ -2015,7 +1985,6 @@ List<Expression/*!*/>/*!*/ decreases) { } else {
q = new ExistsExpr(x, bvars, range, body, trigs, attrs);
}
- parseVarScope.PopMarker();
}
@@ -2029,40 +1998,38 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(37);
x = t;
- parseVarScope.PushMarker();
IdentTypeOptional(out bv);
- bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
+ bvars.Add(bv);
while (la.kind == 19) {
Get();
IdentTypeOptional(out bv);
- bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
+ bvars.Add(bv);
}
Expect(17);
Expression(out range);
- if (la.kind == 104 || la.kind == 105) {
+ if (la.kind == 103 || la.kind == 104) {
QSep();
Expression(out body);
}
if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }
q = new SetComprehension(x, bvars, range, body);
- parseVarScope.PopMarker();
}
void Forall() {
- if (la.kind == 100) {
+ if (la.kind == 99) {
Get();
- } else if (la.kind == 101) {
+ } else if (la.kind == 100) {
Get();
- } else SynErr(146);
+ } else SynErr(145);
}
void Exists() {
- if (la.kind == 102) {
+ if (la.kind == 101) {
Get();
- } else if (la.kind == 103) {
+ } else if (la.kind == 102) {
Get();
- } else SynErr(147);
+ } else SynErr(146);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2075,16 +2042,16 @@ List<Expression/*!*/>/*!*/ decreases) { es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(148);
+ } else SynErr(147);
Expect(8);
}
void QSep() {
- if (la.kind == 104) {
+ if (la.kind == 103) {
Get();
- } else if (la.kind == 105) {
+ } else if (la.kind == 104) {
Get();
- } else SynErr(149);
+ } else SynErr(148);
}
void AttributeBody(ref Attributes attrs) {
@@ -2119,25 +2086,25 @@ List<Expression/*!*/>/*!*/ decreases) { }
static readonly bool[,]/*!*/ set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,T, 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,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,x, x,T,x,x, x,T,T,x, T,x,T,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,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,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, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,T, 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, x,x,x,x, x,x,x,x, x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x, T,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,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, x,x,x,x, x,T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,T, 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,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,x,x,x, T,T,x,T, x,T,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,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,T,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, x,x,x,x, x,x,x,x, x,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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,x, T,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}
};
} // end Parser
@@ -2209,109 +2176,108 @@ public class Errors { case 44: s = "\"match\" expected"; break;
case 45: s = "\"case\" expected"; break;
case 46: s = "\"=>\" expected"; break;
- case 47: s = "\"call\" expected"; break;
- case 48: s = "\"label\" expected"; break;
- case 49: s = "\"break\" expected"; break;
- case 50: s = "\"return\" expected"; break;
- case 51: s = "\":=\" expected"; break;
- case 52: s = "\"new\" expected"; break;
- case 53: s = "\"[\" expected"; break;
- case 54: s = "\"]\" expected"; break;
- case 55: s = "\".\" expected"; break;
- case 56: s = "\"choose\" expected"; break;
- case 57: s = "\"havoc\" expected"; break;
- case 58: s = "\"if\" expected"; break;
- case 59: s = "\"else\" expected"; break;
- case 60: s = "\"while\" expected"; break;
- case 61: s = "\"invariant\" expected"; break;
- case 62: s = "\"foreach\" expected"; break;
- case 63: s = "\"in\" expected"; break;
- case 64: s = "\"assert\" expected"; break;
- case 65: s = "\"assume\" expected"; break;
- case 66: s = "\"use\" expected"; break;
- case 67: s = "\"print\" expected"; break;
- case 68: s = "\"<==>\" expected"; break;
- case 69: s = "\"\\u21d4\" expected"; break;
- case 70: s = "\"==>\" expected"; break;
- case 71: s = "\"\\u21d2\" expected"; break;
- case 72: s = "\"&&\" expected"; break;
- case 73: s = "\"\\u2227\" expected"; break;
- case 74: s = "\"||\" expected"; break;
- case 75: s = "\"\\u2228\" 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 = "\"!in\" expected"; break;
- case 82: s = "\"\\u2260\" expected"; break;
- case 83: s = "\"\\u2264\" expected"; break;
- case 84: s = "\"\\u2265\" expected"; break;
- case 85: s = "\"+\" expected"; break;
- case 86: s = "\"-\" expected"; break;
- case 87: s = "\"/\" expected"; break;
- case 88: s = "\"%\" expected"; break;
- case 89: s = "\"!\" expected"; break;
- case 90: s = "\"\\u00ac\" expected"; break;
- case 91: s = "\"false\" expected"; break;
- case 92: s = "\"true\" expected"; break;
- case 93: s = "\"null\" expected"; break;
- case 94: s = "\"this\" expected"; break;
- case 95: s = "\"fresh\" expected"; break;
- case 96: s = "\"allocated\" expected"; break;
- case 97: s = "\"old\" expected"; break;
- case 98: s = "\"then\" expected"; break;
- case 99: s = "\"..\" expected"; break;
- case 100: s = "\"forall\" expected"; break;
- case 101: s = "\"\\u2200\" expected"; break;
- case 102: s = "\"exists\" expected"; break;
- case 103: s = "\"\\u2203\" expected"; break;
- case 104: s = "\"::\" expected"; break;
- case 105: s = "\"\\u2022\" expected"; break;
- case 106: s = "??? expected"; break;
- case 107: s = "invalid DatatypeDecl"; break;
- case 108: s = "invalid ClassMemberDecl"; break;
- case 109: s = "invalid FunctionDecl"; break;
+ case 47: s = "\"label\" expected"; break;
+ case 48: s = "\"break\" expected"; break;
+ case 49: s = "\"return\" expected"; break;
+ case 50: s = "\":=\" expected"; break;
+ case 51: s = "\"new\" expected"; break;
+ case 52: s = "\"[\" expected"; break;
+ case 53: s = "\"]\" expected"; break;
+ case 54: s = "\".\" expected"; break;
+ case 55: s = "\"choose\" expected"; break;
+ case 56: s = "\"havoc\" expected"; break;
+ case 57: s = "\"if\" expected"; break;
+ case 58: s = "\"else\" expected"; break;
+ case 59: s = "\"while\" expected"; break;
+ case 60: s = "\"invariant\" expected"; break;
+ case 61: s = "\"foreach\" expected"; break;
+ case 62: s = "\"in\" expected"; break;
+ case 63: s = "\"assert\" expected"; break;
+ case 64: s = "\"assume\" expected"; break;
+ case 65: s = "\"use\" expected"; break;
+ case 66: s = "\"print\" expected"; break;
+ case 67: s = "\"<==>\" expected"; break;
+ case 68: s = "\"\\u21d4\" expected"; break;
+ case 69: s = "\"==>\" expected"; break;
+ case 70: s = "\"\\u21d2\" expected"; break;
+ case 71: s = "\"&&\" expected"; break;
+ case 72: s = "\"\\u2227\" expected"; break;
+ case 73: s = "\"||\" expected"; break;
+ case 74: s = "\"\\u2228\" 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 = "\"!in\" expected"; break;
+ case 81: s = "\"\\u2260\" expected"; break;
+ case 82: s = "\"\\u2264\" expected"; break;
+ case 83: s = "\"\\u2265\" expected"; break;
+ case 84: s = "\"+\" expected"; break;
+ case 85: s = "\"-\" expected"; break;
+ case 86: s = "\"/\" expected"; break;
+ case 87: s = "\"%\" expected"; break;
+ case 88: s = "\"!\" expected"; break;
+ case 89: s = "\"\\u00ac\" expected"; break;
+ case 90: s = "\"false\" expected"; break;
+ case 91: s = "\"true\" expected"; break;
+ case 92: s = "\"null\" expected"; break;
+ case 93: s = "\"this\" expected"; break;
+ case 94: s = "\"fresh\" expected"; break;
+ case 95: s = "\"allocated\" expected"; break;
+ case 96: s = "\"old\" expected"; break;
+ case 97: s = "\"then\" expected"; break;
+ case 98: s = "\"..\" expected"; break;
+ case 99: s = "\"forall\" expected"; break;
+ case 100: s = "\"\\u2200\" expected"; break;
+ case 101: s = "\"exists\" expected"; break;
+ case 102: s = "\"\\u2203\" expected"; break;
+ case 103: s = "\"::\" expected"; break;
+ case 104: s = "\"\\u2022\" expected"; break;
+ case 105: s = "??? expected"; break;
+ case 106: s = "invalid DatatypeDecl"; break;
+ case 107: s = "invalid ClassMemberDecl"; break;
+ case 108: s = "invalid FunctionDecl"; break;
+ case 109: s = "invalid MethodDecl"; break;
case 110: s = "invalid MethodDecl"; break;
- case 111: s = "invalid MethodDecl"; break;
- case 112: s = "invalid TypeAndToken"; break;
+ case 111: s = "invalid TypeAndToken"; break;
+ case 112: s = "invalid MethodSpec"; break;
case 113: s = "invalid MethodSpec"; break;
- case 114: s = "invalid MethodSpec"; break;
- case 115: s = "invalid ReferenceType"; break;
- case 116: s = "invalid FunctionSpec"; break;
- case 117: s = "invalid FunctionBody"; break;
- case 118: s = "invalid PossiblyWildFrameExpression"; break;
- case 119: s = "invalid PossiblyWildExpression"; break;
- case 120: s = "invalid MatchOrExpr"; break;
- case 121: s = "invalid OneStmt"; break;
- case 122: s = "invalid UpdateStmt"; break;
+ case 114: s = "invalid ReferenceType"; break;
+ case 115: s = "invalid FunctionSpec"; break;
+ case 116: s = "invalid FunctionBody"; break;
+ case 117: s = "invalid PossiblyWildFrameExpression"; break;
+ case 118: s = "invalid PossiblyWildExpression"; break;
+ case 119: s = "invalid MatchOrExpr"; break;
+ case 120: s = "invalid OneStmt"; break;
+ case 121: s = "invalid UpdateStmt"; break;
+ case 122: s = "invalid IfStmt"; break;
case 123: s = "invalid IfStmt"; break;
- case 124: s = "invalid IfStmt"; break;
- case 125: s = "invalid WhileStmt"; break;
- case 126: s = "invalid ForeachStmt"; break;
- case 127: s = "invalid Lhs"; break;
- case 128: s = "invalid Rhs"; break;
- case 129: s = "invalid Guard"; break;
- case 130: s = "invalid AttributeArg"; break;
- case 131: s = "invalid EquivOp"; break;
- case 132: s = "invalid ImpliesOp"; break;
- case 133: s = "invalid AndOp"; break;
- case 134: s = "invalid OrOp"; break;
- case 135: s = "invalid RelOp"; break;
- case 136: s = "invalid AddOp"; break;
- case 137: s = "invalid UnaryExpression"; break;
- case 138: s = "invalid MulOp"; break;
- case 139: s = "invalid NegOp"; break;
- case 140: s = "invalid EndlessExpression"; break;
+ case 124: s = "invalid WhileStmt"; break;
+ case 125: s = "invalid ForeachStmt"; break;
+ case 126: s = "invalid Lhs"; break;
+ case 127: s = "invalid Rhs"; break;
+ case 128: s = "invalid Guard"; break;
+ case 129: s = "invalid AttributeArg"; break;
+ case 130: s = "invalid EquivOp"; break;
+ case 131: s = "invalid ImpliesOp"; break;
+ case 132: s = "invalid AndOp"; break;
+ case 133: s = "invalid OrOp"; break;
+ case 134: s = "invalid RelOp"; break;
+ case 135: s = "invalid AddOp"; break;
+ case 136: s = "invalid UnaryExpression"; break;
+ case 137: s = "invalid MulOp"; break;
+ case 138: s = "invalid NegOp"; break;
+ case 139: s = "invalid EndlessExpression"; break;
+ case 140: s = "invalid Suffix"; break;
case 141: s = "invalid Suffix"; break;
case 142: s = "invalid Suffix"; break;
- case 143: s = "invalid Suffix"; break;
- case 144: s = "invalid ConstAtomExpression"; break;
- case 145: s = "invalid QuantifierGuts"; break;
- case 146: s = "invalid Forall"; break;
- case 147: s = "invalid Exists"; break;
- case 148: s = "invalid AttributeOrTrigger"; break;
- case 149: s = "invalid QSep"; break;
+ case 143: s = "invalid ConstAtomExpression"; break;
+ case 144: s = "invalid QuantifierGuts"; break;
+ case 145: s = "invalid Forall"; break;
+ case 146: s = "invalid Exists"; break;
+ case 147: s = "invalid AttributeOrTrigger"; break;
+ case 148: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 9b931f73..8722cd63 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1234,6 +1234,9 @@ namespace Microsoft.Dafny { var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, s.Rhss[i]);
s.ResolvedStatements.Add(a);
}
+ if (s.Lhss.Count != 1) {
+ Error(s, "multi-assignments not yet supported"); // TODO
+ }
}
} else {
// if there was an effectful RHS, that must be the only RHS
@@ -1251,14 +1254,15 @@ namespace Microsoft.Dafny { } else {
// a call statement
if (ErrorCount == prevErrorCount) {
-#if !FULL_LHS_SUPPORT_FOR_CALLS
var idLhss = new List<IdentifierExpr>();
foreach (var ll in s.Lhss) {
- var ie = (IdentifierExpr)ll.Resolved; // TODO: the CallStmt should handle all LHS's, not just identifier expressions
- Contract.Assert(ie != null);
- idLhss.Add(ie);
+ var ie = ll.Resolved as IdentifierExpr; // TODO: the CallStmt should handle all LHS's, not just identifier expressions
+ if (ie == null) {
+ Error(ll, "actual out-parameters of calls must be variables, not fields");
+ } else {
+ idLhss.Add(ie);
+ }
}
-#endif
var a = new CallStmt(callRhs.Tok, idLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);
s.ResolvedStatements.Add(a);
}
@@ -1736,11 +1740,15 @@ namespace Microsoft.Dafny { if (callee.IsStatic) {
Error(s.Tok, "a method called as an initialization method must not be 'static'");
}
- } else if (!scope.AllowInstance && !callee.IsStatic && s.Receiver is ThisExpr) {
- // The call really needs an instance, but that instance is given as 'this', which is not
- // available in this context. For more details, see comment in the resolution of a
- // FunctionCallExpr.
- Error(s.Receiver, "'this' is not allowed in a 'static' context");
+ } else if (!callee.IsStatic) {
+ if (!scope.AllowInstance && s.Receiver is ThisExpr) {
+ // The call really needs an instance, but that instance is given as 'this', which is not
+ // available in this context. For more details, see comment in the resolution of a
+ // FunctionCallExpr.
+ Error(s.Receiver, "'this' is not allowed in a 'static' context");
+ } else if (s.Receiver is StaticReceiverExpr) {
+ Error(s.Receiver, "call to instance method requires an instance");
+ }
}
// build the type substitution map
Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
@@ -2653,15 +2661,19 @@ namespace Microsoft.Dafny { Error(e, "wrong number of function arguments (got {0}, expected {1})", e.Args.Count, function.Formals.Count);
} else {
Contract.Assert(ctype != null); // follows from postcondition of ResolveMember
- if (!scope.AllowInstance && !function.IsStatic && e.Receiver is ThisExpr) {
- // The call really needs an instance, but that instance is given as 'this', which is not
- // available in this context. In most cases, occurrences of 'this' inside e.Receiver would
- // have been caught in the recursive call to resolve e.Receiver, but not the specific case
- // of e.Receiver being 'this' (explicitly or implicitly), for that case needs to be allowed
- // in the event that a class function calls another class function (and note that we need the
- // type of the receiver in order to find the method, so we could not have made this check
- // earlier).
- Error(e.Receiver, "'this' is not allowed in a 'static' context");
+ if (!function.IsStatic) {
+ if (!scope.AllowInstance && e.Receiver is ThisExpr) {
+ // The call really needs an instance, but that instance is given as 'this', which is not
+ // available in this context. In most cases, occurrences of 'this' inside e.Receiver would
+ // have been caught in the recursive call to resolve e.Receiver, but not the specific case
+ // of e.Receiver being 'this' (explicitly or implicitly), for that case needs to be allowed
+ // in the event that a static function calls another static function (and note that we need the
+ // type of the receiver in order to find the method, so we could not have made this check
+ // earlier).
+ Error(e.Receiver, "'this' is not allowed in a 'static' context");
+ } else if (e.Receiver is StaticReceiverExpr) {
+ Error(e.Receiver, "call to instance function requires an instance");
+ }
}
// build the type substitution map
Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index ba5a745d..7d750553 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 106;
- const int noSym = 106;
+ const int maxT = 105;
+ const int noSym = 105;
[ContractInvariantMethod]
@@ -515,33 +515,32 @@ public class Scanner { case "reads": t.kind = 41; break;
case "match": t.kind = 44; break;
case "case": t.kind = 45; break;
- case "call": t.kind = 47; break;
- case "label": t.kind = 48; break;
- case "break": t.kind = 49; break;
- case "return": t.kind = 50; break;
- case "new": t.kind = 52; break;
- case "choose": t.kind = 56; break;
- case "havoc": t.kind = 57; break;
- case "if": t.kind = 58; break;
- case "else": t.kind = 59; break;
- case "while": t.kind = 60; break;
- case "invariant": t.kind = 61; break;
- case "foreach": t.kind = 62; break;
- case "in": t.kind = 63; break;
- case "assert": t.kind = 64; break;
- case "assume": t.kind = 65; break;
- case "use": t.kind = 66; break;
- case "print": t.kind = 67; break;
- case "false": t.kind = 91; break;
- case "true": t.kind = 92; break;
- case "null": t.kind = 93; break;
- case "this": t.kind = 94; break;
- case "fresh": t.kind = 95; break;
- case "allocated": t.kind = 96; break;
- case "old": t.kind = 97; break;
- case "then": t.kind = 98; break;
- case "forall": t.kind = 100; break;
- case "exists": t.kind = 102; break;
+ case "label": t.kind = 47; break;
+ case "break": t.kind = 48; break;
+ case "return": t.kind = 49; break;
+ case "new": t.kind = 51; break;
+ case "choose": t.kind = 55; break;
+ case "havoc": t.kind = 56; break;
+ case "if": t.kind = 57; break;
+ case "else": t.kind = 58; break;
+ case "while": t.kind = 59; break;
+ case "invariant": t.kind = 60; break;
+ case "foreach": t.kind = 61; break;
+ case "in": t.kind = 62; break;
+ case "assert": t.kind = 63; break;
+ case "assume": t.kind = 64; break;
+ case "use": t.kind = 65; break;
+ case "print": t.kind = 66; break;
+ case "false": t.kind = 90; break;
+ case "true": t.kind = 91; break;
+ case "null": t.kind = 92; break;
+ case "this": t.kind = 93; break;
+ case "fresh": t.kind = 94; break;
+ case "allocated": t.kind = 95; break;
+ case "old": t.kind = 96; break;
+ case "then": t.kind = 97; break;
+ case "forall": t.kind = 99; break;
+ case "exists": t.kind = 101; break;
default: break;
}
}
@@ -661,70 +660,70 @@ public class Scanner { case 25:
{t.kind = 46; break;}
case 26:
- {t.kind = 51; break;}
+ {t.kind = 50; break;}
case 27:
- {t.kind = 53; break;}
+ {t.kind = 52; break;}
case 28:
- {t.kind = 54; break;}
+ {t.kind = 53; break;}
case 29:
if (ch == '>') {AddCh(); goto case 30;}
else {goto case 0;}
case 30:
- {t.kind = 68; break;}
+ {t.kind = 67; break;}
case 31:
- {t.kind = 69; break;}
+ {t.kind = 68; break;}
case 32:
- {t.kind = 70; break;}
+ {t.kind = 69; break;}
case 33:
- {t.kind = 71; break;}
+ {t.kind = 70; break;}
case 34:
if (ch == '&') {AddCh(); goto case 35;}
else {goto case 0;}
case 35:
- {t.kind = 72; break;}
+ {t.kind = 71; break;}
case 36:
- {t.kind = 73; break;}
+ {t.kind = 72; break;}
case 37:
- {t.kind = 74; break;}
+ {t.kind = 73; break;}
case 38:
- {t.kind = 75; break;}
+ {t.kind = 74; break;}
case 39:
- {t.kind = 78; break;}
+ {t.kind = 77; break;}
case 40:
- {t.kind = 79; break;}
+ {t.kind = 78; break;}
case 41:
- {t.kind = 80; break;}
+ {t.kind = 79; break;}
case 42:
if (ch == 'n') {AddCh(); goto case 43;}
else {goto case 0;}
case 43:
- {t.kind = 81; break;}
+ {t.kind = 80; break;}
case 44:
- {t.kind = 82; break;}
+ {t.kind = 81; break;}
case 45:
- {t.kind = 83; break;}
+ {t.kind = 82; break;}
case 46:
- {t.kind = 84; break;}
+ {t.kind = 83; break;}
case 47:
- {t.kind = 85; break;}
+ {t.kind = 84; break;}
case 48:
- {t.kind = 86; break;}
+ {t.kind = 85; break;}
case 49:
- {t.kind = 87; break;}
+ {t.kind = 86; break;}
case 50:
- {t.kind = 88; break;}
+ {t.kind = 87; break;}
case 51:
- {t.kind = 90; break;}
+ {t.kind = 89; break;}
case 52:
- {t.kind = 99; break;}
+ {t.kind = 98; break;}
case 53:
- {t.kind = 101; break;}
+ {t.kind = 100; break;}
case 54:
- {t.kind = 103; break;}
+ {t.kind = 102; break;}
case 55:
- {t.kind = 104; break;}
+ {t.kind = 103; break;}
case 56:
- {t.kind = 105; break;}
+ {t.kind = 104; break;}
case 57:
recEnd = pos; recKind = 16;
if (ch == '>') {AddCh(); goto case 25;}
@@ -748,23 +747,23 @@ public class Scanner { if (ch == '=') {AddCh(); goto case 39;}
else {t.kind = 24; break;}
case 62:
- recEnd = pos; recKind = 55;
+ recEnd = pos; recKind = 54;
if (ch == '.') {AddCh(); goto case 52;}
- else {t.kind = 55; break;}
+ else {t.kind = 54; break;}
case 63:
- recEnd = pos; recKind = 89;
+ recEnd = pos; recKind = 88;
if (ch == '=') {AddCh(); goto case 40;}
else if (ch == '!') {AddCh(); goto case 41;}
else if (ch == 'i') {AddCh(); goto case 42;}
- else {t.kind = 89; break;}
+ else {t.kind = 88; break;}
case 64:
- recEnd = pos; recKind = 76;
+ recEnd = pos; recKind = 75;
if (ch == '>') {AddCh(); goto case 32;}
- else {t.kind = 76; break;}
+ else {t.kind = 75; break;}
case 65:
- recEnd = pos; recKind = 77;
+ recEnd = pos; recKind = 76;
if (ch == '=') {AddCh(); goto case 29;}
- else {t.kind = 77; break;}
+ else {t.kind = 76; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 28281820..ca19af7b 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2983,8 +2983,7 @@ namespace Microsoft.Dafny { locals.Add(var);
} else if (stmt is CallStmt) {
- CallStmt s = (CallStmt)stmt;
- TrCallStmt(s, builder, locals, etran, null);
+ TrCallStmt((CallStmt)stmt, builder, locals, etran, null);
} else if (stmt is BlockStmt) {
foreach (Statement ss in ((BlockStmt)stmt).Body) {
diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy index 1b105ac1..3db9bf72 100644 --- a/Test/VSComp2010/Problem1-SumMax.dfy +++ b/Test/VSComp2010/Problem1-SumMax.dfy @@ -38,6 +38,6 @@ method Main() a[7] := 1;
a[8] := 10;
a[9] := 6;
- call s, m := M(10, a);
+ var s, m := M(10, a);
print "N = ", a.Length, " sum = ", s, " max = ", m, "\n";
}
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy index bf6aca37..2a262d70 100644 --- a/Test/VSComp2010/Problem2-Invert.dfy +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -61,11 +61,11 @@ method Main() a[8] := 5;
a[9] := 6;
var b := new int[10];
- call M(10, a, b);
+ M(10, a, b);
print "a:\n";
- call PrintArray(a);
+ PrintArray(a);
print "b:\n";
- call PrintArray(b);
+ PrintArray(b);
}
method PrintArray(a: array<int>)
diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy index 03e6bdfe..3d24255d 100644 --- a/Test/VSComp2010/Problem3-FindZero.dfy +++ b/Test/VSComp2010/Problem3-FindZero.dfy @@ -82,11 +82,11 @@ static method Search(ll: Node) returns (r: int) method Main()
{
var list: Node := null;
- call list := list.Cons(0, list);
- call list := list.Cons(5, list);
- call list := list.Cons(0, list);
- call list := list.Cons(8, list);
- call r := Search(list);
+ list := list.Cons(0, list);
+ list := list.Cons(5, list);
+ list := list.Cons(0, list);
+ list := list.Cons(8, list);
+ var r := Search(list);
print "Search returns ", r, "\n";
assert r == 1;
}
diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy index ef084674..2f21b7a1 100644 --- a/Test/VSComp2010/Problem4-Queens.dfy +++ b/Test/VSComp2010/Problem4-Queens.dfy @@ -39,7 +39,7 @@ method Search(N: int) returns (success: bool, board: seq<int>) ==>
(exists p :: 0 <= p && p < N && !IsConsistent(B, p)));
{
- call success, board := SearchAux(N, []);
+ success, board := SearchAux(N, []);
}
// Given a board, this function says whether or not the queen placed in column 'pos'
@@ -110,7 +110,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: // Thus, we meet the precondition of 'SearchAux' on 'candidateBoard', so let's search
// for a solution that extends 'candidateBoard'.
- call s, b := SearchAux(N, candidateBoard);
+ var s, b := SearchAux(N, candidateBoard);
if (s) {
// The recursive call to 'SearchAux' found consistent positions for all remaining columns
newBoard := b;
@@ -137,11 +137,11 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: method Main()
{
- call s, b := Search(2);
+ var s, b := Search(2);
print "N=2 returns ", s, "\n";
- call s, b := Search(4);
+ s, b := Search(4);
print "N=4 returns ", s, "\n";
- call PrintSeq(b);
+ PrintSeq(b);
}
method PrintSeq(b: seq<int>)
diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy index df8cb1b7..0e141927 100644 --- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy +++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy @@ -46,8 +46,8 @@ class AmortizedQueue<T> { front := f;
rear := r;
} else {
- call rr := r.Reverse();
- call ff := f.Concat(rr);
+ var rr := r.Reverse();
+ var ff := f.Concat(rr);
front := ff;
rear := new LinkedList<T>.Init();
@@ -75,7 +75,7 @@ class AmortizedQueue<T> { requires Valid();
ensures r != null && r.Valid() && r.List == List + [item];
{
- call rr := rear.Cons(item);
+ var rr := rear.Cons(item);
r := new AmortizedQueue<T>.InitFromPieces(front, rr);
}
}
@@ -133,8 +133,8 @@ class LinkedList<T> { if (length == 0) {
r := end;
} else {
- call c := tail.Concat(end);
- call r := c.Cons(head);
+ var c := tail.Concat(end);
+ r := c.Cons(head);
}
}
@@ -148,10 +148,10 @@ class LinkedList<T> { if (length == 0) {
r := this;
} else {
- call r := tail.Reverse();
+ r := tail.Reverse();
var e := new LinkedList<T>.Init();
- call e := e.Cons(head);
- call r := r.Concat(e);
+ e := e.Cons(head);
+ r := r.Concat(e);
}
}
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy index cd4a18c2..3bd2bf43 100644 --- a/Test/VSI-Benchmarks/b1.dfy +++ b/Test/VSI-Benchmarks/b1.dfy @@ -35,37 +35,37 @@ method Mul(x: int, y: int) returns (r: int) if (x == 0) {
r := 0;
} else if (x < 0) {
- call r := Mul(-x, y);
+ r := Mul(-x, y);
r := -r;
} else {
- call r := Mul(x-1, y);
- call r := Add(r, y);
+ r := Mul(x-1, y);
+ r := Add(r, y);
}
}
// ---------------------------
method Main() {
- call TestAdd(3, 180);
- call TestAdd(3, -180);
- call TestAdd(0, 1);
+ TestAdd(3, 180);
+ TestAdd(3, -180);
+ TestAdd(0, 1);
- call TestMul(3, 180);
- call TestMul(3, -180);
- call TestMul(180, 3);
- call TestMul(-180, 3);
- call TestMul(0, 1);
- call TestMul(1, 0);
+ TestMul(3, 180);
+ TestMul(3, -180);
+ TestMul(180, 3);
+ TestMul(-180, 3);
+ TestMul(0, 1);
+ TestMul(1, 0);
}
method TestAdd(x: int, y: int) {
print x, " + ", y, " = ";
- call z := Add(x, y);
+ var z := Add(x, y);
print z, "\n";
}
method TestMul(x: int, y: int) {
print x, " * ", y, " = ";
- call z := Mul(x, y);
+ var z := Mul(x, y);
print z, "\n";
}
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index 6c6f11b3..3046621b 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -38,13 +38,13 @@ method Main() { a[2] := -2;
a[3] := 0;
a[4] := 25;
- call TestSearch(a, 4);
- call TestSearch(a, -8);
- call TestSearch(a, -2);
- call TestSearch(a, 0);
- call TestSearch(a, 23);
- call TestSearch(a, 25);
- call TestSearch(a, 27);
+ TestSearch(a, 4);
+ TestSearch(a, -8);
+ TestSearch(a, -2);
+ TestSearch(a, 0);
+ TestSearch(a, 23);
+ TestSearch(a, 25);
+ TestSearch(a, 27);
}
method TestSearch(a: array<int>, key: int)
@@ -52,6 +52,6 @@ method TestSearch(a: array<int>, key: int) requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);
{
var b := new Benchmark2;
- call r := b.BinarySearch(a, key);
+ var r := b.BinarySearch(a, key);
print "Looking for key=", key, ", result=", r, "\n";
}
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 3f30c4b5..3de94555 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -87,10 +87,10 @@ class Benchmark3 { invariant (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
invariant (forall i :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]);
{
- call m,k := RemoveMin(q);
+ var m,k := RemoveMin(q);
perm := perm + [p[k]]; //adds index of min to perm
p := p[k+1..] + p[..k]; //remove index of min from p
- call r.Enqueue(m);
+ r.Enqueue(m);
pperm := pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] + [pperm[k]];
}
}
@@ -116,8 +116,8 @@ class Benchmark3 { invariant 0 <= k && k < |old(q.contents)| && old(q.contents)[k] == m;
invariant (forall i :: 0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far
{
- call x:= q.Dequeue();
- call q.Enqueue(x);
+ var x := q.Dequeue();
+ q.Enqueue(x);
if (x < m) { k := j; m := x; }
j := j+1;
}
@@ -127,11 +127,11 @@ class Benchmark3 { invariant j <= k;
invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j];
{
- call x := q.Dequeue();
- call q.Enqueue(x);
+ var x := q.Dequeue();
+ q.Enqueue(x);
j := j+1;
}
- call m:= q.Dequeue();
+ m := q.Dequeue();
}
}
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index 9f7e272e..b70ff4d0 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -54,7 +54,7 @@ class Map<Key,Value> { ensures !present ==> key !in Keys;
ensures present ==> (exists i :: 0 <= i && i < |Keys| && Keys[i] == key && Values[i] == val);
{
- call p, n, prev := FindIndex(key);
+ var p, n, prev := FindIndex(key);
if (p == null) {
present := false;
} else {
@@ -74,7 +74,7 @@ class Map<Key,Value> { Keys[j] == old(Keys)[j] && Values[j] == old(Values)[j]));
ensures key !in old(Keys) ==> Keys == [key] + old(Keys) && Values == [val] + old(Values);
{
- call p, n, prev := FindIndex(key);
+ var p, n, prev := FindIndex(key);
if (p == null) {
var h := new Node<Key,Value>;
h.key := key; h.val := val; h.next := head;
@@ -107,7 +107,7 @@ class Map<Key,Value> { Keys[h..] == old(Keys)[h+1..] &&
Values[h..] == old(Values)[h+1..]);
{
- call p, n, prev := FindIndex(key);
+ var p, n, prev := FindIndex(key);
if (p != null) {
Keys := Keys[..n] + Keys[n+1..];
Values := Values[..n] + Values[n+1..];
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy index d9bd36f5..cd132ef3 100644 --- a/Test/VSI-Benchmarks/b5.dfy +++ b/Test/VSI-Benchmarks/b5.dfy @@ -98,9 +98,9 @@ class Queue<T> { ensures Valid() && fresh(footprint - old(footprint));
ensures contents == old(contents)[1..] + old(contents)[..1];
{
- call t := Front();
- call Dequeue();
- call Enqueue(t);
+ var t := Front();
+ Dequeue();
+ Enqueue(t);
}
method RotateAny()
@@ -112,9 +112,9 @@ class Queue<T> { ensures (exists i :: 0 <= i && i <= |contents| &&
contents == old(contents)[i..] + old(contents)[..i]);
{
- call t := Front();
- call Dequeue();
- call Enqueue(t);
+ var t := Front();
+ Dequeue();
+ Enqueue(t);
}
}
@@ -152,18 +152,18 @@ class Main<U> { var q0 := new Queue<T>.Init();
var q1 := new Queue<T>.Init();
- call q0.Enqueue(t);
- call q0.Enqueue(u);
+ q0.Enqueue(t);
+ q0.Enqueue(u);
- call q1.Enqueue(v);
+ q1.Enqueue(v);
assert |q0.contents| == 2;
- call w := q0.Front();
+ var w := q0.Front();
assert w == t;
- call q0.Dequeue();
+ q0.Dequeue();
- call w := q0.Front();
+ w := q0.Front();
assert w == u;
assert |q0.contents| == 1;
@@ -179,18 +179,18 @@ class Main<U> { ensures fresh(q0.footprint - old(q0.footprint));
ensures fresh(q1.footprint - old(q1.footprint));
{
- call q0.Enqueue(t);
- call q0.Enqueue(u);
+ q0.Enqueue(t);
+ q0.Enqueue(u);
- call q1.Enqueue(v);
+ q1.Enqueue(v);
assert |q0.contents| == 2;
- call w := q0.Front();
+ var w := q0.Front();
assert w == t;
- call q0.Dequeue();
+ q0.Dequeue();
- call w := q0.Front();
+ w := q0.Front();
assert w == u;
assert |q0.contents| == 1;
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy index 13086f28..fda9ca74 100644 --- a/Test/VSI-Benchmarks/b6.dfy +++ b/Test/VSI-Benchmarks/b6.dfy @@ -107,14 +107,14 @@ class Client method Main()
{
var c := new Collection<int>.Init();
- call c.Add(33);
- call c.Add(45);
- call c.Add(78);
+ c.Add(33);
+ c.Add(45);
+ c.Add(78);
var s := [];
- call iter := c.GetIterator();
- call b := iter.MoveNext();
+ var iter := c.GetIterator();
+ var b := iter.MoveNext();
while (b)
invariant iter.Valid() && b == iter.HasCurrent() && fresh(iter.footprint);
@@ -123,13 +123,13 @@ class Client invariant iter.c == c;
decreases |c.elements| - iter.pos;
{
- call x := iter.GetCurrent();
+ var x := iter.GetCurrent();
s := s + [x];
- call b := iter.MoveNext();
+ b := iter.MoveNext();
}
assert s == c.elements; //verifies that the iterator returns the correct things
- call c.Add(100);
+ c.Add(100);
}
}
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index 2304e602..f34f5c00 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -119,33 +119,34 @@ class Client { method Main()
{
var rd := new Stream;
- call rd.Open();
+ rd.Open();
var q := new Queue<int>;
while (true)
invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
decreases |rd.stream|;
{
- call eos := rd.AtEndOfStream();
+ var eos := rd.AtEndOfStream();
if (eos) {
break;
}
- call ch := rd.GetChar();
- call q.Enqueue(ch);
+ var ch := rd.GetChar();
+ q.Enqueue(ch);
}
- call rd.Close();
- call q,perm := Sort(q);
+ rd.Close();
+ var perm;
+ q,perm := Sort(q);
- var wr:= new Stream;
- call wr.Create();
+ var wr := new Stream;
+ wr.Create();
while (0 < |q.contents|)
invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;
{
- call ch := q.Dequeue();
- call wr.PutChar(ch);
+ var ch := q.Dequeue();
+ wr.PutChar(ch);
}
- call wr.Close();
+ wr.Close();
}
}
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index 3438d6e0..0c9d1186 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -46,7 +46,7 @@ class Glossary { method Main()
{
var rs:= new ReaderStream;
- call rs.Open();
+ rs.Open();
var glossary := new Map<Word,seq<Word>>.Init();
var q := new Queue<Word>.Init();
@@ -60,21 +60,22 @@ class Glossary { invariant q.contents == glossary.keys;
decreases *; // we leave out the decreases clause - unbounded stream
{
- call term,definition := readDefinition(rs);
+ var term,definition := readDefinition(rs);
if (term == null) {
break;
}
- call present, d := glossary.Find(term);
+ var present, d := glossary.Find(term);
if (!present) {
- call glossary.Add(term,definition);
- call q.Enqueue(term);
+ glossary.Add(term,definition);
+ q.Enqueue(term);
}
}
- call rs.Close();
- call q,p := Sort(q);
+ rs.Close();
+ var p;
+ q,p := Sort(q);
var wr := new WriterStream;
- call wr.Create();
+ wr.Create();
while (0 < |q.contents|)
invariant wr.Valid() && fresh(wr.footprint);
@@ -84,12 +85,12 @@ class Glossary { invariant q !in wr.footprint;
invariant (forall k :: k in q.contents ==> k in glossary.keys);
{
- call term := q.Dequeue();
- call present,definition := glossary.Find(term);
+ var term := q.Dequeue();
+ var present,definition := glossary.Find(term);
assert present;
// write term with a html anchor
- call wr.PutWordInsideTag(term, term);
+ wr.PutWordInsideTag(term, term);
var i := 0;
var qcon := q.contents;
@@ -103,19 +104,20 @@ class Glossary { invariant (forall k :: k in q.contents ==> k in glossary.keys);
{
var w := definition[i];
- call present, d := glossary.Find(w);
+ var d;
+ present, d := glossary.Find(w);
if (present)
{
- call wr. PutWordInsideHyperlink(w, w);
+ wr. PutWordInsideHyperlink(w, w);
}
else
{
- call wr. PutWord(w);
+ wr. PutWord(w);
}
i:= i +1;
}
}
- call wr.Close();
+ wr.Close();
}
@@ -125,7 +127,7 @@ class Glossary { ensures rs.Valid() && fresh(rs.footprint - old(rs.footprint));
ensures term != null ==> null !in definition;
{
- call term := rs.GetWord();
+ term := rs.GetWord();
if (term != null)
{
definition := [];
@@ -134,7 +136,7 @@ class Glossary { invariant null !in definition;
decreases *; // we leave out the decreases clause - unbounded stream
{
- call w := rs.GetWord();
+ var w := rs.GetWord();
if (w == null)
{
break;
@@ -273,7 +275,7 @@ class Map<Key,Value> { ensures present ==> (exists i :: 0 <= i && i < |keys| &&
keys[i] == key && values[i] == val);
{
- call j := FindIndex(key);
+ var j := FindIndex(key);
if (j == -1) {
present := false;
} else {
@@ -292,7 +294,7 @@ class Map<Key,Value> { (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));
ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];
{
- call j := FindIndex(key);
+ var j := FindIndex(key);
if (j == -1) {
keys := keys + [key];
values := values + [val];
@@ -321,7 +323,7 @@ class Map<Key,Value> { keys[h..] == old(keys)[h+1..] &&
values[h..] == old(values)[h+1..]);
{
- call j := FindIndex(key);
+ var j := FindIndex(key);
if (0 <= j) {
keys := keys[..j] + keys[j+1..];
values := values[..j] + values[j+1..];
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 289a597d..efcfa8bb 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -22,10 +22,10 @@ class MyClass<T, U> { } else {
this.x := x + 0;
}
- call t, u, v := M(true, lotsaObjects);
+ t, u, v := M(true, lotsaObjects);
var to: MyClass<T,U>;
- call to, u, v := M(true, lotsaObjects);
- call to, u, v := to.M(true, lotsaObjects);
+ to, u, v := this.M(true, lotsaObjects);
+ to, u, v := to.M(true, lotsaObjects);
assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
}
}
@@ -70,9 +70,9 @@ TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, g TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
-TypeTests.dfy(11,4): Error: incorrect type of method in-parameter 0 (expected int, got bool)
-TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected int, got C)
-TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int)
+TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
+TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed
TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
@@ -85,12 +85,12 @@ TypeTests.dfy(80,17): Error: a method called as an initialization method must no TypeTests.dfy(89,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
TypeTests.dfy(90,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
TypeTests.dfy(96,9): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(97,6): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(98,6): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(97,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(98,8): Error: sorry, cannot instantiate 'array' type with a subrange type
22 resolution/type errors detected in TypeTests.dfy
-------------------- NatTypes.dfy --------------------
-NatTypes.dfy(7,10): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
NatTypes.dfy(31,5): Error: value assigned to a nat must be non-negative
@@ -119,7 +119,7 @@ Execution trace: (0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-NatTypes.dfy(89,9): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(89,16): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
@@ -160,11 +160,11 @@ Execution trace: (0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(129,7): Error: call may violate caller's modifies clause
+SmallTests.dfy(129,9): Error: call may violate caller's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(131,7): Error: call may violate caller's modifies clause
+SmallTests.dfy(131,9): Error: call may violate caller's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
@@ -402,7 +402,7 @@ Execution trace: Dafny program verifier finished with 3 verified, 3 errors
-------------------- ResolutionErrors.dfy --------------------
-ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'class' context
+ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
@@ -410,9 +410,11 @@ ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got arra ResolutionErrors.dfy(45,14): Error: a field must be selected via an object, not just a class name
ResolutionErrors.dfy(46,7): Error: unresolved identifier: F
ResolutionErrors.dfy(47,14): Error: an instance function must be selected via an object, not just a class name
+ResolutionErrors.dfy(47,7): Error: call to instance function requires an instance
ResolutionErrors.dfy(48,7): Error: unresolved identifier: G
-ResolutionErrors.dfy(50,2): Error: member M does not exist in class _default
-ResolutionErrors.dfy(52,2): Error: member N does not exist in class _default
+ResolutionErrors.dfy(50,7): Error: unresolved identifier: M
+ResolutionErrors.dfy(51,7): Error: call to instance method requires an instance
+ResolutionErrors.dfy(52,7): Error: unresolved identifier: N
ResolutionErrors.dfy(55,8): Error: non-function expression is called with parameters
ResolutionErrors.dfy(56,14): Error: member z does not exist in class Global
ResolutionErrors.dfy(75,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -420,7 +422,7 @@ ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype construc ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
-18 resolution/type errors detected in ResolutionErrors.dfy
+20 resolution/type errors detected in ResolutionErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
@@ -512,11 +514,11 @@ Dafny program verifier finished with 7 verified, 1 error Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
Modules0.dfy(13,7): Error: module T named among imports does not exist
Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G
-Modules0.dfy(51,6): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
-Modules0.dfy(62,6): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
-Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
-Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
-Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts
+Modules0.dfy(51,8): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
+Modules0.dfy(62,9): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
+Modules0.dfy(72,9): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
+Modules0.dfy(91,6): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
+Modules0.dfy(116,11): Error: ghost variables are allowed only in specification contexts
Modules0.dfy(130,11): Error: old expressions are allowed only in specification and ghost contexts
Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification and ghost contexts
Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts
@@ -599,57 +601,57 @@ Execution trace: Dafny program verifier finished with 15 verified, 6 errors
-------------------- Termination.dfy --------------------
-Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(103,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
- Termination.dfy(102,3): anon7_LoopHead
+ Termination.dfy(103,3): anon7_LoopHead
(0,0): anon7_LoopBody
- Termination.dfy(102,3): anon8_Else
+ Termination.dfy(103,3): anon8_Else
(0,0): anon3
- Termination.dfy(102,3): anon9_Else
+ Termination.dfy(103,3): anon9_Else
(0,0): anon5
-Termination.dfy(110,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(111,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
- Termination.dfy(110,3): anon9_LoopHead
+ Termination.dfy(111,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(110,3): anon10_Else
+ Termination.dfy(111,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(110,3): anon12_Else
+ Termination.dfy(111,3): anon12_Else
(0,0): anon7
-Termination.dfy(119,3): Error: decreases expression might not decrease
+Termination.dfy(120,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
- Termination.dfy(119,3): anon9_LoopHead
+ Termination.dfy(120,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(119,3): anon10_Else
+ Termination.dfy(120,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(119,3): anon12_Else
+ Termination.dfy(120,3): anon12_Else
(0,0): anon7
-Termination.dfy(120,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
+Termination.dfy(121,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
(0,0): anon0
- Termination.dfy(119,3): anon9_LoopHead
+ Termination.dfy(120,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(119,3): anon10_Else
+ Termination.dfy(120,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(119,3): anon12_Else
+ Termination.dfy(120,3): anon12_Else
(0,0): anon7
-Termination.dfy(248,35): Error: cannot prove termination; try supplying a decreases clause
+Termination.dfy(249,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-Termination.dfy(288,3): Error: decreases expression might not decrease
+Termination.dfy(289,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
- Termination.dfy(288,3): anon10_LoopHead
+ Termination.dfy(289,3): anon10_LoopHead
(0,0): anon10_LoopBody
- Termination.dfy(288,3): anon11_Else
- Termination.dfy(288,3): anon12_Else
+ Termination.dfy(289,3): anon11_Else
+ Termination.dfy(289,3): anon12_Else
(0,0): anon13_Else
(0,0): anon8
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 1eeb2d92..e6b9a87d 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -23,19 +23,19 @@ method TestCalls(k: nat) { ghost var r: int;
ghost var s := Global.G(k);
-// call r := Global.N(k);
+// r := Global.N(k);
// assert r == s;
- call r := g.N(k);
+ r := g.N(k);
assert r == s;
- call r := h.N(k);
+ r := h.N(k);
assert r == s;
g := null;
- call r := g.N(k);
+ r := g.N(k);
assert r == s;
-// call r := Global.N(r);
+// r := Global.N(r);
if (k == 0) {
assert r == s;
} else {
diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy index 8629a418..d53fb6a5 100644 --- a/Test/dafny0/Comprehensions.dfy +++ b/Test/dafny0/Comprehensions.dfy @@ -16,14 +16,14 @@ function method Id(x: int): int { x } // for triggering method Main()
{
var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;
- call PrintSet(q);
+ PrintSet(q);
q := set b: bool | true :: if b then 3 else 7;
- call PrintSet(q);
+ PrintSet(q);
var m := set k | k in q :: 2*k;
- call PrintSet(m);
- call PrintSet(set k | k in q && k % 2 == 0);
+ PrintSet(m);
+ PrintSet(set k | k in q && k % 2 == 0);
var sq := [30, 40, 20];
- call PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
+ PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;
}
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 59052ac2..01e14585 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -38,17 +38,17 @@ module J imports G, M { module X2 imports X1 {
class MyClass2 {
method Down(x1: MyClass1, x0: MyClass0) {
- call x1.Down(x0);
+ x1.Down(x0);
}
method WayDown(x0: MyClass0, g: ClassG) {
- call x0.Down();
- call g.T(); // allowed, because this follows import relation
+ x0.Down();
+ g.T(); // allowed, because this follows import relation
var t := g.TFunc(); // allowed, because this follows import relation
}
method Up() {
}
method Somewhere(y: MyClassY) {
- call y.M(); // error: does not follow import relation
+ y.M(); // error: does not follow import relation
}
}
}
@@ -56,10 +56,10 @@ module X2 imports X1 { module X1 imports X0 {
class MyClass1 {
method Down(x0: MyClass0) {
- call x0.Down();
+ x0.Down();
}
method Up(x2: MyClass2) {
- call x2.Up(); // error: does not follow import relation
+ x2.Up(); // error: does not follow import relation
}
}
}
@@ -69,7 +69,7 @@ module X0 { method Down() {
}
method Up(x1: MyClass1, x2: MyClass2) {
- call x1.Up(x2); // error: does not follow import relation
+ x1.Up(x2); // error: does not follow import relation
}
}
}
@@ -78,7 +78,7 @@ module YY { class MyClassY {
method M() { }
method P(g: ClassG) {
- call g.T(); // allowed, because this follows import relation
+ g.T(); // allowed, because this follows import relation
var t := g.TFunc(); // allowed, because this follows import relation
}
}
@@ -88,20 +88,20 @@ class ClassG { method T() { }
function method TFunc(): int { 10 }
method V(y: MyClassY) {
- call y.M(); // error: does not follow import relation
+ y.M(); // error: does not follow import relation
}
}
method Ping() {
- call Pong(); // allowed: intra-module call
+ Pong(); // allowed: intra-module call
}
method Pong() {
- call Ping(); // allowed: intra-module call
+ Ping(); // allowed: intra-module call
}
method ProcG(g: ClassG) {
- call g.T(); // allowed: intra-module call
+ g.T(); // allowed: intra-module call
var t := g.TFunc(); // allowed: intra-module call
}
@@ -111,11 +111,11 @@ class Ghosty { method Caller() {
var x := 3;
ghost var y := 3;
- call Callee(x, y); // fine
- call Callee(x, x); // fine
- call Callee(y, x); // error: cannot pass in ghost to a physical formal
- call Theorem(x); // fine
- call Theorem(y); // fine, because it's a ghost method
+ Callee(x, y); // fine
+ Callee(x, x); // fine
+ Callee(y, x); // error: cannot pass in ghost to a physical formal
+ Theorem(x); // fine
+ Theorem(y); // fine, because it's a ghost method
}
method Callee(a: int, ghost b: int) { }
ghost method Theorem(a: int) { }
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index cfefa7fa..ff84b84b 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -37,7 +37,7 @@ method Proc0(x: int) decreases x;
{
if (0 <= x) {
- call Proc1(x - 1);
+ Proc1(x - 1);
}
}
@@ -45,18 +45,18 @@ method Proc1(x: int) decreases x;
{
if (0 <= x) {
- call Proc0(x - 1);
+ Proc0(x - 1);
}
}
method Botch0(x: int)
decreases x;
{
- call Botch1(x - 1); // error: failure to keep termination metric bounded
+ Botch1(x - 1); // error: failure to keep termination metric bounded
}
method Botch1(x: int)
decreases x;
{
- call Botch0(x); // error: failure to decrease termination metric
+ Botch0(x); // error: failure to decrease termination metric
}
diff --git a/Test/dafny0/MultiDimArray.dfy b/Test/dafny0/MultiDimArray.dfy index ba5dc9da..ff30ef8a 100644 --- a/Test/dafny0/MultiDimArray.dfy +++ b/Test/dafny0/MultiDimArray.dfy @@ -74,7 +74,7 @@ class A { var s := z[1,2,4]; // first three powers of 2 (tra-la-la)
var some: A;
f[i,j,k] := some;
- call M3(i-1, j, k);
+ M3(i-1, j, k);
assert s == z[1,2,4];
if (*) {
assert f[i,j,k] == some; // error: the recursive call may have modified any element in 'f'
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 161ac22f..e4d0cbe7 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -3,8 +3,8 @@ method M(n: nat) { }
method Main() {
- call M(25);
- call M(-25); // error: cannot pass -25 as a nat
+ M(25);
+ M(-25); // error: cannot pass -25 as a nat
}
var f: nat;
@@ -34,7 +34,7 @@ method CheckField(x: nat, y: int) method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
if (0 < i) {
var n: nat := 5;
- call j := Generic(i-1, n, -4);
+ var j := Generic(i-1, n, -4);
assert 0 <= j; // error: the result is an int, not a nat
var q := FenEric(n, -4);
assert 0 <= q; // error: the result is an int, not a nat
@@ -65,7 +65,7 @@ method MatchIt(list: List<object>) returns (k: nat) match (list) {
case Nil =>
case Cons(n, extra, tail) =>
- call w := MatchIt(tail);
+ var w := MatchIt(tail);
assert 0 <= w;
assert 0 <= n; // fine
assert 0 <= n - 10; // error: possible assertion failure
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index b33d4d54..56d7575f 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -47,10 +47,10 @@ method TestNameResolution0() { z := Global.F(2); // error: invocation of instance function requires an instance
z := G(2); // error: cannot resolve G
z := Global.G(2);
- call z := M(2); // error: cannot resolve M
-// call z := Global.M(2); // error: call to instance method requires an instance
- call z := N(1); // error: cannot resolve N
-// call z := Global.N(1);
+ z := M(2); // error: cannot resolve M
+ z := Global.M(2); // error: call to instance method requires an instance
+ z := N(1); // error: cannot resolve N
+ z := Global.N(1);
z := z(5); // error: using local as if it were a function
z := Global.z; // error: class Global does not have a member z
@@ -59,7 +59,7 @@ method TestNameResolution0() { z := Global.X; // this means the instance field X of the object stored in the local variable 'Global'
var gg: Global := null;
var y := gg.G(5);
- call y := gg.N(5);
+ y := gg.N(5);
}
datatype Abc = Abel | Benny | Cecilia(y: int) | David(x: int) | Eleanor;
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index 930c4253..e1416094 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -20,10 +20,10 @@ class MyClass<T,U> { } else {
this.x := x + 0;
}
- call t, u, v := M(true, lotsaObjects);
+ t, u, v := M(true, lotsaObjects);
var to: MyClass<T,U>;
- call to, u, v := this.M(true, lotsaObjects);
- call to, u, v := to.M(true, lotsaObjects);
+ to, u, v := this.M(true, lotsaObjects);
+ to, u, v := to.M(true, lotsaObjects);
assert v[x] != null ==> null !in v[2..x][1..][5 := v[this.x]][..10];
}
}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 3359cff1..fcc764aa 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -109,11 +109,11 @@ class Modifies { method B(p: Modifies)
modifies this;
{
- call A(this);
+ A(this);
if (p == this) {
- call p.A(p);
+ p.A(p);
}
- call A(p); // error: may violate modifies clause
+ A(p); // error: may violate modifies clause
}
method C(b: bool)
@@ -126,9 +126,9 @@ class Modifies { requires p != null;
{
if (y == 3) {
- call p.C(true); // error: may violate modifies clause
+ p.C(true); // error: may violate modifies clause
} else {
- call p.C(false); // error: may violation modifies clause (the check is done without regard
+ p.C(false); // error: may violation modifies clause (the check is done without regard
// for the postcondition, which also makes sense, since there may, in
// principle, be other fields of the object that are not constrained by the
// postcondition)
@@ -138,7 +138,7 @@ class Modifies { method E()
modifies this;
{
- call A(null); // allowed
+ A(null); // allowed
}
method F(s: set<Modifies>)
@@ -164,7 +164,7 @@ class Modifies { foreach (m in s) {
m.x := m.x + 1;
}
- call F(s);
+ F(s);
}
foreach (m in s) {
assert m.x < m.x + 10; // nothing wrong with asserting something
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 5d411eb3..155fbaef 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -28,8 +28,8 @@ class Termination { }
method Lex() {
- call x := Update();
- call y := Update();
+ var x := Update();
+ var y := Update();
while (!(x == 0 && y == 0))
invariant 0 <= x && 0 <= y;
decreases x, y;
@@ -38,7 +38,7 @@ class Termination { y := y - 1;
} else {
x := x - 1;
- call y := Update();
+ y := Update();
}
}
}
@@ -82,7 +82,8 @@ class Termination { while (l != List.Nil)
decreases l;
{
- call x, l := Traverse(l);
+ var x;
+ x, l := Traverse(l);
}
}
@@ -204,7 +205,7 @@ method OuterOld(a: int) decreases a, true;
{
count := count + 1;
- call InnerOld(a, count);
+ InnerOld(a, count);
}
method InnerOld(a: int, b: int)
@@ -213,9 +214,9 @@ method InnerOld(a: int, b: int) {
count := count + 1;
if (b == 0 && 1 <= a) {
- call OuterOld(a - 1);
+ OuterOld(a - 1);
} else if (1 <= b) {
- call InnerOld(a, b - 1);
+ InnerOld(a, b - 1);
}
}
@@ -225,7 +226,7 @@ method Outer(a: int) modifies this;
{
count := count + 1;
- call Inner(a, count);
+ Inner(a, count);
}
method Inner(a: int, b: int)
@@ -233,9 +234,9 @@ method Inner(a: int, b: int) {
count := count + 1;
if (b == 0 && 1 <= a) {
- call Outer(a - 1);
+ Outer(a - 1);
} else if (1 <= b) {
- call Inner(a, b - 1);
+ Inner(a, b - 1);
}
}
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index a932eccf..38050b88 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -35,7 +35,7 @@ method BadLemma(c0: Color, c1: Color) }
method Main() {
- call BadLemma(Color.Yellow, Color.Blue);
+ BadLemma(Color.Yellow, Color.Blue);
assert false; // this shows how things can really go wrong if BadLemma verified successfully
}
@@ -68,7 +68,7 @@ method M(list: List, S: set<MyClass>) returns (ret: int) assert false; // error
}
}
- call k := N();
+ var k := N();
assert k.H() == 5;
ghost var l := NF();
assert l != null ==> l.H() == 5;
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index a044341e..a3698dc0 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -13,7 +13,7 @@ class C<U> { method Main(u: U)
{
var t := F(3,u) && F(this,u);
- call kz := M(t,u);
+ var kz := M(t,u);
assert kz && (G() || !G());
}
@@ -30,14 +30,14 @@ class SetTest { method Good()
{
var s := {2, 5, 3};
- call t := Add(s, 7);
+ var t := Add(s, 7);
assert {5,7,2,3} == t;
}
method Bad()
{
var s := {2, 50, 3};
- call t := Add(s, 7);
+ var t := Add(s, 7);
assert {5,7,2,3} == t; // error
}
}
@@ -52,14 +52,14 @@ class SequenceTest { method Good()
{
var s := [2, 5, 3];
- call t := Add(s, 7);
+ var t := Add(s, 7);
assert [2,5,3,7] == t;
}
method Bad()
{
var s := [2, 5, 3];
- call t := Add(s, 7);
+ var t := Add(s, 7);
assert [2,5,7,3] == t || [2,5,3] == t; // error
}
}
@@ -92,7 +92,7 @@ class CClient { }
c.x := 5;
c.x := c.x;
- call z := c.M(c, 17);
+ var z := c.M(c, 17);
assert z == c.x;
}
}
@@ -170,7 +170,7 @@ method TyKn_Main(k0: TyKn_K) { assert c.x != null ==> c.x.F() == 176; // the Dafny encoding needs the canCall mechanism to verify this
assert c.G() != null ==> c.G().F() == 176; // ditto
- call k2 := c.M();
+ var k2 := c.M();
assert k2 != null ==> k2.F() == 176; // the canCall mechanism does the trick here, but so does the encoding
// via k2's where clause
}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 7deeb0a1..21f0dda8 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -8,8 +8,8 @@ class C { method Caller()
{
- call m,n := M(true); // error on in-parameter
- call n,m := M(m); // 2 errors on out-parameters
+ var m,n := M(true); // error on in-parameter
+ n,m := M(m); // 2 errors on out-parameters
}
}
diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy index b4980d4b..88b06605 100644 --- a/Test/dafny1/BinaryTree.dfy +++ b/Test/dafny1/BinaryTree.dfy @@ -32,7 +32,7 @@ class IntSet { if (root == null) {
present := false;
} else {
- call present := root.Find(x);
+ present := root.Find(x);
}
}
@@ -42,7 +42,7 @@ class IntSet { ensures Valid() && fresh(Repr - old(Repr));
ensures Contents == old(Contents) + {x};
{
- call t := InsertHelper(x, root);
+ var t := InsertHelper(x, root);
root := t;
Contents := root.Contents;
Repr := root.Repr + {this};
@@ -64,12 +64,12 @@ class IntSet { } else {
if (x < n.data) {
assert n.right == null || n.right.Valid();
- call t := InsertHelper(x, n.left);
+ var t := InsertHelper(x, n.left);
n.left := t;
n.Repr := n.Repr + n.left.Repr;
} else {
assert n.left == null || n.left.Valid();
- call t := InsertHelper(x, n.right);
+ var t := InsertHelper(x, n.right);
n.right := t;
n.Repr := n.Repr + n.right.Repr;
}
@@ -85,7 +85,7 @@ class IntSet { ensures Contents == old(Contents) - {x};
{
if (root != null) {
- call newRoot := root.Remove(x);
+ var newRoot := root.Remove(x);
root := newRoot;
if (root == null) {
Contents := {};
@@ -152,9 +152,9 @@ class Node { if (x == data) {
present := true;
} else if (left != null && x < data) {
- call present := left.Find(x);
+ present := left.Find(x);
} else if (right != null && data < x) {
- call present := right.Find(x);
+ present := right.Find(x);
} else {
present := false;
}
@@ -171,12 +171,12 @@ class Node { {
node := this;
if (left != null && x < data) {
- call t := left.Remove(x);
+ var t := left.Remove(x);
left := t;
Contents := Contents - {x};
if (left != null) { Repr := Repr + left.Repr; }
} else if (right != null && data < x) {
- call t := right.Remove(x);
+ var t := right.Remove(x);
right := t;
Contents := Contents - {x};
if (right != null) { Repr := Repr + right.Repr; }
@@ -189,7 +189,7 @@ class Node { node := left;
} else {
// rotate
- call min, r := right.RemoveMin();
+ var min, r := right.RemoveMin();
data := min; right := r;
Contents := Contents - {x};
if (right != null) { Repr := Repr + right.Repr; }
@@ -211,7 +211,8 @@ class Node { min := data;
node := right;
} else {
- call min, t := left.RemoveMin();
+ var t;
+ min, t := left.RemoveMin();
left := t;
node := this;
Contents := Contents - {min};
@@ -225,9 +226,9 @@ class Main { {
var s := new IntSet.Init();
- call s.Insert(12);
- call s.Insert(24);
- call present := s.Find(x);
+ s.Insert(12);
+ s.Insert(24);
+ var present := s.Find(x);
assert present <==> x == 12 || x == 24;
}
@@ -235,8 +236,8 @@ class Main { requires s != null && s.Valid();
modifies s.Repr;
{
- call s.Insert(x);
- call s.Insert(24);
+ s.Insert(x);
+ s.Insert(24);
assert old(s.Contents) - {x,24} == s.Contents - {x,24};
}
}
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index 089a72c4..2dc49cd9 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -57,7 +57,7 @@ class ExtensibleArray<T> { if (M <= i) {
t := elements[i - M];
} else {
- call arr := more.Get(i / 256);
+ var arr := more.Get(i / 256);
t := arr[i % 256];
}
}
@@ -72,7 +72,7 @@ class ExtensibleArray<T> { if (M <= i) {
elements[i - M] := t;
} else {
- call arr := more.Get(i / 256);
+ var arr := more.Get(i / 256);
arr[i % 256] := t;
}
Contents := Contents[i := t];
@@ -94,7 +94,7 @@ class ExtensibleArray<T> { Repr := Repr + {more} + more.Repr;
}
// "elements" is full, so move it into "more" and allocate a new array
- call more.Append(elements);
+ more.Append(elements);
Repr := Repr + more.Repr;
M := M + 256;
elements := new T[256];
@@ -113,14 +113,14 @@ method Main() { invariant a.Valid() && fresh(a.Repr);
invariant |a.Contents| == n;
{
- call a.Append(n);
+ a.Append(n);
n := n + 1;
}
- call k := a.Get(570); print k, "\n";
- call k := a.Get(0); print k, "\n";
- call k := a.Get(1000); print k, "\n";
- call a.Set(1000, 23);
- call k := a.Get(0); print k, "\n";
- call k := a.Get(1000); print k, "\n";
- call k := a.Get(66000); print k, "\n";
+ var k := a.Get(570); print k, "\n";
+ k := a.Get(0); print k, "\n";
+ k := a.Get(1000); print k, "\n";
+ a.Set(1000, 23);
+ k := a.Get(0); print k, "\n";
+ k := a.Get(1000); print k, "\n";
+ k := a.Get(66000); print k, "\n";
}
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy index cff8b934..76e67205 100644 --- a/Test/dafny1/FindZero.dfy +++ b/Test/dafny1/FindZero.dfy @@ -9,7 +9,7 @@ method FindZero(a: array<int>) returns (r: int) invariant forall i :: 0 <= i && i < n && i < a.Length ==> a[i] != 0;
{
if (a[n] == 0) { r := n; return; }
- call Lemma(a, n, a[n]);
+ Lemma(a, n, a[n]);
n := n + a[n];
}
r := -1;
@@ -25,6 +25,6 @@ ghost method Lemma(a: array<int>, k: int, m: int) {
if (0 < m && k < a.Length) {
assert a[k] != 0;
- call Lemma(a, k+1, m-1);
+ Lemma(a, k+1, m-1);
}
}
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index 0e4c58e0..2c90769b 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -24,8 +24,8 @@ class IntegerInduction { ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
{
if (n != 0) {
- call Theorem0(n-1);
- call Lemma(n-1);
+ Theorem0(n-1);
+ Lemma(n-1);
}
}
@@ -33,7 +33,7 @@ class IntegerInduction { requires 0 <= n;
ensures 2 * Gauss(n) == n*(n+1);
{
- if (n != 0) { call Lemma(n-1); }
+ if (n != 0) { Lemma(n-1); }
}
// Here is another proof. It states the lemma as part of the theorem, and
@@ -45,7 +45,7 @@ class IntegerInduction { ensures 2 * Gauss(n) == n*(n+1);
{
if (n != 0) {
- call Theorem1(n-1);
+ Theorem1(n-1);
}
}
@@ -64,7 +64,7 @@ class IntegerInduction { ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
{
if (n != 0) {
- call Theorem2(n-1);
+ Theorem2(n-1);
assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));
}
@@ -84,7 +84,7 @@ class IntegerInduction { ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
{
if (n != 0) {
- call Theorem3(n-1);
+ Theorem3(n-1);
}
}
@@ -112,7 +112,7 @@ class IntegerInduction { if (*) {
assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));
} else {
- call Theorem4();
+ Theorem4();
}
}
diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy index 86ad451d..81b3f4c9 100644 --- a/Test/dafny1/MatrixFun.dfy +++ b/Test/dafny1/MatrixFun.dfy @@ -64,20 +64,20 @@ method Main() B[0,0] := true; B[0,1] := false; B[0,2] := false; B[0,3] := true; B[0,4] := false;
B[1,0] := true; B[1,1] := true; B[1,2] := true; B[1,3] := true; B[1,4] := false;
print "Before:\n";
- call PrintMatrix(B);
- call MirrorImage(B);
+ PrintMatrix(B);
+ MirrorImage(B);
print "Mirror image:\n";
- call PrintMatrix(B);
+ PrintMatrix(B);
var A := new int[3,3];
A[0,0] := 5; A[0,1] := 7; A[0,2] := 9;
A[1,0] := 6; A[1,1] := 2; A[1,2] := 3;
A[2,0] := 7; A[2,1] := 1; A[2,2] := 0;
print "Before:\n";
- call PrintMatrix(A);
- call Flip(A);
+ PrintMatrix(A);
+ Flip(A);
print "Flip:\n";
- call PrintMatrix(A);
+ PrintMatrix(A);
}
method PrintMatrix<T>(m: array2<T>)
diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy index db1c60fa..6e19ab8f 100644 --- a/Test/dafny1/PriorityQueue.dfy +++ b/Test/dafny1/PriorityQueue.dfy @@ -41,7 +41,7 @@ class PriorityQueue { {
n := n + 1;
a[n] := x;
- call SiftUp(n);
+ SiftUp(n);
}
method SiftUp(k: int)
@@ -76,7 +76,7 @@ class PriorityQueue { x := a[1];
a[1] := a[n];
n := n - 1;
- call SiftDown(1);
+ SiftDown(1);
}
method SiftDown(k: int)
@@ -156,7 +156,7 @@ class PriorityQueue_Alternative { {
n := n + 1;
a[n] := x;
- call SiftUp();
+ SiftUp();
}
method SiftUp()
@@ -189,7 +189,7 @@ class PriorityQueue_Alternative { x := a[1];
a[1] := a[n];
n := n - 1;
- call SiftDown();
+ SiftDown();
}
method SiftDown()
diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy index 0ee953e1..bfb588be 100644 --- a/Test/dafny1/Queue.dfy +++ b/Test/dafny1/Queue.dfy @@ -48,9 +48,9 @@ class Queue<T> { ensures Valid() && fresh(footprint - old(footprint));
ensures contents == old(contents)[1..] + old(contents)[..1];
{
- call t := Front();
- call Dequeue();
- call Enqueue(t);
+ var t := Front();
+ Dequeue();
+ Enqueue(t);
}
method RotateAny()
@@ -62,9 +62,9 @@ class Queue<T> { ensures (exists i :: 0 <= i && i <= |contents| &&
contents == old(contents)[i..] + old(contents)[..i]);
{
- call t := Front();
- call Dequeue();
- call Enqueue(t);
+ var t := Front();
+ Dequeue();
+ Enqueue(t);
}
method IsEmpty() returns (isEmpty: bool)
@@ -152,18 +152,18 @@ class Main<U> { var q0 := new Queue<T>.Init();
var q1 := new Queue<T>.Init();
- call q0.Enqueue(t);
- call q0.Enqueue(u);
+ q0.Enqueue(t);
+ q0.Enqueue(u);
- call q1.Enqueue(v);
+ q1.Enqueue(v);
assert |q0.contents| == 2;
- call w := q0.Front();
+ var w := q0.Front();
assert w == t;
- call q0.Dequeue();
+ q0.Dequeue();
- call w := q0.Front();
+ w := q0.Front();
assert w == u;
assert |q0.contents| == 1;
@@ -179,18 +179,18 @@ class Main<U> { ensures fresh(q0.footprint - old(q0.footprint));
ensures fresh(q1.footprint - old(q1.footprint));
{
- call q0.Enqueue(t);
- call q0.Enqueue(u);
+ q0.Enqueue(t);
+ q0.Enqueue(u);
- call q1.Enqueue(v);
+ q1.Enqueue(v);
assert |q0.contents| == 2;
- call w := q0.Front();
+ var w := q0.Front();
assert w == t;
- call q0.Dequeue();
+ q0.Dequeue();
- call w := q0.Front();
+ w := q0.Front();
assert w == u;
assert |q0.contents| == 1;
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index 33442219..95cdab89 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -26,7 +26,7 @@ class Main { n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
{
- call RecursiveMarkWorker(root, S, {});
+ RecursiveMarkWorker(root, S, {});
}
method RecursiveMarkWorker(root: Node, ghost S: set<Node>, ghost stackNodes: set<Node>)
@@ -67,7 +67,7 @@ class Main { {
var c := root.children[i];
if (c != null) {
- call RecursiveMarkWorker(c, S, stackNodes + {root});
+ RecursiveMarkWorker(c, S, stackNodes + {root});
}
i := i + 1;
}
diff --git a/Test/dafny1/SeparationLogicList.dfy b/Test/dafny1/SeparationLogicList.dfy index 7828a54e..56a64bd6 100644 --- a/Test/dafny1/SeparationLogicList.dfy +++ b/Test/dafny1/SeparationLogicList.dfy @@ -28,7 +28,7 @@ class Node<T> { l.next := null;
S := {l};
} else {
- call l, S := Cons(x, null, [], {});
+ l, S := Cons(x, null, [], {});
}
}
@@ -75,7 +75,7 @@ class ListNode<T> { l.Repr := {l};
l.Contents := [x];
} else {
- call l := Cons(x, null);
+ l := Cons(x, null);
}
}
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index 5cee5f6a..d3e0e82e 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -31,7 +31,7 @@ static ghost method Theorem(e: Expr, v: int, val: int) case Const(c) =>
case Var(x) =>
case Nary(op, args) =>
- call Lemma(args, v, val);
+ Lemma(args, v, val);
}
}
@@ -41,8 +41,8 @@ static ghost method Lemma(l: List, v: int, val: int) match l {
case Nil =>
case Cons(e, tail) =>
- call Theorem(e, v, val);
- call Lemma(tail, v, val);
+ Theorem(e, v, val);
+ Lemma(tail, v, val);
}
}
@@ -80,11 +80,11 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) case Var(x) =>
case Nary(op, args) =>
ghost var seArgs := SubstSeq(e, args, v, val);
- call LemmaSeq(e, args, v, val);
+ LemmaSeq(e, args, v, val);
ghost var se := Substitute(e, v, val);
ghost var seArgs2 := SubstSeq(se, seArgs, v, val);
- call LemmaSeq(se, seArgs, v, val);
+ LemmaSeq(se, seArgs, v, val);
var N := |args|;
var j := 0;
@@ -92,7 +92,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) invariant j <= N;
invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);
{
- call TheoremSeq(args[j], v, val);
+ TheoremSeq(args[j], v, val);
j := j + 1;
}
assert seArgs == seArgs2;
@@ -107,6 +107,6 @@ static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>, {
if (q == []) {
} else {
- call LemmaSeq(parent, q[..|q|-1], v, val);
+ LemmaSeq(parent, q[..|q|-1], v, val);
}
}
diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy index 2fecaee5..7ed7ce9b 100644 --- a/Test/dafny1/SumOfCubes.dfy +++ b/Test/dafny1/SumOfCubes.dfy @@ -10,19 +10,19 @@ class SumOfCubes { requires 0 <= n && n <= m;
ensures r == SumEmUp(n, m);
{
- call a := SocuFromZero(m);
- call b := SocuFromZero(n);
+ var a := SocuFromZero(m);
+ var b := SocuFromZero(n);
r := a - b;
- call Lemma0(n, m);
+ Lemma0(n, m);
}
static method SocuFromZero(k: int) returns (r: int)
requires 0 <= k;
ensures r == SumEmUp(0, k);
{
- call g := Gauss(k);
+ var g := Gauss(k);
r := g * g;
- call Lemma1(k);
+ Lemma1(k);
}
ghost static method Lemma0(n: int, m: int)
@@ -36,9 +36,9 @@ class SumOfCubes { {
k := k + 1;
}
- call Lemma3(0, n);
- call Lemma3(n, k);
- call Lemma3(0, k);
+ Lemma3(0, n);
+ Lemma3(n, k);
+ Lemma3(0, k);
}
static function GSum(k: int): int
@@ -52,7 +52,7 @@ class SumOfCubes { ensures r == GSum(k);
{
r := k * (k - 1) / 2;
- call Lemma2(k);
+ Lemma2(k);
}
ghost static method Lemma1(k: int)
@@ -64,10 +64,10 @@ class SumOfCubes { invariant i <= k;
invariant SumEmDown(0, i) == GSum(i) * GSum(i);
{
- call Lemma2(i);
+ Lemma2(i);
i := i + 1;
}
- call Lemma3(0, k);
+ Lemma3(0, k);
}
ghost static method Lemma2(k: int)
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy index 49f5a075..0aa36a10 100644 --- a/Test/dafny1/TerminationDemos.dfy +++ b/Test/dafny1/TerminationDemos.dfy @@ -58,10 +58,10 @@ class Ackermann { if (m == 0) {
r := n + 1;
} else if (n == 0) {
- call r := ComputeAck(m - 1, 1);
+ r := ComputeAck(m - 1, 1);
} else {
- call s := ComputeAck(m, n - 1);
- call r := ComputeAck(m - 1, s);
+ var s := ComputeAck(m, n - 1);
+ r := ComputeAck(m - 1, s);
}
}
}
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index 61e86836..189ff2b5 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -22,9 +22,9 @@ class UltraFilter<G> { {
if (M !in f) {
// instantiate 'g' with the following 'h'
- call h := H(f, S, M);
- call Lemma_HIsFilter(h, f, S, M);
- call Lemma_FHOrdering0(h, f, S, M);
+ var h := H(f, S, M);
+ Lemma_HIsFilter(h, f, S, M);
+ Lemma_FHOrdering0(h, f, S, M);
}
}
@@ -44,9 +44,9 @@ class UltraFilter<G> { // call Lemma_H1(h, f, S, M, *, *);
assume (forall C, D :: C in h && D in h ==> C * D in h);
- call Lemma_H2(h, f, S, M);
+ Lemma_H2(h, f, S, M);
- call Lemma_H3(h, f, S, M);
+ Lemma_H3(h, f, S, M);
}
method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)
diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy index 52cddaac..c7e4bc63 100644 --- a/Test/dafny1/pow2.dfy +++ b/Test/dafny1/pow2.dfy @@ -36,7 +36,7 @@ ghost method Lemma(n: int) ensures pow2_slow(n) == Square(pow2_slow(n/2));
{
if (n != 0) {
- call Lemma(n-2);
+ Lemma(n-2);
}
}
@@ -46,9 +46,9 @@ ghost method Theorem(n: int) {
if (n == 0) {
} else if (IsEven(n)) {
- call Lemma(n);
- call Theorem(n/2);
+ Lemma(n);
+ Theorem(n/2);
} else {
- call Theorem(n-1);
+ Theorem(n-1);
}
}
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy index 95ad12fa..ed376931 100644 --- a/Test/vacid0/Composite.dfy +++ b/Test/vacid0/Composite.dfy @@ -44,7 +44,7 @@ class Composite { {
var delta := x - val;
val := x;
- call Adjust(delta, S, S);
+ Adjust(delta, S, S);
}
method Add(ghost S: set<Composite>, child: Composite, ghost U: set<Composite>)
@@ -73,7 +73,7 @@ class Composite { right := child;
}
child.parent := this;
- call Adjust(child.sum, S, S+U);
+ Adjust(child.sum, S, S+U);
}
method Dislodge(ghost S: set<Composite>)
@@ -97,7 +97,7 @@ class Composite { p.right := null;
}
var delta := -sum;
- call p.Adjust(delta, S - {this}, S);
+ p.Adjust(delta, S - {this}, S);
}
}
@@ -138,35 +138,35 @@ method Main() var c0 := new Composite.Init(57);
var c1 := new Composite.Init(12);
- call c0.Add({c0}, c1, {c1});
+ c0.Add({c0}, c1, {c1});
var c2 := new Composite.Init(48);
var c3 := new Composite.Init(48);
- call c2.Add({c2}, c3, {c3});
- call c0.Add({c0,c1}, c2, {c2,c3});
+ c2.Add({c2}, c3, {c3});
+ c0.Add({c0,c1}, c2, {c2,c3});
ghost var S := {c0, c1, c2, c3};
- call c1.Update(100, S);
- call c2.Update(102, S);
+ c1.Update(100, S);
+ c2.Update(102, S);
- call c2.Dislodge(S);
- call c2.Update(496, S);
- call c0.Update(0, S);
+ c2.Dislodge(S);
+ c2.Update(496, S);
+ c0.Update(0, S);
}
method Harness() {
var a := new Composite.Init(5);
var b := new Composite.Init(7);
- call a.Add({a}, b, {b});
+ a.Add({a}, b, {b});
assert a.sum == 12;
- call b.Update(17, {a,b});
+ b.Update(17, {a,b});
assert a.sum == 22;
var c := new Composite.Init(10);
- call b.Add({a,b}, c, {c});
- call b.Dislodge({a,b,c});
+ b.Add({a,b}, c, {c});
+ b.Dislodge({a,b,c});
assert b.sum == 27;
}
diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy index 2c217264..989ddfc6 100644 --- a/Test/vacid0/SparseArray.dfy +++ b/Test/vacid0/SparseArray.dfy @@ -37,11 +37,9 @@ class SparseArray<T> { ensures |Contents| == N && this.zero == zero;
ensures (forall x :: x in Contents ==> x == zero);
{
- var aa;
- var ii;
- call aa := AllocateArray(N); this.a := aa;
- call ii := AllocateArray(N); this.b := ii;
- call ii := AllocateArray(N); this.c := ii;
+ var aa := AllocateArray(N); this.a := aa;
+ var bb := AllocateArray(N); this.b := bb;
+ bb := AllocateArray(N); this.c := bb;
this.n := 0;
// initialize ghost variable Contents to a sequence of length N containing only zero's,
|