summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg16
-rw-r--r--Source/Dafny/DafnyAst.cs55
-rw-r--r--Source/Dafny/Parser.cs771
-rw-r--r--Source/Dafny/Printer.cs2
-rw-r--r--Source/Dafny/Resolver.cs25
-rw-r--r--Source/Dafny/Scanner.cs275
-rw-r--r--Test/dafny0/Answer5
-rw-r--r--Test/dafny0/ResolutionErrors.dfy27
-rw-r--r--Util/Emacs/dafny-mode.el2
-rw-r--r--Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs3
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs1
-rw-r--r--Util/latex/dafny.sty2
-rw-r--r--Util/vim/syntax/dafny.vim2
13 files changed, 634 insertions, 552 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 91028093..c8c6cbf1 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -416,20 +416,30 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
List<MaybeFreeExpression/*!*/> ens = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> dec = new List<Expression/*!*/>();
Statement/*!*/ bb; BlockStmt body = null;
+ bool isConstructor = false;
bool isRefinement = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
( "method"
+ | "constructor" (. isConstructor = true; .)
| "refines" (. isRefinement = true; .)
)
(. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
+ if (isConstructor) {
+ if (mmod.IsGhost) {
+ SemErr(t, "constructors cannot be declared 'ghost'");
+ }
+ if (mmod.IsStatic) {
+ SemErr(t, "constructors cannot be declared 'static'");
+ }
+ }
.)
{ Attribute<ref attrs> }
Ident<out id>
[ GenericParameters<typeArgs> ]
Formals<true, !mmod.IsGhost, ins>
- [ "returns"
+ [ "returns" (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
Formals<false, !mmod.IsGhost, outs>
]
@@ -439,7 +449,9 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
(. if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
- else
+ else if (isConstructor)
+ m = new Constructor(id, id.val, typeArgs, ins, 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;
m.BodyEndTok = bodyEnd;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b650b655..ab98c57e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -630,6 +630,7 @@ namespace Microsoft.Dafny {
public class ClassDecl : TopLevelDecl {
public readonly List<MemberDecl/*!*/>/*!*/ Members;
+ public bool HasConstructor; // filled in (early) during resolution; true iff there exists a member that is a Constructor
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Members));
@@ -1055,7 +1056,6 @@ namespace Microsoft.Dafny {
this.Ens = ens;
this.Decreases = decreases;
this.Body = body;
-
}
}
@@ -1080,7 +1080,6 @@ namespace Microsoft.Dafny {
Contract.Invariant(cce.NonNullElements(Decreases));
}
-
public Method(IToken tok, string name,
bool isStatic, bool isGhost,
[Captured] List<TypeParameter/*!*/>/*!*/ typeArgs,
@@ -1109,11 +1108,33 @@ namespace Microsoft.Dafny {
this.Ens = ens;
this.Decreases = decreases;
this.Body = body;
+ }
+ }
+ public class Constructor : Method
+ {
+ public Constructor(IToken tok, string name,
+ [Captured] List<TypeParameter/*!*/>/*!*/ typeArgs,
+ [Captured] List<Formal/*!*/>/*!*/ ins,
+ [Captured] List<MaybeFreeExpression/*!*/>/*!*/ req, [Captured] List<FrameExpression/*!*/>/*!*/ mod,
+ [Captured] List<MaybeFreeExpression/*!*/>/*!*/ ens,
+ [Captured] List<Expression/*!*/>/*!*/ decreases,
+ [Captured] BlockStmt body,
+ Attributes attributes)
+ : base(tok, name, false, false, typeArgs, ins, new List<Formal>(), req, mod, ens, decreases, body, attributes) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(ins));
+ Contract.Requires(cce.NonNullElements(req));
+ Contract.Requires(cce.NonNullElements(mod));
+ Contract.Requires(cce.NonNullElements(ens));
+ Contract.Requires(cce.NonNullElements(decreases));
}
}
- public class MethodRefinement : Method {
+ public class MethodRefinement : Method
+ {
public Method Refined; // filled in during resolution
public MethodRefinement(IToken/*!*/ tok, string/*!*/ name,
bool isStatic, bool isGhost,
@@ -1134,7 +1155,6 @@ namespace Microsoft.Dafny {
Contract.Requires(cce.NonNullElements(mod));
Contract.Requires(cce.NonNullElements(ens));
Contract.Requires(cce.NonNullElements(decreases));
-
}
}
@@ -1443,33 +1463,6 @@ namespace Microsoft.Dafny {
this.Lhs = lhs;
this.Rhs = rhs;
}
-#if OLD_STUFF
- public AssignStmt(IToken tok, Expression lhs, Expression rhs)
- : base(tok) { // ordinary assignment statement
- Contract.Requires(tok != null);
- Contract.Requires(lhs != null);
- Contract.Requires(rhs != null);
- this.Lhs = lhs;
- this.Rhs = new ExprRhs(rhs);
- }
- 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, initCall);
- }
- public AssignStmt(IToken tok, Expression lhs, Type type, List<Expression> arrayDimensions)
- : base(tok) { // array alloc statement
- Contract.Requires(tok != null);
- Contract.Requires(lhs != null);
- Contract.Requires(type != null);
- Contract.Requires(arrayDimensions != null && 1 <= arrayDimensions.Count);
- this.Lhs = lhs;
- this.Rhs = new TypeRhs(type, arrayDimensions);
- }
-#endif
public AssignStmt(IToken tok, Expression lhs)
: base(tok) { // havoc
Contract.Requires(tok != null);
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 100e34e1..94f2c240 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -20,12 +20,12 @@ public class Parser {
public const int _digits = 2;
public const int _arrayToken = 3;
public const int _string = 4;
- public const int maxT = 104;
+ public const int maxT = 105;
const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -144,10 +144,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
@@ -160,15 +160,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -192,7 +192,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -379,15 +379,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
if (la.kind == 18) {
FieldDecl(mmod, mm);
- } else if (la.kind == 40) {
+ } else if (la.kind == 41) {
FunctionDecl(mmod, out f);
mm.Add(f);
- } else if (la.kind == 10 || la.kind == 25) {
+ } else if (la.kind == 10 || la.kind == 25 || la.kind == 26) {
MethodDecl(mmod, out m);
mm.Add(m);
} else if (la.kind == 20) {
CouplingInvDecl(mmod, mm);
- } else SynErr(105);
+ } else SynErr(106);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -442,7 +442,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- Expect(40);
+ Expect(41);
if (la.kind == 25) {
Get();
isFunctionMethod = true;
@@ -470,7 +470,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
FunctionBody(out bb, out bodyStart, out bodyEnd);
body = bb;
- } else SynErr(106);
+ } else SynErr(107);
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;
@@ -489,17 +489,29 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
List<MaybeFreeExpression/*!*/> ens = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> dec = new List<Expression/*!*/>();
Statement/*!*/ bb; BlockStmt body = null;
+ bool isConstructor = false;
bool isRefinement = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
if (la.kind == 25) {
Get();
+ } else if (la.kind == 26) {
+ Get();
+ isConstructor = true;
} else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(107);
+ } else SynErr(108);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
+ if (isConstructor) {
+ if (mmod.IsGhost) {
+ SemErr(t, "constructors cannot be declared 'ghost'");
+ }
+ if (mmod.IsStatic) {
+ SemErr(t, "constructors cannot be declared 'static'");
+ }
+ }
while (la.kind == 7) {
Attribute(ref attrs);
@@ -509,8 +521,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
GenericParameters(typeArgs);
}
Formals(true, !mmod.IsGhost, ins);
- if (la.kind == 26) {
+ if (la.kind == 27) {
Get();
+ if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs);
}
if (la.kind == 17) {
@@ -524,10 +537,12 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
BlockStmt(out bb, out bodyStart, out bodyEnd);
body = (BlockStmt)bb;
- } else SynErr(108);
+ } else SynErr(109);
if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
- else
+ else if (isConstructor)
+ m = new Constructor(id, id.val, typeArgs, ins, 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;
m.BodyEndTok = bodyEnd;
@@ -572,7 +587,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 32) {
+ if (la.kind == 33) {
FormalsOptionalIds(formals);
}
ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
@@ -580,7 +595,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
- Expect(32);
+ Expect(33);
if (StartOf(7)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
@@ -590,7 +605,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
formals.Add(new Formal(id, name, ty, true, isGhost));
}
}
- Expect(33);
+ Expect(34);
}
void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
@@ -678,22 +693,22 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
List<Type/*!*/>/*!*/ gt;
switch (la.kind) {
- case 34: {
+ case 35: {
Get();
tok = t;
break;
}
- case 35: {
+ case 36: {
Get();
tok = t; ty = new NatType();
break;
}
- case 36: {
+ case 37: {
Get();
tok = t; ty = new IntType();
break;
}
- case 37: {
+ case 38: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -704,7 +719,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
break;
}
- case 38: {
+ case 39: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -715,17 +730,17 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
break;
}
- case 1: case 3: case 39: {
+ case 1: case 3: case 40: {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(109); break;
+ default: SynErr(110); break;
}
}
void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
- Expect(32);
+ Expect(33);
if (la.kind == 1 || la.kind == 11) {
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
@@ -735,7 +750,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
}
}
- Expect(33);
+ Expect(34);
}
void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
@@ -743,7 +758,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false;
- if (la.kind == 27) {
+ if (la.kind == 28) {
Get();
if (StartOf(8)) {
FrameExpression(out fe);
@@ -755,27 +770,27 @@ List<Expression/*!*/>/*!*/ decreases) {
}
}
Expect(17);
- } else if (la.kind == 28 || la.kind == 29 || la.kind == 30) {
- if (la.kind == 28) {
+ } else if (la.kind == 29 || la.kind == 30 || la.kind == 31) {
+ if (la.kind == 29) {
Get();
isFree = true;
}
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
Expression(out e);
Expect(17);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (la.kind == 30) {
+ } else if (la.kind == 31) {
Get();
Expression(out e);
Expect(17);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(110);
- } else if (la.kind == 31) {
+ } else SynErr(111);
+ } else if (la.kind == 32) {
Get();
Expressions(decreases);
Expect(17);
- } else SynErr(111);
+ } else SynErr(112);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -795,7 +810,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void FrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
Expression(out e);
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
Ident(out id);
fieldName = id.val;
@@ -832,7 +847,7 @@ List<Expression/*!*/>/*!*/ decreases) {
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type/*!*/>/*!*/ gt;
- if (la.kind == 39) {
+ if (la.kind == 40) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 3) {
@@ -855,18 +870,18 @@ List<Expression/*!*/>/*!*/ decreases) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(112);
+ } else SynErr(113);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
Expression(out e);
Expect(17);
reqs.Add(e);
- } else if (la.kind == 41) {
+ } else if (la.kind == 42) {
Get();
if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
@@ -878,16 +893,16 @@ List<Expression/*!*/>/*!*/ decreases) {
}
}
Expect(17);
- } else if (la.kind == 30) {
+ } else if (la.kind == 31) {
Get();
Expression(out e);
Expect(17);
ens.Add(e);
- } else if (la.kind == 31) {
+ } else if (la.kind == 32) {
Get();
Expressions(decreases);
Expect(17);
- } else SynErr(113);
+ } else SynErr(114);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -901,23 +916,23 @@ List<Expression/*!*/>/*!*/ decreases) {
void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 42) {
+ if (la.kind == 43) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(114);
+ } else SynErr(115);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 42) {
+ if (la.kind == 43) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(8)) {
Expression(out e);
- } else SynErr(115);
+ } else SynErr(116);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -938,23 +953,23 @@ List<Expression/*!*/>/*!*/ decreases) {
BlockStmt(out s, out bodyStart, out bodyEnd);
break;
}
- case 63: {
+ case 64: {
AssertStmt(out s);
break;
}
- case 64: {
+ case 65: {
AssumeStmt(out s);
break;
}
- case 65: {
+ case 66: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 16: case 32: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
+ case 1: case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
UpdateStmt(out s);
break;
}
- case 53: {
+ case 54: {
HavocStmt(out s);
break;
}
@@ -962,23 +977,23 @@ List<Expression/*!*/>/*!*/ decreases) {
VarDeclStatement(out s);
break;
}
- case 54: {
+ case 55: {
IfStmt(out s);
break;
}
- case 58: {
+ case 59: {
WhileStmt(out s);
break;
}
- case 60: {
+ case 61: {
MatchStmt(out s);
break;
}
- case 61: {
+ case 62: {
ForeachStmt(out s);
break;
}
- case 44: {
+ case 45: {
Get();
x = t;
Ident(out id);
@@ -987,36 +1002,36 @@ List<Expression/*!*/>/*!*/ decreases) {
s.Labels = new LabelNode(x, id.val, s.Labels);
break;
}
- case 45: {
+ case 46: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
Ident(out id);
label = id.val;
- } else if (la.kind == 17 || la.kind == 45) {
- while (la.kind == 45) {
+ } else if (la.kind == 17 || la.kind == 46) {
+ while (la.kind == 46) {
Get();
breakCount++;
}
- } else SynErr(116);
+ } else SynErr(117);
Expect(17);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
}
- case 46: {
+ case 47: {
Get();
x = t;
Expect(17);
s = new ReturnStmt(x);
break;
}
- default: SynErr(117); break;
+ default: SynErr(118); break;
}
}
void AssertStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(63);
+ Expect(64);
x = t;
Expression(out e);
Expect(17);
@@ -1025,7 +1040,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void AssumeStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(64);
+ Expect(65);
x = t;
Expression(out e);
Expect(17);
@@ -1036,7 +1051,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(65);
+ Expect(66);
x = t;
AttributeArg(out arg);
args.Add(arg);
@@ -1061,14 +1076,14 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 17) {
Get();
rhss.Add(new ExprRhs(e));
- } else if (la.kind == 19 || la.kind == 47) {
+ } else if (la.kind == 19 || la.kind == 48) {
lhss.Add(e); lhs0 = e;
while (la.kind == 19) {
Get();
Lhs(out e);
lhss.Add(e);
}
- Expect(47);
+ Expect(48);
x = t;
Rhs(out r, lhs0);
rhss.Add(r);
@@ -1081,13 +1096,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 22) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(118);
+ } else SynErr(119);
s = new UpdateStmt(x, lhss, rhss);
}
void HavocStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs;
- Expect(53);
+ Expect(54);
x = t;
Lhs(out lhs);
Expect(17);
@@ -1114,7 +1129,7 @@ List<Expression/*!*/>/*!*/ decreases) {
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 47) {
+ if (la.kind == 48) {
Get();
assignTok = t; lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
Rhs(out r, lhs0);
@@ -1150,26 +1165,26 @@ List<Expression/*!*/>/*!*/ decreases) {
List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(54);
+ Expect(55);
x = t;
- if (la.kind == 32) {
+ if (la.kind == 33) {
Guard(out guard);
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
- if (la.kind == 54) {
+ if (la.kind == 55) {
IfStmt(out s);
els = s;
} else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(119);
+ } else SynErr(120);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(120);
+ } else SynErr(121);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1182,9 +1197,9 @@ List<Expression/*!*/>/*!*/ decreases) {
List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(58);
+ Expect(59);
x = t;
- if (la.kind == 32) {
+ if (la.kind == 33) {
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
LoopSpec(out invariants, out decreases);
@@ -1194,18 +1209,18 @@ List<Expression/*!*/>/*!*/ decreases) {
LoopSpec(out invariants, out decreases);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives);
- } else SynErr(121);
+ } else SynErr(122);
}
void MatchStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
- Expect(60);
+ Expect(61);
x = t;
Expression(out e);
Expect(7);
- while (la.kind == 56) {
+ while (la.kind == 57) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1222,27 +1237,27 @@ List<Expression/*!*/>/*!*/ decreases) {
List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();
Statement bodyAssign = null;
- Expect(61);
+ Expect(62);
x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
- Expect(32);
+ Expect(33);
Ident(out boundVar);
if (la.kind == 22) {
Get();
Type(out ty);
}
- Expect(62);
+ Expect(63);
Expression(out collection);
if (la.kind == 16) {
Get();
Expression(out range);
}
- Expect(33);
+ Expect(34);
Expect(7);
- while (la.kind == 63 || la.kind == 64) {
- if (la.kind == 63) {
+ while (la.kind == 64 || la.kind == 65) {
+ if (la.kind == 64) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1253,10 +1268,10 @@ List<Expression/*!*/>/*!*/ decreases) {
if (StartOf(12)) {
UpdateStmt(out s);
bodyAssign = s;
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
HavocStmt(out s);
bodyAssign = s;
- } else SynErr(122);
+ } else SynErr(123);
Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1271,16 +1286,16 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 49 || la.kind == 51) {
+ while (la.kind == 50 || la.kind == 52) {
Suffix(ref e);
}
} else if (StartOf(13)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 49 || la.kind == 51) {
+ while (la.kind == 50 || la.kind == 52) {
Suffix(ref e);
}
- } else SynErr(123);
+ } else SynErr(124);
}
void Rhs(out DeterminedAssignmentRhs r, Expression receiverForInitCall) {
@@ -1291,27 +1306,27 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Expression> args;
r = null; // to please compiler
- if (la.kind == 48) {
+ if (la.kind == 49) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 49 || la.kind == 51) {
- if (la.kind == 49) {
+ if (la.kind == 50 || la.kind == 52) {
+ if (la.kind == 50) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(50);
+ Expect(51);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
} else {
Get();
Ident(out x);
- Expect(32);
+ Expect(33);
args = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(args);
}
- Expect(33);
+ Expect(34);
initCall = new CallStmt(x, new List<IdentifierExpr>(),
receiverForInitCall, x.val, args);
}
@@ -1322,7 +1337,7 @@ List<Expression/*!*/>/*!*/ decreases) {
r = new TypeRhs(newToken, ty, initCall);
}
- } else if (la.kind == 52) {
+ } else if (la.kind == 53) {
Get();
x = t;
Expression(out e);
@@ -1330,20 +1345,20 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(124);
+ } else SynErr(125);
}
void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
- Expect(32);
- if (la.kind == 42) {
+ Expect(33);
+ if (la.kind == 43) {
Get();
e = null;
} else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(125);
- Expect(33);
+ } else SynErr(126);
+ Expect(34);
}
void AlternativeBlock(out List<GuardedAlternative> alternatives) {
@@ -1353,11 +1368,11 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Statement> body;
Expect(7);
- while (la.kind == 56) {
+ while (la.kind == 57) {
Get();
x = t;
Expression(out e);
- Expect(57);
+ Expect(58);
body = new List<Statement>();
while (StartOf(9)) {
Stmt(body);
@@ -1372,14 +1387,14 @@ List<Expression/*!*/>/*!*/ decreases) {
invariants = new List<MaybeFreeExpression/*!*/>();
decreases = new List<Expression/*!*/>();
- while (la.kind == 28 || la.kind == 31 || la.kind == 59) {
- if (la.kind == 28 || la.kind == 59) {
+ while (la.kind == 29 || la.kind == 32 || la.kind == 60) {
+ if (la.kind == 29 || la.kind == 60) {
isFree = false;
- if (la.kind == 28) {
+ if (la.kind == 29) {
Get();
isFree = true;
}
- Expect(59);
+ Expect(60);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(17);
@@ -1403,10 +1418,10 @@ List<Expression/*!*/>/*!*/ decreases) {
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(56);
+ Expect(57);
x = t;
Ident(out id);
- if (la.kind == 32) {
+ if (la.kind == 33) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
@@ -1415,9 +1430,9 @@ List<Expression/*!*/>/*!*/ decreases) {
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
}
- Expect(33);
+ Expect(34);
}
- Expect(57);
+ Expect(58);
while (StartOf(9)) {
Stmt(body);
}
@@ -1432,13 +1447,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(126);
+ } else SynErr(127);
}
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);
@@ -1449,7 +1464,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);
@@ -1458,23 +1473,23 @@ 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(127);
+ } else SynErr(128);
}
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 == 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);
@@ -1485,7 +1500,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);
@@ -1496,11 +1511,11 @@ 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(128);
+ } else SynErr(129);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1579,25 +1594,25 @@ 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(129);
+ } else SynErr(130);
}
void OrOp() {
- if (la.kind == 72) {
+ if (la.kind == 73) {
Get();
- } else if (la.kind == 73) {
+ } else if (la.kind == 74) {
Get();
- } else SynErr(130);
+ } else SynErr(131);
}
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);
@@ -1607,7 +1622,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;
@@ -1622,59 +1637,59 @@ 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 62: {
+ case 63: {
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;
}
- default: SynErr(131); break;
+ default: SynErr(132); 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 == 85 || la.kind == 86) {
+ while (la.kind == 43 || la.kind == 86 || la.kind == 87) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1683,78 +1698,78 @@ 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(132);
+ } else SynErr(133);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 84: {
+ case 85: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 87: case 88: {
+ case 88: case 89: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 37: case 54: case 60: case 98: case 99: case 100: case 101: {
+ case 38: case 55: case 61: case 99: case 100: case 101: case 102: {
EndlessExpression(out e);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 49 || la.kind == 51) {
+ while (la.kind == 50 || la.kind == 52) {
Suffix(ref e);
}
break;
}
- case 7: case 49: {
+ case 7: case 50: {
DisplayExpr(out e);
break;
}
- case 2: case 16: case 32: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
+ case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
ConstAtomExpression(out e);
- while (la.kind == 49 || la.kind == 51) {
+ while (la.kind == 50 || la.kind == 52) {
Suffix(ref e);
}
break;
}
- default: SynErr(133); break;
+ default: SynErr(134); break;
}
}
void MulOp(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 == 42) {
+ if (la.kind == 43) {
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(134);
+ } else SynErr(135);
}
void NegOp() {
- if (la.kind == 87) {
+ if (la.kind == 88) {
Get();
- } else if (la.kind == 88) {
+ } else if (la.kind == 89) {
Get();
- } else SynErr(135);
+ } else SynErr(136);
}
void EndlessExpression(out Expression e) {
@@ -1762,22 +1777,22 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression e0, e1;
e = dummyExpr;
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
x = t;
Expression(out e);
- Expect(96);
+ Expect(97);
Expression(out e0);
- Expect(55);
+ Expect(56);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
- } else if (la.kind == 60) {
+ } else if (la.kind == 61) {
MatchExpression(out e);
} else if (StartOf(16)) {
QuantifierGuts(out e);
- } else if (la.kind == 37) {
+ } else if (la.kind == 38) {
ComprehensionExpr(out e);
- } else SynErr(136);
+ } else SynErr(137);
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -1787,18 +1802,18 @@ List<Expression/*!*/>/*!*/ decreases) {
Ident(out id);
idents.Add(id);
- while (la.kind == 51) {
+ while (la.kind == 52) {
Get();
Ident(out id);
idents.Add(id);
}
- if (la.kind == 32) {
+ if (la.kind == 33) {
Get();
openParen = t; args = new List<Expression>();
if (StartOf(8)) {
Expressions(args);
}
- Expect(33);
+ Expect(34);
}
e = new IdentifierSequence(idents, openParen, args);
}
@@ -1809,37 +1824,37 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 51) {
+ if (la.kind == 52) {
Get();
Ident(out id);
- if (la.kind == 32) {
+ if (la.kind == 33) {
Get();
args = new List<Expression/*!*/>(); func = true;
if (StartOf(8)) {
Expressions(args);
}
- Expect(33);
+ Expect(34);
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (la.kind == 49) {
+ } else if (la.kind == 50) {
Get();
x = t;
if (StartOf(8)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 97) {
+ if (la.kind == 98) {
Get();
anyDots = true;
if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 47) {
+ } else if (la.kind == 48) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 19 || la.kind == 50) {
+ } else if (la.kind == 19 || la.kind == 51) {
while (la.kind == 19) {
Get();
Expression(out ee);
@@ -1850,12 +1865,12 @@ List<Expression/*!*/>/*!*/ decreases) {
multipleIndices.Add(ee);
}
- } else SynErr(137);
- } else if (la.kind == 97) {
+ } else SynErr(138);
+ } else if (la.kind == 98) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(138);
+ } else SynErr(139);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -1878,8 +1893,8 @@ List<Expression/*!*/>/*!*/ decreases) {
}
}
- Expect(50);
- } else SynErr(139);
+ Expect(51);
+ } else SynErr(140);
}
void DisplayExpr(out Expression e) {
@@ -1895,15 +1910,15 @@ List<Expression/*!*/>/*!*/ decreases) {
}
e = new SetDisplayExpr(x, elements);
Expect(8);
- } else if (la.kind == 49) {
+ } else if (la.kind == 50) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(50);
- } else SynErr(140);
+ Expect(51);
+ } else SynErr(141);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -1912,17 +1927,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;
@@ -1932,35 +1947,35 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new LiteralExpr(t, n);
break;
}
- case 92: {
+ case 93: {
Get();
e = new ThisExpr(t);
break;
}
- case 93: {
+ case 94: {
Get();
x = t;
- Expect(32);
- Expression(out e);
Expect(33);
+ Expression(out e);
+ Expect(34);
e = new FreshExpr(x, e);
break;
}
- case 94: {
+ case 95: {
Get();
x = t;
- Expect(32);
- Expression(out e);
Expect(33);
+ Expression(out e);
+ Expect(34);
e = new AllocatedExpr(x, e);
break;
}
- case 95: {
+ case 96: {
Get();
x = t;
- Expect(32);
- Expression(out e);
Expect(33);
+ Expression(out e);
+ Expect(34);
e = new OldExpr(x, e);
break;
}
@@ -1972,15 +1987,15 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(16);
break;
}
- case 32: {
+ case 33: {
Get();
x = t;
Expression(out e);
e = new ParensExpression(x, e);
- Expect(33);
+ Expect(34);
break;
}
- default: SynErr(141); break;
+ default: SynErr(142); break;
}
}
@@ -1999,10 +2014,10 @@ List<Expression/*!*/>/*!*/ decreases) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(60);
+ Expect(61);
x = t;
Expression(out e);
- while (la.kind == 56) {
+ while (la.kind == 57) {
CaseExpression(out c);
cases.Add(c);
}
@@ -2019,13 +2034,13 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression range = null;
Expression/*!*/ body;
- if (la.kind == 98 || la.kind == 99) {
+ if (la.kind == 99 || la.kind == 100) {
Forall();
x = t; univ = true;
- } else if (la.kind == 100 || la.kind == 101) {
+ } else if (la.kind == 101 || la.kind == 102) {
Exists();
x = t;
- } else SynErr(142);
+ } else SynErr(143);
IdentTypeOptional(out bv);
bvars.Add(bv);
while (la.kind == 19) {
@@ -2058,7 +2073,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression/*!*/ range;
Expression body = null;
- Expect(37);
+ Expect(38);
x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -2069,7 +2084,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(16);
Expression(out range);
- if (la.kind == 102 || la.kind == 103) {
+ if (la.kind == 103 || la.kind == 104) {
QSep();
Expression(out body);
}
@@ -2083,10 +2098,10 @@ List<Expression/*!*/>/*!*/ decreases) {
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
Expression/*!*/ body;
- Expect(56);
+ Expect(57);
x = t;
Ident(out id);
- if (la.kind == 32) {
+ if (la.kind == 33) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
@@ -2095,27 +2110,27 @@ List<Expression/*!*/>/*!*/ decreases) {
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
}
- Expect(33);
+ Expect(34);
}
- Expect(57);
+ Expect(58);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
void Forall() {
- if (la.kind == 98) {
+ if (la.kind == 99) {
Get();
- } else if (la.kind == 99) {
+ } else if (la.kind == 100) {
Get();
- } else SynErr(143);
+ } else SynErr(144);
}
void Exists() {
- if (la.kind == 100) {
+ if (la.kind == 101) {
Get();
- } else if (la.kind == 101) {
+ } else if (la.kind == 102) {
Get();
- } else SynErr(144);
+ } else SynErr(145);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2128,16 +2143,16 @@ List<Expression/*!*/>/*!*/ decreases) {
es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(145);
+ } else SynErr(146);
Expect(8);
}
void QSep() {
- if (la.kind == 102) {
+ if (la.kind == 103) {
Get();
- } else if (la.kind == 103) {
+ } else if (la.kind == 104) {
Get();
- } else SynErr(146);
+ } else SynErr(147);
}
void AttributeBody(ref Attributes attrs) {
@@ -2164,32 +2179,32 @@ List<Expression/*!*/>/*!*/ decreases) {
public void Parse() {
la = new Token();
- la.val = "";
+ la.val = "";
Get();
Dafny();
- Expect(0);
+ Expect(0);
}
-
+
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,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,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,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,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,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,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,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, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,T,T,x, x,x,T,x, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, 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,T,x, x,x,x,x, x,T,x,x, x,x,T,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,T, x,x,T,T, T,T,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,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,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,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, 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,T,x,x, x,x,T,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,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,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,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,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,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,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,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, 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,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, 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, 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, T,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,T,T,T, x,x,x,x, x,x,T,T, x,x,x,T, x,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, T,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,T, x,x,x,x, x,x,T,x, x,x,x,T, 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, T,x,x,T, T,T,T,x, x,x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, 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,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
+ {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,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,x,T, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, T,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,T,x, x,x,x,T, 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, T,x,x,T, T,T,T,x, x,x,x}
};
} // end Parser
@@ -2198,18 +2213,20 @@ List<Expression/*!*/>/*!*/ decreases) {
public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
public void SynErr(string filename, int line, int col, int n) {
- SynErr(filename, line, col, GetSyntaxErrorString(n));
- }
- public virtual void SynErr(string filename, int line, int col, string msg) {
- Contract.Requires(msg != null);
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+
+ public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
- }
- string GetSyntaxErrorString(int n) {
+ }
+
+ string GetSyntaxErrorString(int n) {
string s;
switch (n) {
case 0: s = "EOF expected"; break;
@@ -2238,131 +2255,132 @@ public class Errors {
case 23: s = "\"<\" expected"; break;
case 24: s = "\">\" expected"; break;
case 25: s = "\"method\" expected"; break;
- case 26: s = "\"returns\" expected"; break;
- case 27: s = "\"modifies\" expected"; break;
- case 28: s = "\"free\" expected"; break;
- case 29: s = "\"requires\" expected"; break;
- case 30: s = "\"ensures\" expected"; break;
- case 31: s = "\"decreases\" expected"; break;
- case 32: s = "\"(\" expected"; break;
- case 33: s = "\")\" expected"; break;
- case 34: s = "\"bool\" expected"; break;
- case 35: s = "\"nat\" expected"; break;
- case 36: s = "\"int\" expected"; break;
- case 37: s = "\"set\" expected"; break;
- case 38: s = "\"seq\" expected"; break;
- case 39: s = "\"object\" expected"; break;
- case 40: s = "\"function\" expected"; break;
- case 41: s = "\"reads\" expected"; break;
- case 42: s = "\"*\" expected"; break;
- case 43: s = "\"`\" expected"; break;
- case 44: s = "\"label\" expected"; break;
- case 45: s = "\"break\" expected"; break;
- case 46: s = "\"return\" expected"; break;
- case 47: s = "\":=\" expected"; break;
- case 48: s = "\"new\" expected"; break;
- case 49: s = "\"[\" expected"; break;
- case 50: 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 = "\"case\" expected"; break;
- case 57: s = "\"=>\" expected"; break;
- case 58: s = "\"while\" expected"; break;
- case 59: s = "\"invariant\" expected"; break;
- case 60: s = "\"match\" 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 = "\"print\" 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 = "\"this\" expected"; break;
- case 93: s = "\"fresh\" expected"; break;
- case 94: s = "\"allocated\" expected"; break;
- case 95: s = "\"old\" expected"; break;
- case 96: s = "\"then\" expected"; break;
- case 97: s = "\"..\" expected"; break;
- case 98: s = "\"forall\" expected"; break;
- case 99: s = "\"\\u2200\" expected"; break;
- case 100: s = "\"exists\" expected"; break;
- case 101: s = "\"\\u2203\" expected"; break;
- case 102: s = "\"::\" expected"; break;
- case 103: s = "\"\\u2022\" expected"; break;
- case 104: s = "??? expected"; break;
- case 105: s = "invalid ClassMemberDecl"; break;
- case 106: s = "invalid FunctionDecl"; break;
- case 107: s = "invalid MethodDecl"; break;
+ case 26: s = "\"constructor\" expected"; break;
+ case 27: s = "\"returns\" expected"; break;
+ case 28: s = "\"modifies\" expected"; break;
+ case 29: s = "\"free\" expected"; break;
+ case 30: s = "\"requires\" expected"; break;
+ case 31: s = "\"ensures\" expected"; break;
+ case 32: s = "\"decreases\" expected"; break;
+ case 33: s = "\"(\" expected"; break;
+ case 34: s = "\")\" expected"; break;
+ case 35: s = "\"bool\" expected"; break;
+ case 36: s = "\"nat\" expected"; break;
+ case 37: s = "\"int\" expected"; break;
+ case 38: s = "\"set\" expected"; break;
+ case 39: s = "\"seq\" expected"; break;
+ case 40: s = "\"object\" expected"; break;
+ case 41: s = "\"function\" expected"; break;
+ case 42: s = "\"reads\" expected"; break;
+ case 43: s = "\"*\" expected"; break;
+ case 44: s = "\"`\" expected"; break;
+ case 45: s = "\"label\" expected"; break;
+ case 46: s = "\"break\" expected"; break;
+ case 47: s = "\"return\" expected"; break;
+ case 48: s = "\":=\" expected"; break;
+ case 49: s = "\"new\" expected"; break;
+ case 50: s = "\"[\" expected"; break;
+ case 51: s = "\"]\" expected"; break;
+ case 52: s = "\".\" expected"; break;
+ case 53: s = "\"choose\" expected"; break;
+ case 54: s = "\"havoc\" expected"; break;
+ case 55: s = "\"if\" expected"; break;
+ case 56: s = "\"else\" expected"; break;
+ case 57: s = "\"case\" expected"; break;
+ case 58: s = "\"=>\" expected"; break;
+ case 59: s = "\"while\" expected"; break;
+ case 60: s = "\"invariant\" expected"; break;
+ case 61: s = "\"match\" 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 = "\"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 ClassMemberDecl"; break;
+ case 107: s = "invalid FunctionDecl"; break;
case 108: s = "invalid MethodDecl"; break;
- case 109: s = "invalid TypeAndToken"; break;
- case 110: s = "invalid MethodSpec"; break;
+ case 109: s = "invalid MethodDecl"; break;
+ case 110: s = "invalid TypeAndToken"; break;
case 111: s = "invalid MethodSpec"; break;
- case 112: s = "invalid ReferenceType"; break;
- case 113: s = "invalid FunctionSpec"; break;
- case 114: s = "invalid PossiblyWildFrameExpression"; break;
- case 115: s = "invalid PossiblyWildExpression"; break;
- case 116: s = "invalid OneStmt"; break;
+ case 112: s = "invalid MethodSpec"; break;
+ case 113: s = "invalid ReferenceType"; break;
+ case 114: s = "invalid FunctionSpec"; break;
+ case 115: s = "invalid PossiblyWildFrameExpression"; break;
+ case 116: s = "invalid PossiblyWildExpression"; break;
case 117: s = "invalid OneStmt"; break;
- case 118: s = "invalid UpdateStmt"; break;
- case 119: s = "invalid IfStmt"; break;
+ case 118: s = "invalid OneStmt"; break;
+ case 119: s = "invalid UpdateStmt"; break;
case 120: s = "invalid IfStmt"; break;
- case 121: s = "invalid WhileStmt"; break;
- case 122: s = "invalid ForeachStmt"; break;
- case 123: s = "invalid Lhs"; break;
- case 124: s = "invalid Rhs"; break;
- case 125: s = "invalid Guard"; break;
- case 126: s = "invalid AttributeArg"; break;
- case 127: s = "invalid EquivOp"; break;
- case 128: s = "invalid ImpliesOp"; break;
- case 129: s = "invalid AndOp"; break;
- case 130: s = "invalid OrOp"; break;
- case 131: s = "invalid RelOp"; break;
- case 132: s = "invalid AddOp"; break;
- case 133: s = "invalid UnaryExpression"; break;
- case 134: s = "invalid MulOp"; break;
- case 135: s = "invalid NegOp"; break;
- case 136: s = "invalid EndlessExpression"; break;
- case 137: s = "invalid Suffix"; break;
+ case 121: s = "invalid IfStmt"; break;
+ case 122: s = "invalid WhileStmt"; break;
+ case 123: s = "invalid ForeachStmt"; break;
+ case 124: s = "invalid Lhs"; break;
+ case 125: s = "invalid Rhs"; break;
+ case 126: s = "invalid Guard"; break;
+ case 127: s = "invalid AttributeArg"; break;
+ case 128: s = "invalid EquivOp"; break;
+ case 129: s = "invalid ImpliesOp"; break;
+ case 130: s = "invalid AndOp"; break;
+ case 131: s = "invalid OrOp"; break;
+ case 132: s = "invalid RelOp"; break;
+ case 133: s = "invalid AddOp"; break;
+ case 134: s = "invalid UnaryExpression"; break;
+ case 135: s = "invalid MulOp"; break;
+ case 136: s = "invalid NegOp"; break;
+ case 137: s = "invalid EndlessExpression"; break;
case 138: s = "invalid Suffix"; break;
case 139: s = "invalid Suffix"; break;
- case 140: s = "invalid DisplayExpr"; break;
- case 141: s = "invalid ConstAtomExpression"; break;
- case 142: s = "invalid QuantifierGuts"; break;
- case 143: s = "invalid Forall"; break;
- case 144: s = "invalid Exists"; break;
- case 145: s = "invalid AttributeOrTrigger"; break;
- case 146: s = "invalid QSep"; break;
+ case 140: s = "invalid Suffix"; break;
+ case 141: s = "invalid DisplayExpr"; break;
+ case 142: s = "invalid ConstAtomExpression"; break;
+ case 143: s = "invalid QuantifierGuts"; break;
+ case 144: s = "invalid Forall"; break;
+ case 145: s = "invalid Exists"; break;
+ case 146: s = "invalid AttributeOrTrigger"; break;
+ case 147: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2370,8 +2388,9 @@ public class Errors {
Contract.Requires(msg != null);
SemErr(tok.filename, tok.line, tok.col, msg);
}
+
public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 6a84a361..4c8f2063 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -262,7 +262,7 @@ namespace Microsoft.Dafny {
public void PrintMethod(Method method, int indent) {
Contract.Requires(method != null);
Indent(indent);
- string k = method is MethodRefinement ? "refines" : "method";
+ string k = method is MethodRefinement ? "refines" : method is Constructor ? "constructor" : "method";
if (method.IsStatic) { k = "static " + k; }
if (method.IsGhost) { k = "ghost " + k; }
PrintClassMethodHelper(k, method.Attributes, method.Name, method.TypeArgs);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index b1bbe6c4..69a1e9c6 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -186,13 +186,18 @@ namespace Microsoft.Dafny {
Dictionary<string, MemberDecl> members = new Dictionary<string, MemberDecl>();
classMembers.Add(cl, members);
+ bool hasConstructor = false;
foreach (MemberDecl m in cl.Members) {
if (members.ContainsKey(m.Name)) {
Error(m, "Duplicate member name: {0}", m.Name);
} else {
members.Add(m.Name, m);
}
+ if (m is Constructor) {
+ hasConstructor = true;
+ }
}
+ cl.HasConstructor = hasConstructor;
} else {
DatatypeDecl dt = (DatatypeDecl)d;
@@ -1716,6 +1721,9 @@ namespace Microsoft.Dafny {
} else {
callee = (Method)member;
s.Method = callee;
+ if (!isInitCall && callee is Constructor) {
+ Error(s, "a constructor is only allowed to be called when an object is being allocated");
+ }
s.IsGhost = callee.IsGhost;
if (specContextOnly && !callee.IsGhost) {
Error(s, "only ghost methods can be called from this context");
@@ -1858,8 +1866,21 @@ namespace Microsoft.Dafny {
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, specContextOnly, method, rr.EType);
+ } else {
+ bool callsConstructor = false;
+ if (rr.InitCall != null) {
+ ResolveCallStmt(rr.InitCall, specContextOnly, method, rr.EType);
+ if (rr.InitCall.Method is Constructor) {
+ callsConstructor = true;
+ }
+ }
+ if (!callsConstructor && rr.EType is UserDefinedType) {
+ var udt = (UserDefinedType)rr.EType;
+ var cl = (ClassDecl)udt.ResolvedClass; // cast is guarantted by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test
+ if (cl.HasConstructor) {
+ Error(stmt, "when allocating an object of type '{0}', one of its constructor methods must be called", cl.Name);
+ }
+ }
}
rr.Type = rr.EType;
} else {
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index d45bbbbe..f642178b 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
// a) whole stream in buffer
// b) part of stream in buffer
// 2) non seekable stream (network, console)
-
+
public const int EOF = 65535 + 1; // char.MaxValue + 1;
const int MIN_BUFFER_LENGTH = 1024; // 1KB
const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,15 +31,17 @@ public class Buffer {
Stream/*!*/ stream; // input stream (seekable)
bool isUserStream; // was the stream opened by the user?
-[ContractInvariantMethod]
-void ObjectInvariant(){
- Contract.Invariant(buf != null);
- Contract.Invariant(stream != null);}
- [NotDelayed]
- public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
+ [ContractInvariantMethod]
+ void ObjectInvariant(){
+ Contract.Invariant(buf != null);
+ Contract.Invariant(stream != null);
+ }
+
+// [NotDelayed]
+ public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
Contract.Requires(s != null);
stream = s; this.isUserStream = isUserStream;
-
+
int fl, bl;
if (s.CanSeek) {
fl = (int) s.Length;
@@ -51,12 +53,12 @@ void ObjectInvariant(){
buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
fileLen = fl; bufLen = bl;
-
+
if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
if (bufLen == fileLen && s.CanSeek) Close();
}
-
+
protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
Contract.Requires(b != null);
buf = b.buf;
@@ -73,14 +75,14 @@ void ObjectInvariant(){
}
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -100,7 +102,7 @@ void ObjectInvariant(){
Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -139,7 +141,7 @@ void ObjectInvariant(){
}
}
}
-
+
// Read the next chunk of bytes from the stream, increases the buffer
// if needed and updates the fields fileLen and bufLen.
// Returns the number of bytes read.
@@ -209,23 +211,24 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 104;
- const int noSym = 104;
-
-
-[ContractInvariantMethod]
-void objectInvariant(){
- Contract.Invariant(buffer!=null);
- Contract.Invariant(t != null);
- Contract.Invariant(start != null);
- Contract.Invariant(tokens != null);
- Contract.Invariant(pt != null);
- Contract.Invariant(tval != null);
- Contract.Invariant(Filename != null);
- Contract.Invariant(errorHandler != null);
-}
+ const int maxT = 105;
+ const int noSym = 105;
+
+
+ [ContractInvariantMethod]
+ void objectInvariant(){
+ Contract.Invariant(buffer!=null);
+ Contract.Invariant(t != null);
+ Contract.Invariant(start != null);
+ Contract.Invariant(tokens != null);
+ Contract.Invariant(pt != null);
+ Contract.Invariant(tval != null);
+ Contract.Invariant(Filename != null);
+ Contract.Invariant(errorHandler != null);
+ }
+
public Buffer/*!*/ buffer; // scanner buffer
-
+
Token/*!*/ t; // current token
int ch; // current input character
int pos; // byte position of current character
@@ -236,13 +239,13 @@ void objectInvariant(){
Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy)
Token/*!*/ pt; // current peek token
-
+
char[]/*!*/ tval = new char[128]; // text of current token
int tlen; // length of current token
-
+
private string/*!*/ Filename;
private Errors/*!*/ errorHandler;
-
+
static Scanner() {
start = new Hashtable(128);
for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -290,9 +293,9 @@ void objectInvariant(){
start[Buffer.EOF] = -1;
}
-
- [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
+
+// [NotDelayed]
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -302,15 +305,14 @@ void objectInvariant(){
Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
Filename = fileName;
-
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
}
}
-
- [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
+
+// [NotDelayed]
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -319,10 +321,9 @@ void objectInvariant(){
buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
-
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -343,11 +344,11 @@ void objectInvariant(){
Contract.Ensures(Contract.Result<string>() != null);
int p = buffer.Pos;
int ch = buffer.Read();
- // replace isolated '\r' by '\n' in order to make
+ // replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
while (ch != EOL && ch != Buffer.EOF){
- ch = buffer.Read();
+ ch = buffer.Read();
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -358,7 +359,7 @@ void objectInvariant(){
}
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -366,9 +367,9 @@ void objectInvariant(){
// // eol handling uniform across Windows, Unix and Mac
// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
// if (ch == EOL) { line++; col = 0; }
-
+
while (true) {
- pos = buffer.Pos;
+ pos = buffer.Pos;
ch = buffer.Read(); col++;
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
@@ -418,7 +419,7 @@ void objectInvariant(){
return;
}
-
+
}
}
@@ -498,47 +499,48 @@ void objectInvariant(){
case "replaces": t.kind = 20; break;
case "by": t.kind = 21; break;
case "method": t.kind = 25; break;
- case "returns": t.kind = 26; break;
- case "modifies": t.kind = 27; break;
- case "free": t.kind = 28; break;
- case "requires": t.kind = 29; break;
- case "ensures": t.kind = 30; break;
- case "decreases": t.kind = 31; break;
- case "bool": t.kind = 34; break;
- case "nat": t.kind = 35; break;
- case "int": t.kind = 36; break;
- case "set": t.kind = 37; break;
- case "seq": t.kind = 38; break;
- case "object": t.kind = 39; break;
- case "function": t.kind = 40; break;
- case "reads": t.kind = 41; break;
- case "label": t.kind = 44; break;
- case "break": t.kind = 45; break;
- case "return": t.kind = 46; break;
- case "new": t.kind = 48; 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 "case": t.kind = 56; break;
- case "while": t.kind = 58; break;
- case "invariant": t.kind = 59; break;
- case "match": 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 "print": t.kind = 65; break;
- case "false": t.kind = 89; break;
- case "true": t.kind = 90; break;
- case "null": t.kind = 91; break;
- case "this": t.kind = 92; break;
- case "fresh": t.kind = 93; break;
- case "allocated": t.kind = 94; break;
- case "old": t.kind = 95; break;
- case "then": t.kind = 96; break;
- case "forall": t.kind = 98; break;
- case "exists": t.kind = 100; break;
+ case "constructor": t.kind = 26; break;
+ case "returns": t.kind = 27; break;
+ case "modifies": t.kind = 28; break;
+ case "free": t.kind = 29; break;
+ case "requires": t.kind = 30; break;
+ case "ensures": t.kind = 31; break;
+ case "decreases": t.kind = 32; break;
+ case "bool": t.kind = 35; break;
+ case "nat": t.kind = 36; break;
+ case "int": t.kind = 37; break;
+ case "set": t.kind = 38; break;
+ case "seq": t.kind = 39; break;
+ case "object": t.kind = 40; break;
+ case "function": t.kind = 41; break;
+ case "reads": t.kind = 42; break;
+ case "label": t.kind = 45; break;
+ case "break": t.kind = 46; break;
+ case "return": t.kind = 47; break;
+ case "new": t.kind = 49; break;
+ case "choose": t.kind = 53; break;
+ case "havoc": t.kind = 54; break;
+ case "if": t.kind = 55; break;
+ case "else": t.kind = 56; break;
+ case "case": t.kind = 57; break;
+ case "while": t.kind = 59; break;
+ case "invariant": t.kind = 60; break;
+ case "match": 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 "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;
}
}
@@ -555,10 +557,13 @@ void objectInvariant(){
t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
+ if (start.ContainsKey(ch)) {
+ Contract.Assert(start[ch] != null);
+ state = (int) start[ch];
+ }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -645,80 +650,80 @@ void objectInvariant(){
case 20:
{t.kind = 19; break;}
case 21:
- {t.kind = 32; break;}
- case 22:
{t.kind = 33; break;}
+ case 22:
+ {t.kind = 34; break;}
case 23:
- {t.kind = 42; break;}
- case 24:
{t.kind = 43; break;}
+ case 24:
+ {t.kind = 44; break;}
case 25:
- {t.kind = 47; break;}
+ {t.kind = 48; break;}
case 26:
- {t.kind = 49; break;}
- case 27:
{t.kind = 50; break;}
+ case 27:
+ {t.kind = 51; break;}
case 28:
- {t.kind = 57; break;}
+ {t.kind = 58; break;}
case 29:
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 = 97; break;}
+ {t.kind = 98; break;}
case 53:
- {t.kind = 99; break;}
+ {t.kind = 100; break;}
case 54:
- {t.kind = 101; break;}
- case 55:
{t.kind = 102; break;}
- case 56:
+ case 55:
{t.kind = 103; break;}
+ case 56:
+ {t.kind = 104; break;}
case 57:
recEnd = pos; recKind = 15;
if (ch == '>') {AddCh(); goto case 28;}
@@ -742,36 +747,36 @@ void objectInvariant(){
if (ch == '=') {AddCh(); goto case 39;}
else {t.kind = 24; break;}
case 62:
- recEnd = pos; recKind = 51;
+ recEnd = pos; recKind = 52;
if (ch == '.') {AddCh(); goto case 52;}
- else {t.kind = 51; break;}
+ else {t.kind = 52; break;}
case 63:
- recEnd = pos; recKind = 87;
+ 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;}
+ else {t.kind = 88; break;}
case 64:
- recEnd = pos; recKind = 74;
+ recEnd = pos; recKind = 75;
if (ch == '>') {AddCh(); goto case 32;}
- else {t.kind = 74; break;}
+ else {t.kind = 75; 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;}
}
t.val = new String(tval, 0, tlen);
return t;
}
-
+
private void SetScannerBehindT() {
buffer.Pos = t.pos;
NextCh();
line = t.line; col = t.col;
for (int i = 0; i < tlen; i++) NextCh();
}
-
+
// get the next token (possibly a token already seen during peeking)
public Token/*!*/ Scan () {
Contract.Ensures(Contract.Result<Token>() != null);
@@ -792,7 +797,7 @@ void objectInvariant(){
}
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 05250fa8..0eab5c50 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -432,7 +432,10 @@ ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype construc
ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
ResolutionErrors.dfy(247,4): Error: label shadows an enclosing label
ResolutionErrors.dfy(252,2): Error: duplicate label
-38 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(278,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(279,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(281,4): Error: a constructor is only allowed to be called when an object is being allocated
+41 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index cacc34be..9e7ad3b2 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -253,3 +253,30 @@ method DuplicateLabels(n: int) {
x := x + 1;
label DuplicateLabel: x := x + 1;
}
+
+// --------------- constructors -------------------------------------
+
+class ClassWithConstructor {
+ var y: int;
+ method NotTheOne() { }
+ constructor InitA() { }
+ constructor InitB() modifies this; { y := 20; }
+}
+
+class ClassWithoutConstructor {
+ method Init() modifies this; { }
+}
+
+method ConstructorTests()
+{
+ var o := new object; // fine: does not have any constructors
+
+ o := new ClassWithoutConstructor; // fine: don't need to call anything particular method
+ o := new ClassWithoutConstructor.Init(); // this is also fine
+
+ var c := new ClassWithConstructor.InitA();
+ c := new ClassWithConstructor; // error: must call a constructor
+ c := new ClassWithConstructor.NotTheOne(); // error: must call a constructor, not an arbitrary method
+ c := new ClassWithConstructor.InitB();
+ c.InitB(); // error: not allowed to call constructors except during allocation
+}
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 818d7dc3..b69a568a 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -30,7 +30,7 @@
]\\)*" . font-lock-comment-face)
`(,(dafny-regexp-opt '(
- "class" "datatype" "function" "ghost" "var" "method" "unlimited"
+ "class" "datatype" "function" "ghost" "var" "method" "constructor" "unlimited"
"module" "imports" "static" "refines" "replaces" "by"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index a9353821..c620cc67 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -16,7 +16,7 @@ namespace Demo
StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");
this.MarkReservedWords( // NOTE: these keywords must also appear once more below
- "class", "ghost", "static", "var", "method", "datatype",
+ "class", "ghost", "static", "var", "method", "constructor", "datatype",
"assert", "assume", "new", "this", "object", "refines", "replaces", "by",
"unlimited", "module", "imports",
"call", "if", "then", "else", "while", "invariant",
@@ -287,6 +287,7 @@ namespace Demo
| "static"
| "var"
| "method"
+ | "constructor"
| "datatype"
| "assert"
| "assume"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index c37ea13c..654b5dcb 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -244,6 +244,7 @@ namespace DafnyLanguage
case "case":
case "choose":
case "class":
+ case "constructor":
case "datatype":
case "decreases":
case "else":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index fccd3918..b29c054e 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -8,7 +8,7 @@
morekeywords={class,datatype,bool,nat,int,object,set,seq,array,array2,array3,%
function,unlimited,
ghost,var,static,refines,replaces,by,
- method,returns,module,imports,in,
+ method,constructor,returns,module,imports,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
match,case,false,true,null,old,fresh,allocated,choose,this,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index 7727e1f6..fac7e6c7 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -5,7 +5,7 @@
syntax clear
syntax case match
-syntax keyword dafnyFunction function method
+syntax keyword dafnyFunction function method constructor
syntax keyword dafnyTypeDef class datatype
syntax keyword dafnyConditional if then else match case
syntax keyword dafnyRepeat foreach while
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 06:10:33 +0000