diff options
| -rw-r--r-- | Dafny/Compiler.cs | 108 | ||||
| -rw-r--r-- | Dafny/Dafny.atg | 25 | ||||
| -rw-r--r-- | Dafny/DafnyAst.cs | 13 | ||||
| -rw-r--r-- | Dafny/Parser.cs | 298 | ||||
| -rw-r--r-- | Dafny/Printer.cs | 4 | ||||
| -rw-r--r-- | Dafny/Resolver.cs | 233 | ||||
| -rw-r--r-- | Dafny/Scanner.cs | 108 | ||||
| -rw-r--r-- | Dafny/Translator.cs | 224 | ||||
| -rw-r--r-- | Test/VSComp2010/Problem5-DoubleEndedQueue.dfy | 18 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 3 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b5.dfy | 13 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b6.dfy | 6 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b8.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 12 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 40 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny1/BinaryTree.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny1/ExtensibleArray.dfy | 7 | ||||
| -rw-r--r-- | Test/dafny1/ListCopy.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny1/Queue.dfy | 13 | ||||
| -rw-r--r-- | Test/dafny1/UnboundedStack.dfy | 3 | ||||
| -rw-r--r-- | Test/vacid0/Composite.dfy | 18 |
22 files changed, 657 insertions, 515 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index bd6f9240..62270067 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -662,13 +662,27 @@ namespace Microsoft.Dafny { wr.WriteLine(";");
} else {
- Indent(indent);
- TrExpr(s.Lhs);
- if (!(s.Rhs is HavocRhs)) {
+ var tRhs = s.Rhs as TypeRhs;
+ if (tRhs != null && tRhs.InitCall != null) {
+ string nw = "_nw" + tmpVarCount;
+ tmpVarCount++;
+ Indent(indent);
+ wr.Write("{0} = ", nw);
+ TrAssignmentRhs(s.Rhs);
+ wr.WriteLine(";");
+ Indent(indent);
+ TrCallStmt(tRhs.InitCall, nw, indent);
+ wr.WriteLine(";");
+ Indent(indent);
+ TrExpr(s.Lhs);
+ wr.WriteLine(" = {0};", nw);
+ } else if (!(s.Rhs is HavocRhs)) {
+ Indent(indent);
+ TrExpr(s.Lhs);
wr.Write(" = ");
TrAssignmentRhs(s.Rhs);
+ wr.WriteLine(";");
}
- wr.WriteLine(";");
}
} else if (stmt is VarDecl) {
@@ -676,39 +690,7 @@ namespace Microsoft.Dafny { } else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
-
- foreach (VarDecl local in s.NewVars) {
- TrVarDecl(local, false, indent);
- }
-
- Contract.Assert(s.Method != null); // follows from the fact that stmt has been successfully resolved
- Indent(indent);
- if (s.Method.IsStatic) {
- wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
- } else {
- TrParenExpr(s.Receiver);
- }
- wr.Write(".{0}(", s.Method.Name);
-
- string sep = "";
- for (int i = 0; i < s.Method.Ins.Count; i++) {
- Formal p = s.Method.Ins[i];
- if (!p.IsGhost) {
- wr.Write(sep);
- TrExpr(s.Args[i]);
- sep = ", ";
- }
- }
- for (int i = 0; i < s.Method.Outs.Count; i++) {
- Formal p = s.Method.Outs[i];
- if (!p.IsGhost) {
- wr.Write("{0}out ", sep);
- TrExpr(s.Lhs[i]);
- sep = ", ";
- }
- }
-
- wr.WriteLine(");");
+ TrCallStmt(s, null, indent);
} else if (stmt is BlockStmt) {
Indent(indent); wr.WriteLine("{");
@@ -830,10 +812,50 @@ namespace Microsoft.Dafny { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
}
+
+ void TrCallStmt(CallStmt s, string receiverReplacement, int indent) {
+ Contract.Requires(s != null);
+
+ foreach (VarDecl local in s.NewVars) {
+ TrVarDecl(local, false, indent);
+ }
+
+ Contract.Assert(s.Method != null); // follows from the fact that stmt has been successfully resolved
+ Indent(indent);
+ if (receiverReplacement != null) {
+ wr.Write(receiverReplacement);
+ } else if (s.Method.IsStatic) {
+ wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
+ } else {
+ TrParenExpr(s.Receiver);
+ }
+ wr.Write(".{0}(", s.Method.Name);
+
+ string sep = "";
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ wr.Write(sep);
+ TrExpr(s.Args[i]);
+ sep = ", ";
+ }
+ }
+ for (int i = 0; i < s.Method.Outs.Count; i++) {
+ Formal p = s.Method.Outs[i];
+ if (!p.IsGhost) {
+ wr.Write("{0}out ", sep);
+ TrExpr(s.Lhs[i]);
+ sep = ", ";
+ }
+ }
+
+ wr.WriteLine(");");
+ }
int tmpVarCount = 0;
- void TrAssignmentRhs(AssignmentRhs rhs){Contract.Requires(rhs != null);
+ void TrAssignmentRhs(AssignmentRhs rhs) {
+ Contract.Requires(rhs != null);
Contract.Requires(!(rhs is HavocRhs));
if (rhs is ExprRhs) {
ExprRhs e = (ExprRhs)rhs;
@@ -904,11 +926,17 @@ namespace Microsoft.Dafny { if (s.Rhs != null) {
wr.Write(" = ");
TrAssignmentRhs(s.Rhs);
+ wr.WriteLine(";");
+ var tRhs = s.Rhs as TypeRhs;
+ if (tRhs != null && tRhs.InitCall != null) {
+ TrCallStmt(tRhs.InitCall, s.Name, indent);
+ }
} else if (alwaysInitialize) {
// produce a default value
- wr.Write(" = {0}", DefaultValue(s.Type));
+ wr.WriteLine(" = {0};", DefaultValue(s.Type));
+ } else {
+ wr.WriteLine(";");
}
- wr.WriteLine(";");
}
void MatchCasePrelude(string source, DatatypeCtor ctor, List<BoundVar/*!*/>/*!*/ arguments, int caseIndex, int caseCount, int indent) {
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index ce067ec6..2b330706 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -764,10 +764,12 @@ AssignStmt<out Statement/*!*/ s, bool allowChoose> List<Expression> rhs;
Type ty;
s = dummyStmt;
+ CallStmt initCall = null;
.)
LhsExpr<out lhs>
":=" (. x = t; .)
- AssignRhs<out rhs, out ty> (. if (ty == null) {
+ AssignRhs<out rhs, out ty, out initCall, lhs>
+ (. if (ty == null) {
Contract.Assert(rhs != null);
Contract.Assert(rhs.Count == 1);
s = new AssignStmt(x, lhs, rhs[0]);
@@ -778,7 +780,7 @@ AssignStmt<out Statement/*!*/ s, bool allowChoose> }
}
} else if (rhs == null) {
- s = new AssignStmt(x, lhs, ty);
+ s = new AssignStmt(x, lhs, ty, initCall);
} else {
s = new AssignStmt(x, lhs, ty, rhs);
}
@@ -786,20 +788,26 @@ AssignStmt<out Statement/*!*/ s, bool allowChoose> ";"
.
-AssignRhs<.out List<Expression> ee, out Type ty.>
+AssignRhs<.out List<Expression> ee, out Type ty, out CallStmt initCall, Expression receiverForInitCall.>
/* ensures ee != null || ty != null; */
/* ensures ee != null ==> 1 <= ee.Count; */
/* ensures ty == null ==> 1 == ee.Count; */
= (. IToken/*!*/ x; Expression/*!*/ e;
ee = null; ty = null;
+ initCall = null;
+ List<Expression> args;
.)
( "new" TypeAndToken<out x, out ty>
- [ "[" Expression<out e> (. ee = new List<Expression>(); ee.Add(e); .)
- { "," Expression<out e> (. ee.Add(e); .)
- }
+ [ "[" (. ee = new List<Expression>(); .)
+ Expressions<ee>
"]" (. // make sure an array class with this dimensionality exists
UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
.)
+ | "." Ident<out x>
+ "(" (. args = new List<Expression/*!*/>(); .)
+ [ Expressions<args> ]
+ ")" (. initCall = new CallStmt(x, new List<AutoVarDecl>(), new List<IdentifierExpr>(),
+ receiverForInitCall, x.val, args); .)
]
| "choose" (. x = t; .)
"(" Expression<out e> ")" (. e = new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e);
@@ -835,19 +843,20 @@ IdentTypeRhs<out VarDecl/*!*/ d, bool isGhost> = (. Contract.Ensures(Contract.ValueAtReturn(out d) != null); IToken/*!*/ id; Type/*!*/ ty;
List<Expression> rhs = null; Type newType = null;
Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
+ CallStmt initCall = null;
.)
Ident<out id>
[ ":" Type<out ty> (. optionalType = ty; .)
]
[ ":="
- AssignRhs<out rhs, out newType>
+ AssignRhs<out rhs, out newType, out initCall, new IdentifierExpr(id, id.val)>
]
(. if (newType == null && rhs != null) {
Contract.Assert(rhs.Count == 1);
optionalRhs = new ExprRhs(rhs[0]);
} else if (newType != null) {
if (rhs == null) {
- optionalRhs = new TypeRhs(newType);
+ optionalRhs = new TypeRhs(newType, initCall);
} else {
optionalRhs = new TypeRhs(newType, rhs);
}
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index f5542b4c..18895aa3 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -1316,17 +1316,24 @@ namespace Microsoft.Dafny { public class TypeRhs : DeterminedAssignmentRhs {
public readonly Type EType;
+ public readonly List<Expression> ArrayDimensions;
+ public readonly CallStmt InitCall; // may be null (and is definitely null for arrays)
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(EType != null);
Contract.Invariant(ArrayDimensions == null || 1 <= ArrayDimensions.Count);
+ Contract.Invariant(ArrayDimensions == null || InitCall == null);
}
- public readonly List<Expression> ArrayDimensions;
public TypeRhs(Type type) {
Contract.Requires(type != null);
EType = type;
}
+ public TypeRhs(Type type, CallStmt initCall) {
+ Contract.Requires(type != null);
+ EType = type;
+ InitCall = initCall;
+ }
public TypeRhs(Type type, List<Expression> arrayDimensions) {
Contract.Requires(type != null);
Contract.Requires(arrayDimensions != null && 1 <= arrayDimensions.Count);
@@ -1355,13 +1362,13 @@ namespace Microsoft.Dafny { this.Lhs = lhs;
this.Rhs = new ExprRhs(rhs);
}
- public AssignStmt(IToken tok, Expression lhs, Type type)
+ public AssignStmt(IToken tok, Expression lhs, Type type, CallStmt initCall)
: base(tok) { // alloc statement
Contract.Requires(tok != null);
Contract.Requires(lhs != null);
Contract.Requires(type != null);
this.Lhs = lhs;
- this.Rhs = new TypeRhs(type);
+ this.Rhs = new TypeRhs(type, initCall);
}
public AssignStmt(IToken tok, Expression lhs, Type type, List<Expression> arrayDimensions)
: base(tok) { // array alloc statement
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index 7cc48f3b..5c1e473b 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -634,13 +634,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; Expression/*!*/ e0; Expression/*!*/ e1 = dummyExpr;
e = dummyExpr;
- if (la.kind == 53) {
+ if (la.kind == 54) {
Get();
x = t;
Expression(out e);
- Expect(65);
+ Expect(66);
Expression(out e0);
- Expect(54);
+ Expect(55);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(8)) {
@@ -1016,19 +1016,19 @@ List<Expression/*!*/>/*!*/ decreases) { s = dummyStmt; /* to please the compiler */
switch (la.kind) {
- case 61: {
+ case 62: {
AssertStmt(out s);
break;
}
- case 62: {
+ case 63: {
AssumeStmt(out s);
break;
}
- case 63: {
+ case 64: {
UseStmt(out s);
break;
}
- case 64: {
+ case 65: {
PrintStmt(out s);
break;
}
@@ -1036,19 +1036,19 @@ List<Expression/*!*/>/*!*/ decreases) { AssignStmt(out s, true);
break;
}
- case 52: {
+ case 53: {
HavocStmt(out s);
break;
}
- case 57: {
+ case 58: {
CallStmt(out s);
break;
}
- case 53: {
+ case 54: {
IfStmt(out s);
break;
}
- case 55: {
+ case 56: {
WhileStmt(out s);
break;
}
@@ -1056,7 +1056,7 @@ List<Expression/*!*/>/*!*/ decreases) { MatchStmt(out s);
break;
}
- case 58: {
+ case 59: {
ForeachStmt(out s);
break;
}
@@ -1109,7 +1109,7 @@ List<Expression/*!*/>/*!*/ decreases) { void AssertStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(61);
+ Expect(62);
x = t;
Expression(out e);
Expect(15);
@@ -1118,7 +1118,7 @@ List<Expression/*!*/>/*!*/ decreases) { void AssumeStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(62);
+ Expect(63);
x = t;
Expression(out e);
Expect(15);
@@ -1127,7 +1127,7 @@ List<Expression/*!*/>/*!*/ decreases) { void UseStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(63);
+ Expect(64);
x = t;
Expression(out e);
Expect(15);
@@ -1138,7 +1138,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(64);
+ Expect(65);
x = t;
AttributeArg(out arg);
args.Add(arg);
@@ -1157,11 +1157,12 @@ List<Expression/*!*/>/*!*/ decreases) { List<Expression> rhs;
Type ty;
s = dummyStmt;
+ CallStmt initCall = null;
LhsExpr(out lhs);
Expect(47);
x = t;
- AssignRhs(out rhs, out ty);
+ AssignRhs(out rhs, out ty, out initCall, lhs);
if (ty == null) {
Contract.Assert(rhs != null);
Contract.Assert(rhs.Count == 1);
@@ -1173,7 +1174,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
}
} else if (rhs == null) {
- s = new AssignStmt(x, lhs, ty);
+ s = new AssignStmt(x, lhs, ty, initCall);
} else {
s = new AssignStmt(x, lhs, ty, rhs);
}
@@ -1183,7 +1184,7 @@ List<Expression/*!*/>/*!*/ decreases) { void HavocStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs;
- Expect(52);
+ Expect(53);
x = t;
LhsExpr(out lhs);
Expect(15);
@@ -1196,7 +1197,7 @@ List<Expression/*!*/>/*!*/ decreases) { List<IdentifierExpr/*!*/> lhs = new List<IdentifierExpr/*!*/>();
List<AutoVarDecl/*!*/> newVars = new List<AutoVarDecl/*!*/>();
- Expect(57);
+ Expect(58);
x = t;
CallStmtSubExpr(out e);
if (la.kind == 17 || la.kind == 47) {
@@ -1253,13 +1254,13 @@ List<Expression/*!*/>/*!*/ decreases) { Statement els = null;
IToken bodyStart, bodyEnd;
- Expect(53);
+ Expect(54);
x = t;
Guard(out guard);
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
- if (la.kind == 53) {
+ if (la.kind == 54) {
IfStmt(out s);
els = s;
} else if (la.kind == 7) {
@@ -1279,18 +1280,18 @@ List<Expression/*!*/>/*!*/ decreases) { Statement/*!*/ body;
IToken bodyStart, bodyEnd;
- Expect(55);
+ Expect(56);
x = t;
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
- while (la.kind == 26 || la.kind == 29 || la.kind == 56) {
- if (la.kind == 26 || la.kind == 56) {
+ while (la.kind == 26 || la.kind == 29 || la.kind == 57) {
+ if (la.kind == 26 || la.kind == 57) {
isFree = false;
if (la.kind == 26) {
Get();
isFree = true;
}
- Expect(56);
+ Expect(57);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(15);
@@ -1335,7 +1336,7 @@ List<Expression/*!*/>/*!*/ decreases) { AssignStmt bodyAssign = null;
parseVarScope.PushMarker();
- Expect(58);
+ Expect(59);
x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
@@ -1346,20 +1347,20 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
Type(out ty);
}
- Expect(59);
+ Expect(60);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (la.kind == 60) {
+ if (la.kind == 61) {
Get();
Expression(out range);
}
Expect(31);
Expect(7);
- while (la.kind == 61 || la.kind == 62 || la.kind == 63) {
- if (la.kind == 61) {
+ while (la.kind == 62 || la.kind == 63 || la.kind == 64) {
+ if (la.kind == 62) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (la.kind == 62) {
+ } else if (la.kind == 63) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1370,7 +1371,7 @@ List<Expression/*!*/>/*!*/ decreases) { if (StartOf(13)) {
AssignStmt(out s, false);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (la.kind == 52) {
+ } else if (la.kind == 53) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
} else SynErr(123);
@@ -1389,27 +1390,37 @@ List<Expression/*!*/>/*!*/ decreases) { SelectExpression(out e);
}
- void AssignRhs(out List<Expression> ee, out Type ty) {
+ void AssignRhs(out List<Expression> ee, out Type ty, out CallStmt initCall, Expression receiverForInitCall) {
IToken/*!*/ x; Expression/*!*/ e;
ee = null; ty = null;
+ initCall = null;
+ List<Expression> args;
if (la.kind == 48) {
Get();
TypeAndToken(out x, out ty);
- if (la.kind == 49) {
- Get();
- Expression(out e);
- ee = new List<Expression>(); ee.Add(e);
- while (la.kind == 17) {
+ if (la.kind == 49 || la.kind == 51) {
+ if (la.kind == 49) {
Get();
- Expression(out e);
- ee.Add(e);
+ ee = new List<Expression>();
+ Expressions(ee);
+ Expect(50);
+ UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
+
+ } else {
+ Get();
+ Ident(out x);
+ Expect(30);
+ args = new List<Expression/*!*/>();
+ if (StartOf(9)) {
+ Expressions(args);
+ }
+ Expect(31);
+ initCall = new CallStmt(x, new List<AutoVarDecl>(), new List<IdentifierExpr>(),
+ receiverForInitCall, x.val, args);
}
- Expect(50);
- UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
-
}
- } else if (la.kind == 51) {
+ } else if (la.kind == 52) {
Get();
x = t;
Expect(30);
@@ -1432,7 +1443,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 30 || la.kind == 97 || la.kind == 98) {
ObjectExpression(out e);
} else SynErr(125);
- while (la.kind == 49 || la.kind == 93) {
+ while (la.kind == 49 || la.kind == 51) {
SelectOrCallSuffix(ref e);
}
}
@@ -1441,6 +1452,7 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out d) != null); IToken/*!*/ id; Type/*!*/ ty;
List<Expression> rhs = null; Type newType = null;
Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
+ CallStmt initCall = null;
Ident(out id);
if (la.kind == 20) {
@@ -1450,14 +1462,14 @@ List<Expression/*!*/>/*!*/ decreases) { }
if (la.kind == 47) {
Get();
- AssignRhs(out rhs, out newType);
+ AssignRhs(out rhs, out newType, out initCall, new IdentifierExpr(id, id.val));
}
if (newType == null && rhs != null) {
Contract.Assert(rhs.Count == 1);
optionalRhs = new ExprRhs(rhs[0]);
} else if (newType != null) {
if (rhs == null) {
- optionalRhs = new TypeRhs(newType);
+ optionalRhs = new TypeRhs(newType, initCall);
} else {
optionalRhs = new TypeRhs(newType, rhs);
}
@@ -1521,7 +1533,7 @@ List<Expression/*!*/>/*!*/ decreases) { ObjectExpression(out e);
SelectOrCallSuffix(ref e);
} else SynErr(127);
- while (la.kind == 49 || la.kind == 93) {
+ while (la.kind == 49 || la.kind == 51) {
SelectOrCallSuffix(ref e);
}
}
@@ -1540,7 +1552,7 @@ List<Expression/*!*/>/*!*/ decreases) { void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 66 || la.kind == 67) {
+ while (la.kind == 67 || la.kind == 68) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1551,7 +1563,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 == 68 || la.kind == 69) {
+ if (la.kind == 69 || la.kind == 70) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1560,9 +1572,9 @@ List<Expression/*!*/>/*!*/ decreases) { }
void EquivOp() {
- if (la.kind == 66) {
+ if (la.kind == 67) {
Get();
- } else if (la.kind == 67) {
+ } else if (la.kind == 68) {
Get();
} else SynErr(129);
}
@@ -1571,12 +1583,12 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(14)) {
- if (la.kind == 70 || la.kind == 71) {
+ 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 == 70 || la.kind == 71) {
+ while (la.kind == 71 || la.kind == 72) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1587,7 +1599,7 @@ List<Expression/*!*/>/*!*/ decreases) { x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 72 || la.kind == 73) {
+ while (la.kind == 73 || la.kind == 74) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1598,9 +1610,9 @@ List<Expression/*!*/>/*!*/ decreases) { }
void ImpliesOp() {
- if (la.kind == 68) {
+ if (la.kind == 69) {
Get();
- } else if (la.kind == 69) {
+ } else if (la.kind == 70) {
Get();
} else SynErr(130);
}
@@ -1616,17 +1628,17 @@ List<Expression/*!*/>/*!*/ decreases) { }
void AndOp() {
- if (la.kind == 70) {
+ if (la.kind == 71) {
Get();
- } else if (la.kind == 71) {
+ } else if (la.kind == 72) {
Get();
} else SynErr(131);
}
void OrOp() {
- if (la.kind == 72) {
+ if (la.kind == 73) {
Get();
- } else if (la.kind == 73) {
+ } else if (la.kind == 74) {
Get();
} else SynErr(132);
}
@@ -1634,7 +1646,7 @@ List<Expression/*!*/>/*!*/ decreases) { 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 == 83 || la.kind == 84) {
+ while (la.kind == 84 || la.kind == 85) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1644,7 +1656,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 74: {
+ case 75: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
@@ -1659,47 +1671,47 @@ List<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 75: {
+ case 76: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 76: {
+ case 77: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 77: {
+ case 78: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 78: {
+ case 79: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 59: {
+ case 60: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 79: {
+ case 80: {
Get();
x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 80: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 81: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
@@ -1711,7 +1723,7 @@ List<Expression/*!*/>/*!*/ decreases) { 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 == 39 || la.kind == 85 || la.kind == 86) {
+ while (la.kind == 39 || la.kind == 86 || la.kind == 87) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1720,10 +1732,10 @@ 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 == 83) {
+ if (la.kind == 84) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 84) {
+ } else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
} else SynErr(134);
@@ -1731,12 +1743,12 @@ List<Expression/*!*/>/*!*/ decreases) { void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
- if (la.kind == 84) {
+ 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 == 87 || la.kind == 88) {
+ } else if (la.kind == 88 || la.kind == 89) {
NegOp();
x = t;
UnaryExpression(out e);
@@ -1753,19 +1765,19 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 39) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 85) {
+ } else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 86) {
+ } else if (la.kind == 87) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
} else SynErr(136);
}
void NegOp() {
- if (la.kind == 87) {
+ if (la.kind == 88) {
Get();
- } else if (la.kind == 88) {
+ } else if (la.kind == 89) {
Get();
} else SynErr(137);
}
@@ -1775,17 +1787,17 @@ List<Expression/*!*/>/*!*/ decreases) { e = dummyExpr;
switch (la.kind) {
- case 89: {
+ case 90: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 90: {
+ case 91: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 91: {
+ case 92: {
Get();
e = new LiteralExpr(t);
break;
@@ -1795,11 +1807,11 @@ List<Expression/*!*/>/*!*/ decreases) { e = new LiteralExpr(t, n);
break;
}
- case 92: {
+ case 93: {
Get();
x = t;
Ident(out dtName);
- Expect(93);
+ Expect(51);
Ident(out id);
elements = new List<Expression/*!*/>();
if (la.kind == 30) {
@@ -1830,12 +1842,12 @@ List<Expression/*!*/>/*!*/ decreases) { e = new AllocatedExpr(x, e);
break;
}
- case 60: {
+ case 61: {
Get();
x = t;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(60);
+ Expect(61);
break;
}
case 7: {
@@ -1924,7 +1936,7 @@ List<Expression/*!*/>/*!*/ decreases) { List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 93) {
+ if (la.kind == 51) {
Get();
Ident(out id);
if (la.kind == 30) {
@@ -2111,17 +2123,17 @@ List<Expression/*!*/>/*!*/ decreases) { {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
{x,x,x,x, x,x,x,T, 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,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, 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,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,T, x,T,T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,T, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, T,T,x,T, x,T,T,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,T, x,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,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, T,T,x,T, x,T,T,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,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,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,T,T,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,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,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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,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,T,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,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,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,T, x,T,T,x, x,x,x,x, x,x,x}
+ {x,T,T,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,T,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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x}
};
} // end Parser
@@ -2197,49 +2209,49 @@ public class Errors { case 48: s = "\"new\" expected"; break;
case 49: s = "\"[\" expected"; break;
case 50: s = "\"]\" expected"; break;
- case 51: s = "\"choose\" expected"; break;
- case 52: s = "\"havoc\" expected"; break;
- case 53: s = "\"if\" expected"; break;
- case 54: s = "\"else\" expected"; break;
- case 55: s = "\"while\" expected"; break;
- case 56: s = "\"invariant\" expected"; break;
- case 57: s = "\"call\" expected"; break;
- case 58: s = "\"foreach\" expected"; break;
- case 59: s = "\"in\" expected"; break;
- case 60: s = "\"|\" expected"; break;
- case 61: s = "\"assert\" expected"; break;
- case 62: s = "\"assume\" expected"; break;
- case 63: s = "\"use\" expected"; break;
- case 64: s = "\"print\" expected"; break;
- case 65: s = "\"then\" expected"; break;
- case 66: s = "\"<==>\" expected"; break;
- case 67: s = "\"\\u21d4\" expected"; break;
- case 68: s = "\"==>\" expected"; break;
- case 69: s = "\"\\u21d2\" expected"; break;
- case 70: s = "\"&&\" expected"; break;
- case 71: s = "\"\\u2227\" expected"; break;
- case 72: s = "\"||\" expected"; break;
- case 73: s = "\"\\u2228\" expected"; break;
- case 74: s = "\"==\" 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 = "\"!in\" expected"; break;
- case 80: s = "\"\\u2260\" expected"; break;
- case 81: s = "\"\\u2264\" expected"; break;
- case 82: s = "\"\\u2265\" expected"; break;
- case 83: s = "\"+\" 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 = "\"\\u00ac\" expected"; break;
- case 89: s = "\"false\" expected"; break;
- case 90: s = "\"true\" expected"; break;
- case 91: s = "\"null\" expected"; break;
- case 92: s = "\"#\" expected"; break;
- case 93: s = "\".\" expected"; break;
+ case 51: s = "\".\" expected"; break;
+ case 52: s = "\"choose\" expected"; break;
+ case 53: s = "\"havoc\" expected"; break;
+ case 54: s = "\"if\" expected"; break;
+ case 55: s = "\"else\" expected"; break;
+ case 56: s = "\"while\" expected"; break;
+ case 57: s = "\"invariant\" expected"; break;
+ case 58: s = "\"call\" expected"; break;
+ case 59: s = "\"foreach\" expected"; break;
+ case 60: s = "\"in\" expected"; break;
+ case 61: s = "\"|\" expected"; break;
+ case 62: s = "\"assert\" expected"; break;
+ case 63: s = "\"assume\" expected"; break;
+ case 64: s = "\"use\" expected"; break;
+ case 65: s = "\"print\" expected"; break;
+ case 66: s = "\"then\" 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 = "\"#\" expected"; break;
case 94: s = "\"fresh\" expected"; break;
case 95: s = "\"allocated\" expected"; break;
case 96: s = "\"..\" expected"; break;
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs index 629a0f89..6af086a5 100644 --- a/Dafny/Printer.cs +++ b/Dafny/Printer.cs @@ -590,6 +590,10 @@ namespace Microsoft.Dafny { s = ", ";
}
wr.Write("]");
+ } else if (t.InitCall != null) {
+ wr.Write(".{0}(", t.InitCall.MethodName);
+ PrintExpressionList(t.InitCall.Args);
+ wr.Write(")");
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 7344e058..92ae3ae2 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -1236,7 +1236,7 @@ namespace Microsoft.Dafny { }
} else if (s.Rhs is TypeRhs) {
TypeRhs rr = (TypeRhs)s.Rhs;
- Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost);
+ Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, method);
if (!UnifyTypes(s.Lhs.Type, t)) {
Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, s.Lhs.Type);
}
@@ -1261,7 +1261,7 @@ namespace Microsoft.Dafny { rhsType = rr.Expr.Type;
} else if (s.Rhs is TypeRhs) {
TypeRhs rr = (TypeRhs)s.Rhs;
- rhsType = ResolveTypeRhs(rr, stmt, s.IsGhost);
+ rhsType = ResolveTypeRhs(rr, stmt, s.IsGhost, method);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS
}
@@ -1282,109 +1282,7 @@ namespace Microsoft.Dafny { } else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
-
- // resolve receiver
- ResolveReceiver(s.Receiver, true, false);
- Contract.Assert(s.Receiver.Type != null); // follows from postcondition of ResolveExpression
- // resolve the method name
- UserDefinedType ctype;
- MemberDecl member = ResolveMember(s.Tok, s.Receiver.Type, s.MethodName, out ctype);
- Method callee = null;
- if (member == null) {
- // error has already been reported by ResolveMember
- } else if (!(member is Method)) {
- Error(s, "member {0} in class {1} does not refer to a method", s.MethodName, cce.NonNull(ctype).Name);
- } else {
- callee = (Method)member;
- s.Method = callee;
- s.IsGhost = callee.IsGhost;
- if (specContextOnly && !callee.IsGhost) {
- Error(s, "only ghost methods can be called from this context");
- }
- }
-
- // resolve any local variables declared here
- foreach (AutoVarDecl local in s.NewVars) {
- // first, fix up the local variables to be ghost variable if the corresponding formal out-parameter is a ghost
- if (s.IsGhost || callee != null && local.Index < callee.Outs.Count && callee.Outs[local.Index].IsGhost) {
- local.MakeGhost();
- }
- ResolveStatement(local, specContextOnly, method);
- }
-
- // resolve left-hand side
- Dictionary<string,object> lhsNameSet = new Dictionary<string,object>();
- foreach (IdentifierExpr lhs in s.Lhs) {
- ResolveExpression(lhs, true, true);
- if (lhsNameSet.ContainsKey(lhs.Name)) {
- Error(s, "Duplicate variable in left-hand side of call statement: {0}", lhs.Name);
- } else {
- lhsNameSet.Add(lhs.Name, null);
- }
- }
- // resolve arguments
- int j = 0;
- foreach (Expression e in s.Args) {
- bool allowGhost = s.IsGhost || callee == null || callee.Ins.Count <= j || callee.Ins[j].IsGhost;
- ResolveExpression(e, true, allowGhost);
- j++;
- }
-
- if (callee == null) {
- // error has been reported above
- } else if (callee.Ins.Count != s.Args.Count) {
- Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, callee.Ins.Count);
- } else if (callee.Outs.Count != s.Lhs.Count) {
- Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, callee.Outs.Count);
- } else {
- Contract.Assert(ctype != null); // follows from postcondition of ResolveMember above
- 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");
- }
- // build the type substitution map
- Dictionary<TypeParameter,Type> subst = new Dictionary<TypeParameter,Type>();
- for (int i = 0; i < ctype.TypeArgs.Count; i++) {
- subst.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
- }
- foreach (TypeParameter p in callee.TypeArgs) {
- subst.Add(p, new ParamTypeProxy(p));
- }
- // type check the arguments
- for (int i = 0; i < callee.Ins.Count; i++) {
- Type st = SubstType(callee.Ins[i].Type, subst);
- if (!UnifyTypes(cce.NonNull(s.Args[i].Type), st)) {
- Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
- }
- }
- for (int i = 0; i < callee.Outs.Count; i++) {
- Type st = SubstType(callee.Outs[i].Type, subst);
- IdentifierExpr lhs = s.Lhs[i];
- if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {
- Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);
- } else if (!specContextOnly && !cce.NonNull(lhs.Var).IsGhost && (s.IsGhost || callee.Outs[i].IsGhost)) {
- Error(s, "actual out-parameter {0} is required to be a ghost variable", i);
- }
- }
-
- // Resolution termination check
- if (method.EnclosingClass != null && callee.EnclosingClass != null) {
- ModuleDecl callerModule = method.EnclosingClass.Module;
- ModuleDecl calleeModule = callee.EnclosingClass.Module;
- if (callerModule == calleeModule) {
- // intra-module call; this is allowed; add edge in module's call graph
- callerModule.CallGraph.AddEdge(method, callee);
- } else if (calleeModule.IsDefaultModule) {
- // all is fine: everything implicitly imports the default module
- } else if (importGraph.Reaches(callerModule, calleeModule)) {
- // all is fine: the callee is downstream of the caller
- } else {
- Error(s, "inter-module calls must follow the module import relation (so module {0} must transitively import {1})", callerModule.Name, calleeModule.Name);
- }
- }
- }
+ ResolveCallStmt(s, specContextOnly, method, null);
} else if (stmt is BlockStmt) {
scope.PushMarker();
@@ -1572,6 +1470,126 @@ namespace Microsoft.Dafny { Contract.Assert(false); throw new cce.UnreachableException();
}
}
+
+ void ResolveCallStmt(CallStmt s, bool specContextOnly, Method method, Type receiverType) {
+ Contract.Requires(s != null);
+ Contract.Requires(method != null);
+ bool isInitCall = receiverType != null;
+
+ // resolve receiver, unless told otherwise
+ if (receiverType == null) {
+ ResolveReceiver(s.Receiver, true, false);
+ Contract.Assert(s.Receiver.Type != null); // follows from postcondition of ResolveExpression
+ receiverType = s.Receiver.Type;
+ }
+ // resolve the method name
+ UserDefinedType ctype;
+ MemberDecl member = ResolveMember(s.Tok, receiverType, s.MethodName, out ctype);
+ Method callee = null;
+ if (member == null) {
+ // error has already been reported by ResolveMember
+ } else if (!(member is Method)) {
+ Error(s, "member {0} in class {1} does not refer to a method", s.MethodName, cce.NonNull(ctype).Name);
+ } else {
+ callee = (Method)member;
+ s.Method = callee;
+ s.IsGhost = callee.IsGhost;
+ if (specContextOnly && !callee.IsGhost) {
+ Error(s, "only ghost methods can be called from this context");
+ }
+ }
+
+ // resolve any local variables declared here
+ foreach (AutoVarDecl local in s.NewVars) {
+ // first, fix up the local variables to be ghost variable if the corresponding formal out-parameter is a ghost
+ if (s.IsGhost || callee != null && local.Index < callee.Outs.Count && callee.Outs[local.Index].IsGhost) {
+ local.MakeGhost();
+ }
+ ResolveStatement(local, specContextOnly, method);
+ }
+
+ // resolve left-hand side
+ Dictionary<string, object> lhsNameSet = new Dictionary<string, object>();
+ foreach (IdentifierExpr lhs in s.Lhs) {
+ ResolveExpression(lhs, true, true);
+ if (lhsNameSet.ContainsKey(lhs.Name)) {
+ Error(s, "Duplicate variable in left-hand side of call statement: {0}", lhs.Name);
+ } else {
+ lhsNameSet.Add(lhs.Name, null);
+ }
+ }
+ // resolve arguments
+ int j = 0;
+ foreach (Expression e in s.Args) {
+ bool allowGhost = s.IsGhost || callee == null || callee.Ins.Count <= j || callee.Ins[j].IsGhost;
+ ResolveExpression(e, true, allowGhost);
+ j++;
+ }
+
+ if (callee == null) {
+ // error has been reported above
+ } else if (callee.Ins.Count != s.Args.Count) {
+ Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, callee.Ins.Count);
+ } else if (callee.Outs.Count != s.Lhs.Count) {
+ if (isInitCall) {
+ Error(s, "a method called as an initialization method must not have any result arguments");
+ } else {
+ Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, callee.Outs.Count);
+ }
+ } else {
+ Contract.Assert(ctype != null); // follows from postcondition of ResolveMember above
+ if (isInitCall) {
+ 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");
+ }
+ // build the type substitution map
+ Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
+ for (int i = 0; i < ctype.TypeArgs.Count; i++) {
+ subst.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
+ }
+ foreach (TypeParameter p in callee.TypeArgs) {
+ subst.Add(p, new ParamTypeProxy(p));
+ }
+ // type check the arguments
+ for (int i = 0; i < callee.Ins.Count; i++) {
+ Type st = SubstType(callee.Ins[i].Type, subst);
+ if (!UnifyTypes(cce.NonNull(s.Args[i].Type), st)) {
+ Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
+ }
+ }
+ for (int i = 0; i < callee.Outs.Count; i++) {
+ Type st = SubstType(callee.Outs[i].Type, subst);
+ IdentifierExpr lhs = s.Lhs[i];
+ if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {
+ Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);
+ } else if (!specContextOnly && !cce.NonNull(lhs.Var).IsGhost && (s.IsGhost || callee.Outs[i].IsGhost)) {
+ Error(s, "actual out-parameter {0} is required to be a ghost variable", i);
+ }
+ }
+
+ // Resolution termination check
+ if (method.EnclosingClass != null && callee.EnclosingClass != null) {
+ ModuleDecl callerModule = method.EnclosingClass.Module;
+ ModuleDecl calleeModule = callee.EnclosingClass.Module;
+ if (callerModule == calleeModule) {
+ // intra-module call; this is allowed; add edge in module's call graph
+ callerModule.CallGraph.AddEdge(method, callee);
+ } else if (calleeModule.IsDefaultModule) {
+ // all is fine: everything implicitly imports the default module
+ } else if (importGraph.Reaches(callerModule, calleeModule)) {
+ // all is fine: the callee is downstream of the caller
+ } else {
+ Error(s, "inter-module calls must follow the module import relation (so module {0} must transitively import {1})", callerModule.Name, calleeModule.Name);
+ }
+ }
+ }
+ }
void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, Method method)
{
@@ -1593,15 +1611,18 @@ namespace Microsoft.Dafny { for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }
}
- Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContext) {
+ Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContext, Method method) {
Contract.Requires(rr != null);
Contract.Requires(stmt != null);
+ Contract.Requires(method != null);
Contract.Ensures(Contract.Result<Type>() != null);
ResolveType(rr.EType);
if (rr.ArrayDimensions == null) {
if (!rr.EType.IsRefType) {
Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);
+ } else if (rr.InitCall != null) {
+ ResolveCallStmt(rr.InitCall, specContext, method, rr.EType);
}
return rr.EType;
} else {
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs index e99d4770..126c762b 100644 --- a/Dafny/Scanner.cs +++ b/Dafny/Scanner.cs @@ -271,13 +271,14 @@ public class Scanner { start[61] = 61;
start[91] = 27;
start[93] = 28;
- start[124] = 62;
+ start[46] = 62;
+ start[124] = 63;
start[8660] = 31;
start[8658] = 33;
start[38] = 34;
start[8743] = 36;
start[8744] = 38;
- start[33] = 63;
+ start[33] = 64;
start[8800] = 44;
start[8804] = 45;
start[8805] = 46;
@@ -287,7 +288,6 @@ public class Scanner { start[37] = 50;
start[172] = 51;
start[35] = 52;
- start[46] = 64;
start[8704] = 54;
start[8707] = 55;
start[8226] = 57;
@@ -519,23 +519,23 @@ public class Scanner { case "break": t.kind = 45; break;
case "return": t.kind = 46; break;
case "new": t.kind = 48; break;
- case "choose": t.kind = 51; break;
- case "havoc": t.kind = 52; break;
- case "if": t.kind = 53; break;
- case "else": t.kind = 54; break;
- case "while": t.kind = 55; break;
- case "invariant": t.kind = 56; break;
- case "call": t.kind = 57; break;
- case "foreach": t.kind = 58; break;
- case "in": t.kind = 59; break;
- case "assert": t.kind = 61; break;
- case "assume": t.kind = 62; break;
- case "use": t.kind = 63; break;
- case "print": t.kind = 64; break;
- case "then": t.kind = 65; break;
- case "false": t.kind = 89; break;
- case "true": t.kind = 90; break;
- case "null": t.kind = 91; break;
+ case "choose": t.kind = 52; break;
+ case "havoc": t.kind = 53; break;
+ case "if": t.kind = 54; break;
+ case "else": t.kind = 55; break;
+ case "while": t.kind = 56; break;
+ case "invariant": t.kind = 57; break;
+ case "call": t.kind = 58; break;
+ case "foreach": t.kind = 59; break;
+ case "in": t.kind = 60; break;
+ case "assert": t.kind = 62; break;
+ case "assume": t.kind = 63; break;
+ case "use": t.kind = 64; break;
+ case "print": t.kind = 65; break;
+ case "then": t.kind = 66; break;
+ case "false": t.kind = 90; break;
+ case "true": t.kind = 91; break;
+ case "null": t.kind = 92; break;
case "fresh": t.kind = 94; break;
case "allocated": t.kind = 95; break;
case "this": t.kind = 97; break;
@@ -670,53 +670,53 @@ public class Scanner { if (ch == '>') {AddCh(); goto case 30;}
else {goto case 0;}
case 30:
- {t.kind = 66; break;}
- case 31:
{t.kind = 67; break;}
- case 32:
+ case 31:
{t.kind = 68; break;}
- case 33:
+ case 32:
{t.kind = 69; break;}
+ case 33:
+ {t.kind = 70; break;}
case 34:
if (ch == '&') {AddCh(); goto case 35;}
else {goto case 0;}
case 35:
- {t.kind = 70; break;}
- case 36:
{t.kind = 71; break;}
- case 37:
+ case 36:
{t.kind = 72; break;}
- case 38:
+ case 37:
{t.kind = 73; break;}
+ case 38:
+ {t.kind = 74; break;}
case 39:
- {t.kind = 76; break;}
- case 40:
{t.kind = 77; break;}
- case 41:
+ case 40:
{t.kind = 78; break;}
+ case 41:
+ {t.kind = 79; break;}
case 42:
if (ch == 'n') {AddCh(); goto case 43;}
else {goto case 0;}
case 43:
- {t.kind = 79; break;}
- case 44:
{t.kind = 80; break;}
- case 45:
+ case 44:
{t.kind = 81; break;}
- case 46:
+ case 45:
{t.kind = 82; break;}
- case 47:
+ case 46:
{t.kind = 83; break;}
- case 48:
+ case 47:
{t.kind = 84; break;}
- case 49:
+ case 48:
{t.kind = 85; break;}
- case 50:
+ case 49:
{t.kind = 86; break;}
+ case 50:
+ {t.kind = 87; break;}
case 51:
- {t.kind = 88; break;}
+ {t.kind = 89; break;}
case 52:
- {t.kind = 92; break;}
+ {t.kind = 93; break;}
case 53:
{t.kind = 96; break;}
case 54:
@@ -745,27 +745,27 @@ public class Scanner { else if (ch == '=') {AddCh(); goto case 66;}
else {goto case 0;}
case 62:
- recEnd = pos; recKind = 60;
- if (ch == '|') {AddCh(); goto case 37;}
- else {t.kind = 60; break;}
+ recEnd = pos; recKind = 51;
+ if (ch == '.') {AddCh(); goto case 53;}
+ else {t.kind = 51; break;}
case 63:
- recEnd = pos; recKind = 87;
+ recEnd = pos; recKind = 61;
+ if (ch == '|') {AddCh(); goto case 37;}
+ else {t.kind = 61; break;}
+ case 64:
+ 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 = 87; break;}
- case 64:
- recEnd = pos; recKind = 93;
- if (ch == '.') {AddCh(); goto case 53;}
- else {t.kind = 93; break;}
+ else {t.kind = 88; break;}
case 65:
- recEnd = pos; recKind = 75;
+ recEnd = pos; recKind = 76;
if (ch == '=') {AddCh(); goto case 29;}
- else {t.kind = 75; break;}
+ else {t.kind = 76; break;}
case 66:
- recEnd = pos; recKind = 74;
+ recEnd = pos; recKind = 75;
if (ch == '>') {AddCh(); goto case 32;}
- else {t.kind = 74; break;}
+ else {t.kind = 75; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index aff8c86a..18b7a22f 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -1345,7 +1345,7 @@ namespace Microsoft.Dafny { Contract.Requires(predef != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
- if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr) {
+ if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
return Bpl.Expr.True;
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
@@ -1503,7 +1503,7 @@ namespace Microsoft.Dafny { Contract.Requires(predef != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
- if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr) {
+ if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
return Bpl.Expr.True;
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
@@ -1714,7 +1714,7 @@ namespace Microsoft.Dafny { Contract.Requires(etran != null);
Contract.Requires(predef != null);
- if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr) {
+ if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
// always allowed
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
@@ -2848,91 +2848,7 @@ namespace Microsoft.Dafny { } else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
- foreach (VarDecl local in s.NewVars) {
- TrStmt(local, builder, locals, etran);
- }
- AddComment(builder, stmt, "call statement");
- Bpl.ExprSeq ins = new Bpl.ExprSeq();
- Contract.Assert(s.Method != null); // follows from the fact that stmt has been successfully resolved
- if (!s.Method.IsStatic) {
- ins.Add(etran.TrExpr(s.Receiver));
- }
-
- // Ideally, the modifies and decreases checks would be done after the precondition check,
- // but Boogie doesn't give us a hook for that. So, we set up our own local variables here to
- // store the actual parameters.
- // Create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
- Dictionary<IVariable,Expression> substMap = new Dictionary<IVariable,Expression>();
- for (int i = 0; i < s.Method.Ins.Count; i++) {
- Formal p = s.Method.Ins[i];
- VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost, null);
- local.type = local.OptionalType; // resolve local here
- IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);
- ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here
- substMap.Add(p, ie);
- locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
-
- Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
- Expression actual = s.Args[i];
- TrStmt_CheckWellformed(actual, builder, locals, etran, true);
- Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(stmt.Tok, etran.TrExpr(actual), cce.NonNull(actual.Type), s.Method.Ins[i].Type));
- builder.Add(cmd);
- ins.Add(lhs);
- }
- // Also create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.
- Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();
- List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>(s.Lhs.Count);
- for (int i = 0; i < s.Lhs.Count; i++) {
- Expression e = s.Lhs[i];
- if (ExpressionTranslator.ModeledAsBoxType(s.Method.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType(cce.NonNull(e.Type))) {
- // we need an Unbox
- Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$tmp#" + otherTmpVarCount, predef.BoxType));
- otherTmpVarCount++;
- locals.Add(var);
- Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(stmt.Tok, var.Name, predef.BoxType);
- tmpOuts.Add(varIdE);
- outs.Add(varIdE);
- } else {
- tmpOuts.Add(null);
- outs.Add(etran.TrExpr(e));
- }
- }
-
- // Check modifies clause
- CheckFrameSubset(stmt.Tok, s.Method.Mod, s.Receiver, substMap, etran, builder, "call may violate caller's modifies clause", null);
-
- // Check termination
- ModuleDecl module = cce.NonNull(s.Method.EnclosingClass).Module;
- if (module == cce.NonNull(currentMethod.EnclosingClass).Module) {
- if (module.CallGraph.GetSCCRepresentative(s.Method) == module.CallGraph.GetSCCRepresentative(currentMethod)) {
- bool contextDecrInferred, calleeDecrInferred;
- List<Expression> contextDecreases = MethodDecreasesWithDefault(currentMethod, out contextDecrInferred);
- List<Expression> calleeDecreases = MethodDecreasesWithDefault(s.Method, out calleeDecrInferred);
- CheckCallTermination(stmt.Tok, contextDecreases, calleeDecreases, null, s.Receiver, substMap, etran, builder, contextDecrInferred);
- }
- }
-
- // Make the call
- Bpl.CallCmd call = new Bpl.CallCmd(stmt.Tok, s.Method.FullName, ins, outs);
- builder.Add(call);
- for (int i = 0; i < s.Lhs.Count; i++) {
- Bpl.IdentifierExpr tmpVarIdE = tmpOuts[i];
- IdentifierExpr e = s.Lhs[i];
- Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(e); // TODO: is this cast always justified?
- if (tmpVarIdE != null) {
- // Instead of an assignment:
- // e := UnBox(tmpVar);
- // we use:
- // havoc e; assume e == UnBox(tmpVar);
- // because that will reap the benefits of e's where clause, so that some additional type information will be known about
- // the out-parameter.
- Bpl.Cmd cmd = new Bpl.HavocCmd(stmt.Tok, new IdentifierExprSeq(lhs));
- builder.Add(cmd);
- cmd = new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.Eq(lhs, FunctionCall(stmt.Tok, BuiltinFunction.Unbox, TrType(cce.NonNull(e.Type)), tmpVarIdE)));
- builder.Add(cmd);
- }
- }
- builder.Add(CaptureState(stmt.Tok));
+ TrCallStmt(s, builder, locals, etran, null);
} else if (stmt is BlockStmt) {
foreach (Statement ss in ((BlockStmt)stmt).Body) {
@@ -3265,6 +3181,100 @@ namespace Microsoft.Dafny { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
}
+
+ void TrCallStmt(CallStmt s, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran, Bpl.Expr actualReceiver) {
+ Contract.Requires(s != null);
+ Contract.Requires(builder != null);
+ Contract.Requires(locals != null);
+ Contract.Requires(etran != null);
+
+ Expression receiver = actualReceiver == null ? s.Receiver : new BoogieWrapper(actualReceiver);
+ foreach (VarDecl local in s.NewVars) {
+ TrStmt(local, builder, locals, etran);
+ }
+ AddComment(builder, s, actualReceiver == null ? "call statement" : "init call statement");
+ Bpl.ExprSeq ins = new Bpl.ExprSeq();
+ Contract.Assert(s.Method != null); // follows from the fact that stmt has been successfully resolved
+ if (!s.Method.IsStatic) {
+ ins.Add(etran.TrExpr(receiver));
+ }
+
+ // Ideally, the modifies and decreases checks would be done after the precondition check,
+ // but Boogie doesn't give us a hook for that. So, we set up our own local variables here to
+ // store the actual parameters.
+ // Create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
+ Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost, null);
+ local.type = local.OptionalType; // resolve local here
+ IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);
+ ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here
+ substMap.Add(p, ie);
+ locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
+
+ Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
+ Expression actual = s.Args[i];
+ TrStmt_CheckWellformed(actual, builder, locals, etran, true);
+ Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(s.Tok, etran.TrExpr(actual), cce.NonNull(actual.Type), s.Method.Ins[i].Type));
+ builder.Add(cmd);
+ ins.Add(lhs);
+ }
+ // Also create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.
+ Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();
+ List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>(s.Lhs.Count);
+ for (int i = 0; i < s.Lhs.Count; i++) {
+ Expression e = s.Lhs[i];
+ if (ExpressionTranslator.ModeledAsBoxType(s.Method.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType(cce.NonNull(e.Type))) {
+ // we need an Unbox
+ Bpl.LocalVariable var = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$tmp#" + otherTmpVarCount, predef.BoxType));
+ otherTmpVarCount++;
+ locals.Add(var);
+ Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(s.Tok, var.Name, predef.BoxType);
+ tmpOuts.Add(varIdE);
+ outs.Add(varIdE);
+ } else {
+ tmpOuts.Add(null);
+ outs.Add(etran.TrExpr(e));
+ }
+ }
+
+ // Check modifies clause
+ CheckFrameSubset(s.Tok, s.Method.Mod, receiver, substMap, etran, builder, "call may violate caller's modifies clause", null);
+
+ // Check termination
+ ModuleDecl module = cce.NonNull(s.Method.EnclosingClass).Module;
+ if (module == cce.NonNull(currentMethod.EnclosingClass).Module) {
+ if (module.CallGraph.GetSCCRepresentative(s.Method) == module.CallGraph.GetSCCRepresentative(currentMethod)) {
+ bool contextDecrInferred, calleeDecrInferred;
+ List<Expression> contextDecreases = MethodDecreasesWithDefault(currentMethod, out contextDecrInferred);
+ List<Expression> calleeDecreases = MethodDecreasesWithDefault(s.Method, out calleeDecrInferred);
+ CheckCallTermination(s.Tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, builder, contextDecrInferred);
+ }
+ }
+
+ // Make the call
+ Bpl.CallCmd call = new Bpl.CallCmd(s.Tok, s.Method.FullName, ins, outs);
+ builder.Add(call);
+ for (int i = 0; i < s.Lhs.Count; i++) {
+ Bpl.IdentifierExpr tmpVarIdE = tmpOuts[i];
+ IdentifierExpr e = s.Lhs[i];
+ Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(e); // TODO: is this cast always justified?
+ if (tmpVarIdE != null) {
+ // Instead of an assignment:
+ // e := UnBox(tmpVar);
+ // we use:
+ // havoc e; assume e == UnBox(tmpVar);
+ // because that will reap the benefits of e's where clause, so that some additional type information will be known about
+ // the out-parameter.
+ Bpl.Cmd cmd = new Bpl.HavocCmd(s.Tok, new IdentifierExprSeq(lhs));
+ builder.Add(cmd);
+ cmd = new Bpl.AssumeCmd(s.Tok, Bpl.Expr.Eq(lhs, FunctionCall(s.Tok, BuiltinFunction.Unbox, TrType(cce.NonNull(e.Type)), tmpVarIdE)));
+ builder.Add(cmd);
+ }
+ }
+ builder.Add(CaptureState(s.Tok));
+ }
static Expression CreateIntLiteral(IToken tok, int n)
{
@@ -3707,7 +3717,7 @@ namespace Microsoft.Dafny { } else if (rhs is HavocRhs) {
Contract.Assert(lhs is IdentifierExpr); // for this kind of RHS, the LHS is restricted to be a simple variable
- Bpl.IdentifierExpr x = (Bpl.IdentifierExpr)etran.TrExpr(lhs); // TODO: is this cast always justified?
+ var x = (Bpl.IdentifierExpr)etran.TrExpr(lhs); // TODO: is this cast always justified?
builder.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(x)));
} else {
@@ -3726,7 +3736,7 @@ namespace Microsoft.Dafny { i++;
}
}
-
+
Bpl.IdentifierExpr nw = GetNewVar_IdExpr(tok, locals);
builder.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(nw)));
// assume $nw != null && !$Heap[$nw, alloc] && dtype($nw) == RHS;
@@ -3757,11 +3767,14 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr heap = (Bpl.IdentifierExpr/*TODO: this cast is dubious*/)etran.HeapExpr;
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, heap, ExpressionTranslator.UpdateHeap(tok, heap, nw, alloc, Bpl.Expr.True));
builder.Add(cmd);
+ // assume $IsGoodHeap($Heap);
+ builder.Add(AssumeGoodHeap(tok, etran));
+ if (tRhs.InitCall != null) {
+ TrCallStmt(tRhs.InitCall, builder, locals, etran, nw);
+ }
// x := $nw;
Bpl.IdentifierExpr x = (Bpl.IdentifierExpr)etran.TrExpr(lhs); // TODO: is this cast always justified?
builder.Add(Bpl.Cmd.SimpleAssign(tok, x, nw));
- // assume $IsGoodHeap($Heap);
- builder.Add(AssumeGoodHeap(tok, etran));
}
builder.Add(CaptureState(tok));
}
@@ -3775,8 +3788,23 @@ namespace Microsoft.Dafny { }
// ----- Expression ---------------------------------------------------------------------------
-
- internal class ExpressionTranslator {
+
+ /// <summary>
+ /// This class gives a way to represent a Boogie translation target as if it were still a Dafny expression.
+ /// </summary>
+ internal class BoogieWrapper : Expression
+ {
+ public readonly Bpl.Expr Expr;
+ public BoogieWrapper(Bpl.Expr expr)
+ : base(expr.tok)
+ {
+ Contract.Requires(expr != null);
+ Expr = expr;
+ }
+ }
+
+ internal class ExpressionTranslator
+ {
public readonly Bpl.Expr HeapExpr;
public readonly PredefinedDecls predef;
public readonly Translator translator;
@@ -3938,6 +3966,10 @@ namespace Microsoft.Dafny { } else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
return TrVar(expr.tok, cce.NonNull(e.Var));
+
+ } else if (expr is BoogieWrapper) {
+ var e = (BoogieWrapper)expr;
+ return e.Expr;
} else if (expr is SetDisplayExpr) {
SetDisplayExpr e = (SetDisplayExpr)expr;
@@ -5198,7 +5230,7 @@ namespace Microsoft.Dafny { Contract.Requires(expr != null);
Contract.Requires(n != null);
- if (expr is LiteralExpr || expr is WildcardExpr || expr is ThisExpr) {
+ if (expr is LiteralExpr || expr is WildcardExpr || expr is ThisExpr || expr is BoogieWrapper) {
return false;
} else if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
@@ -5335,7 +5367,7 @@ namespace Microsoft.Dafny { Expression newExpr = null; // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end
- if (expr is LiteralExpr || expr is WildcardExpr) {
+ if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) {
// nothing to substitute
} else if (expr is ThisExpr) {
return receiverReplacement == null ? expr : receiverReplacement;
diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy index fdda243c..cf109c1a 100644 --- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy +++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy @@ -30,12 +30,10 @@ class AmortizedQueue<T> { modifies this;
ensures Valid() && List == [];
{
- var tmp := new LinkedList<T>;
+ var tmp := new LinkedList<T>.Init();
front := tmp;
- call front.Init();
- tmp := new LinkedList<T>;
+ tmp := new LinkedList<T>.Init();
rear := tmp;
- call rear.Init();
Repr := {this};
Repr := Repr + front.Repr + rear.Repr;
List := [];
@@ -54,8 +52,7 @@ class AmortizedQueue<T> { call ff := f.Concat(rr);
front := ff;
- var tmp := new LinkedList<T>;
- call tmp.Init();
+ var tmp := new LinkedList<T>.Init();
rear := tmp;
}
Repr := {this};
@@ -74,8 +71,7 @@ class AmortizedQueue<T> { requires Valid() && List != [];
ensures r != null && r.Valid() && r.List == List[1..];
{
- r := new AmortizedQueue<T>;
- call r.InitFromPieces(front.tail, rear);
+ r := new AmortizedQueue<T>.InitFromPieces(front.tail, rear);
}
method Enqueue(item: T) returns (r: AmortizedQueue<T>)
@@ -83,8 +79,7 @@ class AmortizedQueue<T> { ensures r != null && r.Valid() && r.List == List + [item];
{
call rr := rear.Cons(item);
- var tmp := new AmortizedQueue<T>;
- call tmp.InitFromPieces(front, rr);
+ var tmp := new AmortizedQueue<T>.InitFromPieces(front, rr);
r := tmp;
}
}
@@ -158,8 +153,7 @@ class LinkedList<T> { r := this;
} else {
call r := tail.Reverse();
- var e := new LinkedList<T>;
- call e.Init();
+ var e := new LinkedList<T>.Init();
call e := e.Cons(head);
call r := r.Concat(e);
}
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index bb88b265..3f30c4b5 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -54,8 +54,7 @@ class Benchmark3 { // the final Queue is a permutation of the input Queue
ensures (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
{
- r := new Queue<int>;
- call r.Init();
+ r := new Queue<int>.Init();
ghost var p := [];
var n := 0;
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy index 94fe1eaa..d9bd36f5 100644 --- a/Test/VSI-Benchmarks/b5.dfy +++ b/Test/VSI-Benchmarks/b5.dfy @@ -31,8 +31,7 @@ class Queue<T> { ensures Valid() && fresh(footprint - {this});
ensures |contents| == 0;
{
- var n := new Node<T>;
- call n.Init();
+ var n := new Node<T>.Init();
head := n;
tail := n;
contents := n.tailContents;
@@ -53,8 +52,8 @@ class Queue<T> { ensures Valid() && fresh(footprint - old(footprint));
ensures contents == old(contents) + [t];
{
- var n := new Node<T>;
- call n.Init(); n.data := t;
+ var n := new Node<T>.Init();
+ n.data := t;
tail.next := n;
tail := n;
@@ -150,10 +149,8 @@ class Node<T> { class Main<U> {
method A<T>(t: T, u: T, v: T)
{
- var q0 := new Queue<T>;
- call q0.Init();
- var q1 := new Queue<T>;
- call q1.Init();
+ var q0 := new Queue<T>.Init();
+ var q1 := new Queue<T>.Init();
call q0.Enqueue(t);
call q0.Enqueue(u);
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy index 9b244e69..13086f28 100644 --- a/Test/VSI-Benchmarks/b6.dfy +++ b/Test/VSI-Benchmarks/b6.dfy @@ -47,8 +47,7 @@ class Collection<T> { ensures fresh(iter.footprint) && iter.pos == -1;
ensures iter.c == this;
{
- iter:= new Iterator<T>;
- call iter.Init(this);
+ iter:= new Iterator<T>.Init(this);
}
}
@@ -107,8 +106,7 @@ class Client method Main()
{
- var c := new Collection<int>;
- call c.Init();
+ var c := new Collection<int>.Init();
call c.Add(33);
call c.Add(45);
call c.Add(78);
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index a37f86e4..02c1a63a 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -47,10 +47,8 @@ class Glossary { {
var rs:= new ReaderStream;
call rs.Open();
- var glossary := new Map<Word,seq<Word>>;
- call glossary.Init();
- var q:= new Queue<Word>;
- call q.Init();
+ var glossary := new Map<Word,seq<Word>>.Init();
+ var q:= new Queue<Word>.Init();
while (true)
invariant rs.Valid() && fresh(rs.footprint);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 08570842..f57c6ead 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -79,7 +79,9 @@ TypeTests.dfy(64,6): Error: Duplicate local-variable name: z TypeTests.dfy(66,6): Error: Duplicate local-variable name: x
TypeTests.dfy(69,8): Error: Duplicate local-variable name: x
TypeTests.dfy(72,6): Error: Duplicate local-variable name: y
-14 resolution/type errors detected in TypeTests.dfy
+TypeTests.dfy(79,17): Error: member F in class C does not refer to a method
+TypeTests.dfy(80,17): Error: a method called as an initialization method must not have any result arguments
+16 resolution/type errors detected in TypeTests.dfy
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
@@ -142,8 +144,14 @@ Execution trace: (0,0): anon6
(0,0): anon14_Then
(0,0): anon11
+SmallTests.dfy(272,24): Error BP5002: A precondition for this call might not hold.
+SmallTests.dfy(250,30): Related location: This is the precondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(267,19): anon3_Else
+ (0,0): anon2
-Dafny program verifier finished with 29 verified, 12 errors
+Dafny program verifier finished with 34 verified, 13 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 2eca82fd..a839d5a9 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -232,3 +232,43 @@ datatype Lindgren { Longstocking(seq<object>, Lindgren);
HerrNilsson;
}
+
+// --------------------------------------------------
+
+class InitCalls {
+ var z: int;
+ var p: InitCalls;
+
+ method Init(y: int)
+ modifies this;
+ ensures z == y;
+ {
+ z := y;
+ }
+
+ method InitFromReference(q: InitCalls)
+ requires q != null && 15 <= q.z;
+ modifies this;
+ ensures p == q;
+ {
+ p := q;
+ }
+
+ method TestDriver()
+ {
+ var c: InitCalls;
+ c := new InitCalls.Init(15);
+ var d := new InitCalls.Init(17);
+ var e: InitCalls := new InitCalls.Init(18);
+ var f: object := new InitCalls.Init(19);
+ assert c.z + d.z + e.z == 50;
+ // poor man's type cast:
+ ghost var g: InitCalls;
+ assert f == g ==> g.z == 19;
+
+ // test that the call is done before the assignment to the LHS
+ var r := c;
+ r := new InitCalls.InitFromReference(r); // fine, since r.z==15
+ r := new InitCalls.InitFromReference(r); // error, since r.z is unknown
+ }
+}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 6e8e2b72..cbab53bf 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -72,3 +72,11 @@ method DuplicateVarName(x: int) returns (y: int) var y := y; // error: redeclaration of an out-parameter is not allowed (it is
// treated like an outermost-scoped local in this regard)
}
+
+// ---------------------
+
+method InitCalls() {
+ var c := new C.F(null, null); // error: F is not a method
+ var d := new C.M(8); // error: M has out parameters
+ var e := new C.Caller();
+}
diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy index fbda3ecb..b4980d4b 100644 --- a/Test/dafny1/BinaryTree.dfy +++ b/Test/dafny1/BinaryTree.dfy @@ -58,8 +58,7 @@ class IntSet { decreases if n == null then {} else n.Repr;
{
if (n == null) {
- m := new Node;
- call m.Init(x);
+ m := new Node.Init(x);
} else if (x == n.data) {
m := n;
} else {
@@ -224,8 +223,7 @@ class Node { class Main {
method Client0(x: int)
{
- var s := new IntSet;
- call s.Init();
+ var s := new IntSet.Init();
call s.Insert(12);
call s.Insert(24);
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index 810931be..b790eea5 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -90,8 +90,8 @@ class ExtensibleArray<T> { elements[length - M] := t;
} else {
if (more == null) {
- var mr := new ExtensibleArray<array<T>>; more := mr;
- call mr.Init();
+ var mr := new ExtensibleArray<array<T>>.Init();
+ more := mr;
Repr := Repr + {mr} + mr.Repr;
}
// "elements" is full, so move it into "more" and allocate a new array
@@ -108,8 +108,7 @@ class ExtensibleArray<T> { }
method Main() {
- var a := new ExtensibleArray<int>;
- call a.Init();
+ var a := new ExtensibleArray<int>.Init();
var n := 0;
while (n < 256*256+600)
invariant a.Valid() && fresh(a.Repr);
diff --git a/Test/dafny1/ListCopy.dfy b/Test/dafny1/ListCopy.dfy index 52f5cf76..d5febfe0 100644 --- a/Test/dafny1/ListCopy.dfy +++ b/Test/dafny1/ListCopy.dfy @@ -19,8 +19,7 @@ class Node { var newRegion: set<Node> := {};
if (oldListPtr != null) {
- newRoot := new Node;
- call newRoot.Init();
+ newRoot := new Node.Init();
newRegion := newRegion + {newRoot};
var prev := newRoot;
@@ -33,8 +32,7 @@ class Node { invariant newRegion !! existingRegion;
decreases *; // omit loop termination check
{
- var tmp := new Node;
- call tmp.Init();
+ var tmp := new Node.Init();
newRegion := newRegion + {tmp};
prev.nxt := tmp;
diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy index 42b7dd64..0ee953e1 100644 --- a/Test/dafny1/Queue.dfy +++ b/Test/dafny1/Queue.dfy @@ -33,8 +33,7 @@ class Queue<T> { ensures Valid() && fresh(footprint - {this});
ensures |contents| == 0;
{
- var n := new Node<T>;
- call n.Init();
+ var n := new Node<T>.Init();
head := n;
tail := n;
contents := n.tailContents;
@@ -81,8 +80,8 @@ class Queue<T> { ensures Valid() && fresh(footprint - old(footprint));
ensures contents == old(contents) + [t];
{
- var n := new Node<T>;
- call n.Init(); n.data := t;
+ var n := new Node<T>.Init();
+ n.data := t;
tail.next := n;
tail := n;
@@ -150,10 +149,8 @@ class Node<T> { class Main<U> {
method A<T>(t: T, u: T, v: T)
{
- var q0 := new Queue<T>;
- call q0.Init();
- var q1 := new Queue<T>;
- call q1.Init();
+ var q0 := new Queue<T>.Init();
+ var q1 := new Queue<T>.Init();
call q0.Enqueue(t);
call q0.Enqueue(u);
diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy index 4c3b095a..940e1a0a 100644 --- a/Test/dafny1/UnboundedStack.dfy +++ b/Test/dafny1/UnboundedStack.dfy @@ -31,8 +31,7 @@ class UnboundedStack<T> { ensures IsUnboundedStack();
ensures content == [val] + old(content);
{
- var tmp := new Node<T>;
- call tmp.InitNode(val,top);
+ var tmp := new Node<T>.InitNode(val,top);
top := tmp;
representation := representation + top.footprint;
content := [val] + content;
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy index 87e63e2c..95ad12fa 100644 --- a/Test/vacid0/Composite.dfy +++ b/Test/vacid0/Composite.dfy @@ -135,18 +135,14 @@ class Composite { method Main()
{
- var c0 := new Composite;
- call c0.Init(57);
+ var c0 := new Composite.Init(57);
- var c1 := new Composite;
- call c1.Init(12);
+ var c1 := new Composite.Init(12);
call c0.Add({c0}, c1, {c1});
- var c2 := new Composite;
- call c2.Init(48);
+ var c2 := new Composite.Init(48);
- var c3 := new Composite;
- call c3.Init(48);
+ var c3 := new Composite.Init(48);
call c2.Add({c2}, c3, {c3});
call c0.Add({c0,c1}, c2, {c2,c3});
@@ -160,15 +156,15 @@ method Main() }
method Harness() {
- var a := new Composite; call a.Init(5);
- var b := new Composite; call b.Init(7);
+ var a := new Composite.Init(5);
+ var b := new Composite.Init(7);
call a.Add({a}, b, {b});
assert a.sum == 12;
call b.Update(17, {a,b});
assert a.sum == 22;
- var c := new Composite; call c.Init(10);
+ var c := new Composite.Init(10);
call b.Add({a,b}, c, {c});
call b.Dislodge({a,b,c});
assert b.sum == 27;
|