summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Dafny/Dafny.atg57
-rw-r--r--Dafny/Parser.cs474
-rw-r--r--Dafny/Scanner.cs111
3 files changed, 361 insertions, 281 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 2eaaca7f..7019a22b 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -191,6 +191,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
.)
+ SYNC
"class"
{ Attribute<ref attrs> }
Ident<out id>
@@ -234,6 +235,7 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
IToken bodyStart = Token.NoToken; // dummy assignment
.)
+ SYNC
"datatype"
{ Attribute<ref attrs> }
Ident<out id>
@@ -241,7 +243,7 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
"=" (. bodyStart = t; .)
DatatypeMemberDecl<ctors>
{ "|" DatatypeMemberDecl<ctors> }
- ";"
+ SYNC ";"
(. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
dt.BodyStartTok = bodyStart;
dt.BodyEndTok = t;
@@ -263,6 +265,7 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
.)
+ SYNC
"var"
(. if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -271,7 +274,7 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
{ "," IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
}
- ";"
+ SYNC ";"
.
CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
@@ -379,6 +382,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
+ SYNC
( "method"
| "constructor" (. if (allowConstructor) {
isConstructor = true;
@@ -423,16 +427,17 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
= (. 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;
.)
+ SYNC
( "modifies" [ FrameExpression<out fe> (. mod.Add(fe); .)
{ "," FrameExpression<out fe> (. mod.Add(fe); .)
}
- ] ";"
+ ] SYNC ";"
| [ "free" (. isFree = true; .)
]
- ( "requires" Expression<out e> ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
- | "ensures" Expression<out e> ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
+ ( "requires" Expression<out e> SYNC ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
+ | "ensures" Expression<out e> SYNC ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
)
- | "decreases" DecreasesList<decreases, false> ";"
+ | "decreases" DecreasesList<decreases, false> SYNC ";"
)
.
Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
@@ -555,13 +560,15 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
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; .)
- ( "requires" Expression<out e> ";" (. reqs.Add(e); .)
+ (
+ SYNC
+ "requires" Expression<out e> SYNC ";" (. reqs.Add(e); .)
| "reads" [ PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
{ "," PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
}
- ] ";"
- | "ensures" Expression<out e> ";" (. ens.Add(e); .)
- | "decreases" DecreasesList<decreases, false> ";"
+ ] SYNC ";"
+ | "ensures" Expression<out e> SYNC ";" (. ens.Add(e); .)
+ | "decreases" DecreasesList<decreases, false> SYNC ";"
)
.
PossiblyWildExpression<out Expression/*!*/ e>
@@ -622,6 +629,7 @@ OneStmt<out Statement/*!*/ s>
int breakCount;
.)
/* This list does not contain BlockStmt, see comment above in Stmt production. */
+ SYNC
( BlockStmt<out s, out bodyStart, out bodyEnd>
| AssertStmt<out s>
| AssumeStmt<out s>
@@ -640,6 +648,7 @@ OneStmt<out Statement/*!*/ s>
| { "break" (. breakCount++; .)
}
)
+ SYNC
";" (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
| ReturnStmt<out s>
)
@@ -814,25 +823,29 @@ WhileStmt<out Statement/*!*/ stmt>
)
.
LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>
-= (. bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
+= (. FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
+ MaybeFreeExpression invariant = null;
decreases = new List<Expression/*!*/>();
mod = null;
.)
- { (. isFree = false; .)
- [ "free" (. isFree = true; .)
- ]
- "invariant"
- Expression<out e> (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
- ";"
- | "decreases" DecreasesList<decreases, true> ";"
- | "modifies" (. mod = mod ?? new List<FrameExpression>(); .)
+ {
+ Invariant<out invariant> SYNC ";" (. invariants.Add(invariant); .)
+ | SYNC "decreases" DecreasesList<decreases, true> SYNC ";"
+ | SYNC "modifies" (. mod = mod ?? new List<FrameExpression>(); .)
[ FrameExpression<out fe> (. mod.Add(fe); .)
{ "," FrameExpression<out fe> (. mod.Add(fe); .)
}
- ] ";"
+ ] SYNC ";"
}
.
+Invariant<out MaybeFreeExpression/*!*/ invariant>
+= (. bool isFree = false; Expression/*!*/ e; invariant = null; .)
+ SYNC
+ ["free" (. isFree = true; .)
+ ]
+ "invariant" Expression<out e> (. invariant = new MaybeFreeExpression(e, isFree); .)
+ .
DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
= (. Expression/*!*/ e; .)
PossiblyWildExpression<out e> (. if (!allowWildcard && e is WildcardExpr) {
@@ -1310,8 +1323,8 @@ Suffix<ref Expression/*!*/ e>
}
)
| ".." (. anyDots = true; .)
- [ Expression<out ee> (. e1 = ee; .)
- ]
+ [ Expression<out ee> (. e1 = ee; .)
+ ]
)
(. if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 583fcc61..f723ad2c 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -23,7 +23,7 @@ public class Parser {
const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -134,10 +134,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);
}
@@ -150,15 +150,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 {
@@ -182,7 +182,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -191,13 +191,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
// to support multiple files, create a default module only if theModules doesn't already contain one
DefaultModuleDecl defaultModule = null;
foreach (ModuleDecl mdecl in theModules) {
- defaultModule = mdecl as DefaultModuleDecl;
- if (defaultModule != null) { break; }
+ defaultModule = mdecl as DefaultModuleDecl;
+ if (defaultModule != null) { break; }
}
bool defaultModuleCreatedHere = false;
if (defaultModule == null) {
- defaultModuleCreatedHere = true;
- defaultModule = new DefaultModuleDecl();
+ defaultModuleCreatedHere = true;
+ defaultModule = new DefaultModuleDecl();
}
while (StartOf(1)) {
@@ -241,14 +241,14 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
theModules.Add(defaultModule);
} else {
- // find the default class in the default module, then append membersDefaultClass to its member list
- foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
- DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;
- if (defaultClass != null) {
- defaultClass.Members.AddRange(membersDefaultClass);
- break;
- }
- }
+ // find the default class in the default module, then append membersDefaultClass to its member list
+ foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
+ DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;
+ if (defaultClass != null) {
+ defaultClass.Members.AddRange(membersDefaultClass);
+ break;
+ }
+ }
}
Expect(0);
@@ -288,6 +288,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(105); Get();}
Expect(9);
while (la.kind == 7) {
Attribute(ref attrs);
@@ -310,7 +311,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (optionalId == null)
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
else
- c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
+ c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
@@ -325,6 +326,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
IToken bodyStart = Token.NoToken; // dummy assignment
+ while (!(la.kind == 0 || la.kind == 14)) {SynErr(106); Get();}
Expect(14);
while (la.kind == 7) {
Attribute(ref attrs);
@@ -340,6 +342,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Get();
DatatypeMemberDecl(ctors);
}
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(107); Get();}
Expect(17);
dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
dt.BodyStartTok = bodyStart;
@@ -375,7 +378,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
mm.Add(m);
} else if (la.kind == 20) {
CouplingInvDecl(mmod, mm);
- } else SynErr(105);
+ } else SynErr(108);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -397,6 +400,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(109); Get();}
Expect(18);
if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -411,6 +415,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(110); Get();}
Expect(17);
}
@@ -477,6 +482,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
+ while (!(StartOf(4))) {SynErr(111); Get();}
if (la.kind == 25) {
Get();
} else if (la.kind == 26) {
@@ -484,21 +490,21 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (allowConstructor) {
isConstructor = true;
} else {
- SemErr(t, "constructors are only allowed in classes");
+ SemErr(t, "constructors are only allowed in classes");
}
} else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(106);
+ } else SynErr(112);
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'");
- }
+ if (mmod.IsGhost) {
+ SemErr(t, "constructors cannot be declared 'ghost'");
+ }
+ if (mmod.IsStatic) {
+ SemErr(t, "constructors cannot be declared 'static'");
+ }
}
while (la.kind == 7) {
@@ -514,7 +520,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs);
}
- while (StartOf(4)) {
+ while (StartOf(5)) {
MethodSpec(req, mod, ens, dec);
}
if (la.kind == 7) {
@@ -524,9 +530,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
else if (isConstructor)
- m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);
+ 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 = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
m.BodyStartTok = bodyStart;
m.BodyEndTok = bodyEnd;
@@ -579,7 +585,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(33);
- if (StartOf(5)) {
+ if (StartOf(6)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
while (la.kind == 19) {
@@ -656,9 +662,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Get();
UserDefinedType udt = ty as UserDefinedType;
if (udt != null && udt.TypeArgs.Count == 0) {
- name = udt.Name;
+ name = udt.Name;
} else {
- SemErr(id, "invalid formal-parameter name in datatype constructor");
+ SemErr(id, "invalid formal-parameter name in datatype constructor");
}
Type(out ty);
@@ -666,7 +672,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (name != null) {
identName = name;
} else {
- identName = "#" + anonymousIds++;
+ identName = "#" + anonymousIds++;
}
}
@@ -728,7 +734,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(107); break;
+ default: SynErr(113); break;
}
}
@@ -752,9 +758,10 @@ 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;
+ while (!(StartOf(7))) {SynErr(114); Get();}
if (la.kind == 28) {
Get();
- if (StartOf(6)) {
+ if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 19) {
@@ -763,6 +770,7 @@ List<Expression/*!*/>/*!*/ decreases) {
mod.Add(fe);
}
}
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(115); Get();}
Expect(17);
} else if (la.kind == 29 || la.kind == 30 || la.kind == 31) {
if (la.kind == 29) {
@@ -772,19 +780,22 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 30) {
Get();
Expression(out e);
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(116); Get();}
Expect(17);
req.Add(new MaybeFreeExpression(e, isFree));
} else if (la.kind == 31) {
Get();
Expression(out e);
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(117); Get();}
Expect(17);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(108);
+ } else SynErr(118);
} else if (la.kind == 32) {
Get();
DecreasesList(decreases, false);
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(119); Get();}
Expect(17);
- } else SynErr(109);
+ } else SynErr(120);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -793,7 +804,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(7);
bodyStart = t;
- while (StartOf(7)) {
+ while (StartOf(9)) {
Stmt(body);
}
Expect(8);
@@ -818,7 +829,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (!allowWildcard && e is WildcardExpr) {
SemErr(e.tok, "'decreases *' is only allowed on loops");
} else {
- decreases.Add(e);
+ decreases.Add(e);
}
while (la.kind == 19) {
@@ -827,7 +838,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (!allowWildcard && e is WildcardExpr) {
SemErr(e.tok, "'decreases *' is only allowed on loops");
} else {
- decreases.Add(e);
+ decreases.Add(e);
}
}
@@ -863,7 +874,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
int dims = 1;
if (tok.val.Length != 5) {
- dims = int.Parse(tok.val.Substring(5));
+ dims = int.Parse(tok.val.Substring(5));
}
ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
@@ -874,20 +885,22 @@ List<Expression/*!*/>/*!*/ decreases) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(110);
+ } else SynErr(121);
}
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 == 30) {
+ while (!(la.kind == 0 || la.kind == 30)) {SynErr(122); Get();}
Get();
Expression(out e);
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(123); Get();}
Expect(17);
reqs.Add(e);
} else if (la.kind == 43) {
Get();
- if (StartOf(8)) {
+ if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
while (la.kind == 19) {
@@ -896,17 +909,20 @@ List<Expression/*!*/>/*!*/ decreases) {
reads.Add(fe);
}
}
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(124); Get();}
Expect(17);
} else if (la.kind == 31) {
Get();
Expression(out e);
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(125); Get();}
Expect(17);
ens.Add(e);
} else if (la.kind == 32) {
Get();
DecreasesList(decreases, false);
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(126); Get();}
Expect(17);
- } else SynErr(111);
+ } else SynErr(127);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -923,9 +939,9 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 44) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
- } else if (StartOf(6)) {
+ } else if (StartOf(8)) {
FrameExpression(out fe);
- } else SynErr(112);
+ } else SynErr(128);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -934,9 +950,9 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 44) {
Get();
e = new WildcardExpr(t);
- } else if (StartOf(6)) {
+ } else if (StartOf(8)) {
Expression(out e);
- } else SynErr(113);
+ } else SynErr(129);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -952,6 +968,7 @@ List<Expression/*!*/>/*!*/ decreases) {
IToken bodyStart, bodyEnd;
int breakCount;
+ while (!(StartOf(11))) {SynErr(130); Get();}
switch (la.kind) {
case 7: {
BlockStmt(out s, out bodyStart, out bodyEnd);
@@ -1013,7 +1030,8 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
breakCount++;
}
- } else SynErr(114);
+ } else SynErr(131);
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(132); Get();}
Expect(17);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
@@ -1022,7 +1040,7 @@ List<Expression/*!*/>/*!*/ decreases) {
ReturnStmt(out s);
break;
}
- default: SynErr(115); break;
+ default: SynErr(133); break;
}
}
@@ -1093,7 +1111,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 22) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(116);
+ } else SynErr(134);
s = new UpdateStmt(x, lhss, rhss);
}
@@ -1134,13 +1152,13 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(17);
UpdateStmt update;
if (rhss.Count == 0) {
- update = null;
+ update = null;
} else {
- var ies = new List<Expression>();
- foreach (var lhs in lhss) {
- ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
- }
- update = new UpdateStmt(assignTok, ies, rhss);
+ var ies = new List<Expression>();
+ foreach (var lhs in lhss) {
+ ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
+ }
+ update = new UpdateStmt(assignTok, ies, rhss);
}
s = new VarDeclStmt(x, lhss, update);
@@ -1169,13 +1187,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(117);
+ } else SynErr(135);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(118);
+ } else SynErr(136);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1197,11 +1215,11 @@ List<Expression/*!*/>/*!*/ decreases) {
LoopSpec(out invariants, out decreases, out mod);
BlockStmt(out body, out bodyStart, out bodyEnd);
stmt = new WhileStmt(x, guard, invariants, decreases, mod, body);
- } else if (StartOf(9)) {
+ } else if (StartOf(12)) {
LoopSpec(out invariants, out decreases, out mod);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives);
- } else SynErr(119);
+ } else SynErr(137);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1260,7 +1278,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(48);
returnTok = t;
- if (StartOf(10)) {
+ if (StartOf(13)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
while (la.kind == 19) {
@@ -1298,7 +1316,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Ident(out x);
Expect(33);
args = new List<Expression/*!*/>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(args);
}
Expect(34);
@@ -1309,7 +1327,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (ee != null) {
r = new TypeRhs(newToken, ty, ee);
} else {
- r = new TypeRhs(newToken, ty, initCall);
+ r = new TypeRhs(newToken, ty, initCall);
}
} else if (la.kind == 54) {
@@ -1320,10 +1338,10 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 44) {
Get();
r = new HavocRhs(t);
- } else if (StartOf(6)) {
+ } else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(120);
+ } else SynErr(138);
}
void Lhs(out Expression e) {
@@ -1334,13 +1352,13 @@ List<Expression/*!*/>/*!*/ decreases) {
while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
- } else if (StartOf(11)) {
+ } else if (StartOf(14)) {
ConstAtomExpression(out e);
Suffix(ref e);
while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
- } else SynErr(121);
+ } else SynErr(139);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1360,10 +1378,10 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 44) {
Get();
e = null;
- } else if (StartOf(6)) {
+ } else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(122);
+ } else SynErr(140);
Expect(34);
}
@@ -1380,7 +1398,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression(out e);
Expect(58);
body = new List<Statement>();
- while (StartOf(7)) {
+ while (StartOf(9)) {
Stmt(body);
}
alternatives.Add(new GuardedAlternative(x, e, body));
@@ -1389,30 +1407,29 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod) {
- bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
+ FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
+ MaybeFreeExpression invariant = null;
decreases = new List<Expression/*!*/>();
mod = null;
- while (StartOf(12)) {
+ while (StartOf(15)) {
if (la.kind == 29 || la.kind == 60) {
- isFree = false;
- if (la.kind == 29) {
- Get();
- isFree = true;
- }
- Expect(60);
- Expression(out e);
- invariants.Add(new MaybeFreeExpression(e, isFree));
+ Invariant(out invariant);
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(141); Get();}
Expect(17);
+ invariants.Add(invariant);
} else if (la.kind == 32) {
+ while (!(la.kind == 0 || la.kind == 32)) {SynErr(142); Get();}
Get();
DecreasesList(decreases, true);
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(143); Get();}
Expect(17);
} else {
+ while (!(la.kind == 0 || la.kind == 28)) {SynErr(144); Get();}
Get();
mod = mod ?? new List<FrameExpression>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 19) {
@@ -1421,11 +1438,24 @@ List<Expression/*!*/>/*!*/ decreases) {
mod.Add(fe);
}
}
+ while (!(la.kind == 0 || la.kind == 17)) {SynErr(145); Get();}
Expect(17);
}
}
}
+ void Invariant(out MaybeFreeExpression/*!*/ invariant) {
+ bool isFree = false; Expression/*!*/ e; invariant = null;
+ while (!(la.kind == 0 || la.kind == 29 || la.kind == 60)) {SynErr(146); Get();}
+ if (la.kind == 29) {
+ Get();
+ isFree = true;
+ }
+ Expect(60);
+ Expression(out e);
+ invariant = new MaybeFreeExpression(e, isFree);
+ }
+
void CaseStatement(out MatchCaseStmt/*!*/ c) {
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ x, id;
@@ -1448,7 +1478,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(34);
}
Expect(58);
- while (StartOf(7)) {
+ while (StartOf(9)) {
Stmt(body);
}
c = new MatchCaseStmt(x, id.val, arguments, body);
@@ -1459,10 +1489,10 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 4) {
Get();
arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2));
- } else if (StartOf(6)) {
+ } else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(123);
+ } else SynErr(147);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1514,13 +1544,13 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 67) {
Get();
- } else SynErr(124);
+ } else SynErr(148);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(13)) {
+ if (StartOf(16)) {
if (la.kind == 70 || la.kind == 71) {
AndOp();
x = t;
@@ -1552,7 +1582,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 69) {
Get();
- } else SynErr(125);
+ } else SynErr(149);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1561,23 +1591,23 @@ List<Expression/*!*/>/*!*/ decreases) {
List<Expression> chain = null;
List<BinaryExpr.Opcode> ops = null;
int kind = 0; // 0 ("uncommitted") indicates chain of ==, possibly with one !=
- // 1 ("ascending") indicates chain of ==, <, <=, possibly with one !=
- // 2 ("descending") indicates chain of ==, >, >=, possibly with one !=
- // 3 ("illegal") indicates illegal chain
- // 4 ("disjoint") indicates chain of disjoint set operators
+ // 1 ("ascending") indicates chain of ==, <, <=, possibly with one !=
+ // 2 ("descending") indicates chain of ==, >, >=, possibly with one !=
+ // 3 ("illegal") indicates illegal chain
+ // 4 ("disjoint") indicates chain of disjoint set operators
bool hasSeenNeq = false;
Term(out e0);
e = e0;
- if (StartOf(14)) {
+ if (StartOf(17)) {
RelOp(out x, out op);
firstOpTok = x;
Term(out e1);
e = new BinaryExpr(x, op, e0, e1);
if (op == BinaryExpr.Opcode.Disjoint)
- acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
- while (StartOf(14)) {
+ while (StartOf(17)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -1631,11 +1661,11 @@ List<Expression/*!*/>/*!*/ decreases) {
Term(out e1);
ops.Add(op); chain.Add(e1);
if (op == BinaryExpr.Opcode.Disjoint) {
- e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
- acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
+ e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
}
else
- e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
+ e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
}
}
@@ -1650,7 +1680,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 71) {
Get();
- } else SynErr(126);
+ } else SynErr(150);
}
void OrOp() {
@@ -1658,7 +1688,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 73) {
Get();
- } else SynErr(127);
+ } else SynErr(151);
}
void Term(out Expression/*!*/ e0) {
@@ -1727,10 +1757,10 @@ List<Expression/*!*/>/*!*/ decreases) {
if (y == Token.NoToken) {
SemErr(x, "invalid RelOp");
} else if (y.pos != x.pos + 1) {
- SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");
+ SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");
} else {
- x.val = "!in";
- op = BinaryExpr.Opcode.NotIn;
+ x.val = "!in";
+ op = BinaryExpr.Opcode.NotIn;
}
break;
@@ -1750,7 +1780,7 @@ List<Expression/*!*/>/*!*/ decreases) {
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(128); break;
+ default: SynErr(152); break;
}
}
@@ -1772,7 +1802,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(129);
+ } else SynErr(153);
}
void UnaryExpression(out Expression/*!*/ e) {
@@ -1818,7 +1848,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
break;
}
- default: SynErr(130); break;
+ default: SynErr(154); break;
}
}
@@ -1833,7 +1863,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 87) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(131);
+ } else SynErr(155);
}
void NegOp() {
@@ -1841,7 +1871,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 88) {
Get();
- } else SynErr(132);
+ } else SynErr(156);
}
void EndlessExpression(out Expression e) {
@@ -1918,7 +1948,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new LetExpr(x, letVars, letRHSs, e);
break;
}
- default: SynErr(133); break;
+ default: SynErr(157); break;
}
}
@@ -1937,7 +1967,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 33) {
Get();
openParen = t; args = new List<Expression>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(args);
}
Expect(34);
@@ -1957,7 +1987,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 33) {
Get();
args = new List<Expression/*!*/>(); func = true;
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(args);
}
Expect(34);
@@ -1967,13 +1997,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 51) {
Get();
x = t;
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expression(out ee);
e0 = ee;
if (la.kind == 97) {
Get();
anyDots = true;
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
@@ -1992,39 +2022,39 @@ List<Expression/*!*/>/*!*/ decreases) {
multipleIndices.Add(ee);
}
- } else SynErr(134);
+ } else SynErr(158);
} else if (la.kind == 97) {
Get();
anyDots = true;
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- } else SynErr(135);
+ } else SynErr(159);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);
} else {
- if (!anyDots && e0 == null) {
- /* a parsing error occurred */
- e0 = dummyExpr;
- }
- Contract.Assert(anyDots || e0 != null);
- if (anyDots) {
- //Contract.Assert(e0 != null || e1 != null);
- e = new SeqSelectExpr(x, false, e, e0, e1);
- } else if (e1 == null) {
- Contract.Assert(e0 != null);
- e = new SeqSelectExpr(x, true, e, e0, null);
- } else {
- Contract.Assert(e0 != null);
- e = new SeqUpdateExpr(x, e, e0, e1);
- }
+ if (!anyDots && e0 == null) {
+ /* a parsing error occurred */
+ e0 = dummyExpr;
+ }
+ Contract.Assert(anyDots || e0 != null);
+ if (anyDots) {
+ //Contract.Assert(e0 != null || e1 != null);
+ e = new SeqSelectExpr(x, false, e, e0, e1);
+ } else if (e1 == null) {
+ Contract.Assert(e0 != null);
+ e = new SeqSelectExpr(x, true, e, e0, null);
+ } else {
+ Contract.Assert(e0 != null);
+ e = new SeqUpdateExpr(x, e, e0, e1);
+ }
}
Expect(52);
- } else SynErr(136);
+ } else SynErr(160);
}
void DisplayExpr(out Expression e) {
@@ -2035,7 +2065,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 7) {
Get();
x = t; elements = new List<Expression/*!*/>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
@@ -2043,12 +2073,12 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 51) {
Get();
x = t; elements = new List<Expression/*!*/>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
Expect(52);
- } else SynErr(137);
+ } else SynErr(161);
}
void MultiSetExpr(out Expression e) {
@@ -2061,7 +2091,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 7) {
Get();
elements = new List<Expression/*!*/>();
- if (StartOf(6)) {
+ if (StartOf(8)) {
Expressions(elements);
}
e = new MultiSetDisplayExpr(x, elements);
@@ -2072,9 +2102,9 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression(out e);
e = new MultiSetFormingExpr(x, e);
Expect(34);
- } else if (StartOf(15)) {
+ } else if (StartOf(18)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(138);
+ } else SynErr(162);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2151,7 +2181,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(34);
break;
}
- default: SynErr(139); break;
+ default: SynErr(163); break;
}
}
@@ -2160,8 +2190,8 @@ List<Expression/*!*/>/*!*/ decreases) {
try {
n = BigInteger.Parse(t.val);
} catch (System.FormatException) {
- SemErr("incorrectly formatted number");
- n = BigInteger.Zero;
+ SemErr("incorrectly formatted number");
+ n = BigInteger.Zero;
}
}
@@ -2194,14 +2224,14 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 100 || la.kind == 101) {
Exists();
x = t;
- } else SynErr(140);
+ } else SynErr(164);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
if (univ) {
q = new ForallExpr(x, bvars, range, body, attrs);
} else {
- q = new ExistsExpr(x, bvars, range, body, attrs);
+ q = new ExistsExpr(x, bvars, range, body, attrs);
}
}
@@ -2264,7 +2294,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 99) {
Get();
- } else SynErr(141);
+ } else SynErr(165);
}
void Exists() {
@@ -2272,7 +2302,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 101) {
Get();
- } else SynErr(142);
+ } else SynErr(166);
}
void QSep() {
@@ -2280,7 +2310,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 103) {
Get();
- } else SynErr(143);
+ } else SynErr(167);
}
void AttributeBody(ref Attributes attrs) {
@@ -2291,7 +2321,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(22);
Expect(1);
aName = t.val;
- if (StartOf(16)) {
+ if (StartOf(19)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 19) {
@@ -2307,23 +2337,27 @@ List<Expression/*!*/>/*!*/ decreases) {
public void Parse() {
la = new Token();
- la.val = "";
+ la.val = "";
Get();
Dafny();
+ Expect(0);
- 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},
+ {T,T,T,x, x,x,x,T, x,T,T,T, x,x,T,x, T,T,T,x, x,x,x,x, x,T,T,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, 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,T,T,T, T,T,T,T, 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,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,T,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,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,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},
+ {T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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, 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,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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {T,x,x,x, 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,T,T,x, x,x,x,T, x,x,x,x, 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,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,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, 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,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, 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,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,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, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {T,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,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, 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,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T,T,x, x,x,x,T, x,x,x,x, 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,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,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, T,T,T,T, T,T,T,T, x,x,T,T, T,T,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,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
@@ -2340,18 +2374,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;
@@ -2459,49 +2495,73 @@ public class Errors {
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 MethodDecl"; break;
- case 107: s = "invalid TypeAndToken"; break;
- case 108: s = "invalid MethodSpec"; break;
- case 109: s = "invalid MethodSpec"; break;
- case 110: s = "invalid ReferenceType"; break;
- case 111: s = "invalid FunctionSpec"; break;
- case 112: s = "invalid PossiblyWildFrameExpression"; break;
- case 113: s = "invalid PossiblyWildExpression"; break;
- case 114: s = "invalid OneStmt"; break;
- case 115: s = "invalid OneStmt"; break;
- case 116: s = "invalid UpdateStmt"; break;
- case 117: s = "invalid IfStmt"; break;
- case 118: s = "invalid IfStmt"; break;
- case 119: s = "invalid WhileStmt"; break;
- case 120: s = "invalid Rhs"; break;
- case 121: s = "invalid Lhs"; break;
- case 122: s = "invalid Guard"; break;
- case 123: s = "invalid AttributeArg"; break;
- case 124: s = "invalid EquivOp"; break;
- case 125: s = "invalid ImpliesOp"; break;
- case 126: s = "invalid AndOp"; break;
- case 127: s = "invalid OrOp"; break;
- case 128: s = "invalid RelOp"; break;
- case 129: s = "invalid AddOp"; break;
- case 130: s = "invalid UnaryExpression"; break;
- case 131: s = "invalid MulOp"; break;
- case 132: s = "invalid NegOp"; break;
- case 133: s = "invalid EndlessExpression"; break;
- case 134: s = "invalid Suffix"; break;
- case 135: s = "invalid Suffix"; break;
- case 136: s = "invalid Suffix"; break;
- case 137: s = "invalid DisplayExpr"; break;
- case 138: s = "invalid MultiSetExpr"; break;
- case 139: s = "invalid ConstAtomExpression"; break;
- case 140: s = "invalid QuantifierGuts"; break;
- case 141: s = "invalid Forall"; break;
- case 142: s = "invalid Exists"; break;
- case 143: s = "invalid QSep"; break;
+ case 105: s = "this symbol not expected in ClassDecl"; break;
+ case 106: s = "this symbol not expected in DatatypeDecl"; break;
+ case 107: s = "this symbol not expected in DatatypeDecl"; break;
+ case 108: s = "invalid ClassMemberDecl"; break;
+ case 109: s = "this symbol not expected in FieldDecl"; break;
+ case 110: s = "this symbol not expected in FieldDecl"; break;
+ case 111: s = "this symbol not expected in MethodDecl"; break;
+ case 112: s = "invalid MethodDecl"; break;
+ case 113: s = "invalid TypeAndToken"; break;
+ case 114: s = "this symbol not expected in MethodSpec"; break;
+ case 115: s = "this symbol not expected in MethodSpec"; break;
+ case 116: s = "this symbol not expected in MethodSpec"; break;
+ case 117: s = "this symbol not expected in MethodSpec"; break;
+ case 118: s = "invalid MethodSpec"; break;
+ case 119: s = "this symbol not expected in MethodSpec"; break;
+ case 120: s = "invalid MethodSpec"; break;
+ case 121: s = "invalid ReferenceType"; break;
+ case 122: s = "this symbol not expected in FunctionSpec"; break;
+ case 123: s = "this symbol not expected in FunctionSpec"; break;
+ case 124: s = "this symbol not expected in FunctionSpec"; break;
+ case 125: s = "this symbol not expected in FunctionSpec"; break;
+ case 126: s = "this symbol not expected in FunctionSpec"; break;
+ case 127: s = "invalid FunctionSpec"; break;
+ case 128: s = "invalid PossiblyWildFrameExpression"; break;
+ case 129: s = "invalid PossiblyWildExpression"; break;
+ case 130: s = "this symbol not expected in OneStmt"; break;
+ case 131: s = "invalid OneStmt"; break;
+ case 132: s = "this symbol not expected in OneStmt"; break;
+ case 133: s = "invalid OneStmt"; break;
+ case 134: s = "invalid UpdateStmt"; break;
+ case 135: s = "invalid IfStmt"; break;
+ case 136: s = "invalid IfStmt"; break;
+ case 137: s = "invalid WhileStmt"; break;
+ case 138: s = "invalid Rhs"; break;
+ case 139: s = "invalid Lhs"; break;
+ case 140: s = "invalid Guard"; break;
+ case 141: s = "this symbol not expected in LoopSpec"; break;
+ case 142: s = "this symbol not expected in LoopSpec"; break;
+ case 143: s = "this symbol not expected in LoopSpec"; break;
+ case 144: s = "this symbol not expected in LoopSpec"; break;
+ case 145: s = "this symbol not expected in LoopSpec"; break;
+ case 146: s = "this symbol not expected in Invariant"; break;
+ case 147: s = "invalid AttributeArg"; break;
+ case 148: s = "invalid EquivOp"; break;
+ case 149: s = "invalid ImpliesOp"; break;
+ case 150: s = "invalid AndOp"; break;
+ case 151: s = "invalid OrOp"; break;
+ case 152: s = "invalid RelOp"; break;
+ case 153: s = "invalid AddOp"; break;
+ case 154: s = "invalid UnaryExpression"; break;
+ case 155: s = "invalid MulOp"; break;
+ case 156: s = "invalid NegOp"; break;
+ case 157: s = "invalid EndlessExpression"; break;
+ case 158: s = "invalid Suffix"; break;
+ case 159: s = "invalid Suffix"; break;
+ case 160: s = "invalid Suffix"; break;
+ case 161: s = "invalid DisplayExpr"; break;
+ case 162: s = "invalid MultiSetExpr"; break;
+ case 163: s = "invalid ConstAtomExpression"; break;
+ case 164: s = "invalid QuantifierGuts"; break;
+ case 165: s = "invalid Forall"; break;
+ case 166: s = "invalid Exists"; break;
+ case 167: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2509,8 +2569,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++;
}
@@ -2526,4 +2587,5 @@ public class FatalError: Exception {
public FatalError(string m): base(m) {}
}
+
} \ No newline at end of file
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 1ab06974..f0eb1937 100644
--- a/Dafny/Scanner.cs
+++ b/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.
@@ -213,22 +215,24 @@ public class Scanner {
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);
-}
+ [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
+ int charPos;
int col; // column number of current character
int line; // line number of current character
int oldEols; // EOLs that appeared in a comment;
@@ -236,13 +240,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 +294,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 +306,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 +322,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 +345,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 +360,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 +368,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 +420,7 @@ void objectInvariant(){
return;
}
-
+
}
}
@@ -438,7 +440,7 @@ void objectInvariant(){
bool Comment0() {
- int level = 1, pos0 = pos, line0 = line, col0 = col;
+ int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos;
NextCh();
if (ch == '/') {
NextCh();
@@ -451,13 +453,13 @@ void objectInvariant(){
else NextCh();
}
} else {
- buffer.Pos = pos0; NextCh(); line = line0; col = col0;
+ buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;
}
return false;
}
bool Comment1() {
- int level = 1, pos0 = pos, line0 = line, col0 = col;
+ int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos;
NextCh();
if (ch == '*') {
NextCh();
@@ -478,7 +480,7 @@ void objectInvariant(){
else NextCh();
}
} else {
- buffer.Pos = pos0; NextCh(); line = line0; col = col0;
+ buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;
}
return false;
}
@@ -556,10 +558,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: {
@@ -759,14 +764,14 @@ void objectInvariant(){
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);
@@ -787,7 +792,7 @@ void objectInvariant(){
}
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 03:37:47 +0000