diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-04-19 16:48:32 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-04-19 16:48:32 -0700 |
| commit | a0ccbb8461b68eb4a61ba78e0efced94423e93c7 (patch) | |
| tree | 41bd0df0cf2afbb78c7cd7f500840397fe332269 | |
| parent | 9313173a5462dd6bf0ac386c6ac129d6284e9f4d (diff) | |
Dafny: added type "nat"
| -rw-r--r-- | Dafny/Dafny.atg | 1 | ||||
| -rw-r--r-- | Dafny/DafnyAst.cs | 20 | ||||
| -rw-r--r-- | Dafny/Parser.cs | 685 | ||||
| -rw-r--r-- | Dafny/Resolver.cs | 57 | ||||
| -rw-r--r-- | Dafny/Scanner.cs | 265 | ||||
| -rw-r--r-- | Dafny/Translator.cs | 163 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 48 | ||||
| -rw-r--r-- | Test/dafny0/NatTypes.dfy | 110 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 9 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 3 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 2 | ||||
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 7 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 1 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 2 | ||||
| -rw-r--r-- | Util/vim/syntax/dafny.vim | 2 |
15 files changed, 829 insertions, 546 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 7d7a496c..e32f0745 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -516,6 +516,7 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty> List<Type/*!*/>/*!*/ gt;
.)
( "bool" (. tok = t; .)
+ | "nat" (. tok = t; ty = new NatType(); .)
| "int" (. tok = t; ty = new IntType(); .)
| "set" (. tok = t; gt = new List<Type/*!*/>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 045f879a..69756d76 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -135,6 +135,10 @@ namespace Microsoft.Dafny { }
}
+ public bool IsSubrangeType {
+ get { return this is NatType; }
+ }
+
public bool IsRefType {
get {
if (this is ObjectType) {
@@ -197,7 +201,16 @@ namespace Microsoft.Dafny { }
}
- public class ObjectType : BasicType {
+ public class NatType : IntType
+ {
+ [Pure]
+ public override string ToString() {
+ return "nat";
+ }
+ }
+
+ public class ObjectType : BasicType
+ {
[Pure]
public override string ToString() {
return "object";
@@ -218,9 +231,8 @@ namespace Microsoft.Dafny { }
public class SetType : CollectionType {
- public SetType(Type arg) :base(arg){
+ public SetType(Type arg) : base(arg) {
Contract.Requires(arg != null);
-
}
[Pure]
public override string ToString() {
@@ -231,7 +243,7 @@ namespace Microsoft.Dafny { }
public class SeqType : CollectionType {
- public SeqType(Type arg):base(arg) {
+ public SeqType(Type arg) : base(arg) {
Contract.Requires(arg != null);
}
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index 988b73e2..72e66d1d 100644 --- a/Dafny/Parser.cs +++ b/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 = 105;
+ public const int maxT = 106;
const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -161,10 +161,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);
}
@@ -177,15 +177,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 {
@@ -209,7 +209,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -394,7 +394,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
if (la.kind == 16) {
FieldDecl(mmod, mm);
- } else if (la.kind == 37) {
+ } else if (la.kind == 38) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (la.kind == 10 || la.kind == 23) {
@@ -402,7 +402,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! mm.Add(m);
} else if (la.kind == 18) {
CouplingInvDecl(mmod, mm);
- } else SynErr(106);
+ } else SynErr(107);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -457,7 +457,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- Expect(37);
+ Expect(38);
if (la.kind == 23) {
Get();
isFunctionMethod = true;
@@ -486,7 +486,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
FunctionBody(out bb, out bodyStart, out bodyEnd);
body = bb;
- } else SynErr(107);
+ } else SynErr(108);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
f.BodyStartTok = bodyStart;
@@ -515,7 +515,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! } else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(108);
+ } else SynErr(109);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
while (la.kind == 7) {
@@ -542,7 +542,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
BlockStmt(out bb, out bodyStart, out bodyEnd);
body = (BlockStmt)bb;
- } else SynErr(109);
+ } else SynErr(110);
parseVarScope.PopMarker();
if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -634,18 +634,18 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; Expression/*!*/ e0; Expression/*!*/ e1 = dummyExpr;
e = dummyExpr;
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
x = t;
Expression(out e);
- Expect(66);
+ Expect(67);
Expression(out e0);
- Expect(55);
+ Expect(56);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(8)) {
EquivExpression(out e);
- } else SynErr(110);
+ } else SynErr(111);
}
void GIdentType(bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {
@@ -709,13 +709,23 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type/*!*/>/*!*/ gt;
- if (la.kind == 32) {
+ switch (la.kind) {
+ case 32: {
Get();
tok = t;
- } else if (la.kind == 33) {
+ break;
+ }
+ case 33: {
+ Get();
+ tok = t; ty = new NatType();
+ break;
+ }
+ case 34: {
Get();
tok = t; ty = new IntType();
- } else if (la.kind == 34) {
+ break;
+ }
+ case 35: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -724,7 +734,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
ty = new SetType(gt[0]);
- } else if (la.kind == 35) {
+ break;
+ }
+ case 36: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -733,9 +745,14 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
ty = new SeqType(gt[0]);
- } else if (la.kind == 1 || la.kind == 3 || la.kind == 36) {
+ break;
+ }
+ case 1: case 3: case 37: {
ReferenceType(out tok, out ty);
- } else SynErr(111);
+ break;
+ }
+ default: SynErr(112); break;
+ }
}
void Formals(bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals) {
@@ -785,12 +802,12 @@ List<Expression/*!*/>/*!*/ decreases) { Expression(out e);
Expect(15);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(112);
+ } else SynErr(113);
} else if (la.kind == 29) {
Get();
Expressions(decreases);
Expect(15);
- } else SynErr(113);
+ } else SynErr(114);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -812,7 +829,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 == 40) {
+ if (la.kind == 41) {
Get();
Ident(out id);
fieldName = id.val;
@@ -849,7 +866,7 @@ List<Expression/*!*/>/*!*/ decreases) { tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type/*!*/>/*!*/ gt;
- if (la.kind == 36) {
+ if (la.kind == 37) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 3) {
@@ -872,7 +889,7 @@ List<Expression/*!*/>/*!*/ decreases) { GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(114);
+ } else SynErr(115);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -883,7 +900,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expression(out e);
Expect(15);
reqs.Add(e);
- } else if (la.kind == 38) {
+ } else if (la.kind == 39) {
Get();
if (StartOf(11)) {
PossiblyWildFrameExpression(out fe);
@@ -904,51 +921,51 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
Expressions(decreases);
Expect(15);
- } else SynErr(115);
+ } else SynErr(116);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
Expect(7);
bodyStart = t;
- if (la.kind == 41) {
+ if (la.kind == 42) {
MatchExpression(out e);
} else if (StartOf(9)) {
Expression(out e);
- } else SynErr(116);
+ } else SynErr(117);
Expect(8);
bodyEnd = t;
}
void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 39) {
+ if (la.kind == 40) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(9)) {
FrameExpression(out fe);
- } else SynErr(117);
+ } else SynErr(118);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 39) {
+ if (la.kind == 40) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(9)) {
Expression(out e);
- } else SynErr(118);
+ } else SynErr(119);
}
void MatchExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(41);
+ Expect(42);
x = t;
Expression(out e);
- while (la.kind == 42) {
+ while (la.kind == 43) {
CaseExpression(out c);
cases.Add(c);
}
@@ -960,7 +977,7 @@ List<Expression/*!*/>/*!*/ decreases) { List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
Expression/*!*/ body;
- Expect(42);
+ Expect(43);
x = t; parseVarScope.PushMarker();
Ident(out id);
if (la.kind == 30) {
@@ -976,7 +993,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(31);
}
- Expect(43);
+ Expect(44);
MatchOrExpr(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
parseVarScope.PopMarker();
@@ -988,11 +1005,11 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
MatchOrExpr(out e);
Expect(31);
- } else if (la.kind == 41) {
+ } else if (la.kind == 42) {
MatchExpression(out e);
} else if (StartOf(9)) {
Expression(out e);
- } else SynErr(119);
+ } else SynErr(120);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1008,7 +1025,7 @@ List<Expression/*!*/>/*!*/ decreases) { ss.Add(s);
} else if (la.kind == 11 || la.kind == 16) {
VarDeclStmts(ss);
- } else SynErr(120);
+ } else SynErr(121);
}
void OneStmt(out Statement/*!*/ s) {
@@ -1016,51 +1033,51 @@ List<Expression/*!*/>/*!*/ decreases) { s = dummyStmt; /* to please the compiler */
switch (la.kind) {
- case 62: {
+ case 63: {
AssertStmt(out s);
break;
}
- case 63: {
+ case 64: {
AssumeStmt(out s);
break;
}
- case 64: {
+ case 65: {
UseStmt(out s);
break;
}
- case 65: {
+ case 66: {
PrintStmt(out s);
break;
}
- case 1: case 30: case 97: case 98: {
+ case 1: case 30: case 98: case 99: {
AssignStmt(out s, true);
break;
}
- case 53: {
+ case 54: {
HavocStmt(out s);
break;
}
- case 58: {
+ case 59: {
CallStmt(out s);
break;
}
- case 54: {
+ case 55: {
IfStmt(out s);
break;
}
- case 56: {
+ case 57: {
WhileStmt(out s);
break;
}
- case 41: {
+ case 42: {
MatchStmt(out s);
break;
}
- case 59: {
+ case 60: {
ForeachStmt(out s);
break;
}
- case 44: {
+ case 45: {
Get();
x = t;
Ident(out id);
@@ -1068,7 +1085,7 @@ List<Expression/*!*/>/*!*/ decreases) { s = new LabelStmt(x, id.val);
break;
}
- case 45: {
+ case 46: {
Get();
x = t;
if (la.kind == 1) {
@@ -1079,14 +1096,14 @@ List<Expression/*!*/>/*!*/ decreases) { s = new BreakStmt(x, label);
break;
}
- case 46: {
+ case 47: {
Get();
x = t;
Expect(15);
s = new ReturnStmt(x);
break;
}
- default: SynErr(121); break;
+ default: SynErr(122); break;
}
}
@@ -1109,7 +1126,7 @@ List<Expression/*!*/>/*!*/ decreases) { void AssertStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(62);
+ Expect(63);
x = t;
Expression(out e);
Expect(15);
@@ -1118,7 +1135,7 @@ List<Expression/*!*/>/*!*/ decreases) { void AssumeStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(63);
+ Expect(64);
x = t;
Expression(out e);
Expect(15);
@@ -1127,7 +1144,7 @@ List<Expression/*!*/>/*!*/ decreases) { void UseStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(64);
+ Expect(65);
x = t;
Expression(out e);
Expect(15);
@@ -1138,7 +1155,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);
@@ -1160,7 +1177,7 @@ List<Expression/*!*/>/*!*/ decreases) { CallStmt initCall = null;
LhsExpr(out lhs);
- Expect(47);
+ Expect(48);
x = t;
AssignRhs(out rhs, out ty, out initCall, lhs);
if (ty == null) {
@@ -1184,7 +1201,7 @@ List<Expression/*!*/>/*!*/ decreases) { void HavocStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ lhs;
- Expect(53);
+ Expect(54);
x = t;
LhsExpr(out lhs);
Expect(15);
@@ -1197,10 +1214,10 @@ List<Expression/*!*/>/*!*/ decreases) { List<IdentifierExpr/*!*/> lhs = new List<IdentifierExpr/*!*/>();
List<AutoVarDecl/*!*/> newVars = new List<AutoVarDecl/*!*/>();
- Expect(58);
+ Expect(59);
x = t;
CallStmtSubExpr(out e);
- if (la.kind == 17 || la.kind == 47) {
+ if (la.kind == 17 || la.kind == 48) {
if (la.kind == 17) {
Get();
e = ConvertToLocal(e);
@@ -1219,7 +1236,7 @@ List<Expression/*!*/>/*!*/ decreases) { Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
- Expect(47);
+ Expect(48);
CallStmtSubExpr(out e);
} else {
Get();
@@ -1254,19 +1271,19 @@ List<Expression/*!*/>/*!*/ decreases) { Statement els = null;
IToken bodyStart, bodyEnd;
- Expect(54);
+ Expect(55);
x = t;
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(122);
+ } else SynErr(123);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -1280,18 +1297,18 @@ List<Expression/*!*/>/*!*/ decreases) { Statement/*!*/ body;
IToken bodyStart, bodyEnd;
- Expect(56);
+ Expect(57);
x = t;
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
- while (la.kind == 26 || la.kind == 29 || la.kind == 57) {
- if (la.kind == 26 || la.kind == 57) {
+ while (la.kind == 26 || la.kind == 29 || la.kind == 58) {
+ if (la.kind == 26 || la.kind == 58) {
isFree = false;
if (la.kind == 26) {
Get();
isFree = true;
}
- Expect(57);
+ Expect(58);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(15);
@@ -1315,11 +1332,11 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
- Expect(41);
+ Expect(42);
x = t;
Expression(out e);
Expect(7);
- while (la.kind == 42) {
+ while (la.kind == 43) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1336,7 +1353,7 @@ List<Expression/*!*/>/*!*/ decreases) { AssignStmt bodyAssign = null;
parseVarScope.PushMarker();
- Expect(59);
+ Expect(60);
x = t;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
@@ -1347,20 +1364,20 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
Type(out ty);
}
- Expect(60);
+ Expect(61);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (la.kind == 61) {
+ if (la.kind == 62) {
Get();
Expression(out range);
}
Expect(31);
Expect(7);
- while (la.kind == 62 || la.kind == 63 || la.kind == 64) {
- if (la.kind == 62) {
+ while (la.kind == 63 || la.kind == 64 || la.kind == 65) {
+ if (la.kind == 63) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (la.kind == 63) {
+ } else if (la.kind == 64) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1371,10 +1388,10 @@ List<Expression/*!*/>/*!*/ decreases) { if (StartOf(13)) {
AssignStmt(out s, false);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else SynErr(123);
+ } else SynErr(124);
Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1396,15 +1413,15 @@ List<Expression/*!*/>/*!*/ decreases) { initCall = null;
List<Expression> args;
- if (la.kind == 48) {
+ if (la.kind == 49) {
Get();
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(ee.Count, new IntType(), true);
} else {
@@ -1420,7 +1437,7 @@ List<Expression/*!*/>/*!*/ decreases) { receiverForInitCall, x.val, args);
}
}
- } else if (la.kind == 52) {
+ } else if (la.kind == 53) {
Get();
x = t;
Expression(out e);
@@ -1430,7 +1447,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(9)) {
Expression(out e);
ee = new List<Expression>() { e };
- } else SynErr(124);
+ } else SynErr(125);
if (ee == null && ty == null) { ee = new List<Expression>() { dummyExpr}; }
}
@@ -1438,10 +1455,10 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (la.kind == 30 || la.kind == 97 || la.kind == 98) {
+ } else if (la.kind == 30 || la.kind == 98 || la.kind == 99) {
ObjectExpression(out e);
- } else SynErr(125);
- while (la.kind == 49 || la.kind == 51) {
+ } else SynErr(126);
+ while (la.kind == 50 || la.kind == 52) {
SelectOrCallSuffix(ref e);
}
}
@@ -1458,7 +1475,7 @@ List<Expression/*!*/>/*!*/ decreases) { Type(out ty);
optionalType = ty;
}
- if (la.kind == 47) {
+ if (la.kind == 48) {
Get();
AssignRhs(out rhs, out newType, out initCall, new IdentifierExpr(id, id.val));
}
@@ -1481,13 +1498,13 @@ List<Expression/*!*/>/*!*/ decreases) { void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
Expect(30);
- if (la.kind == 39) {
+ if (la.kind == 40) {
Get();
e = null;
} else if (StartOf(9)) {
Expression(out ee);
e = ee;
- } else SynErr(126);
+ } else SynErr(127);
Expect(31);
}
@@ -1497,7 +1514,7 @@ List<Expression/*!*/>/*!*/ decreases) { List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(42);
+ Expect(43);
x = t; parseVarScope.PushMarker();
Ident(out id);
if (la.kind == 30) {
@@ -1513,7 +1530,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(31);
}
- Expect(43);
+ Expect(44);
parseVarScope.PushMarker();
while (StartOf(10)) {
Stmt(body);
@@ -1527,11 +1544,11 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (la.kind == 30 || la.kind == 97 || la.kind == 98) {
+ } else if (la.kind == 30 || la.kind == 98 || la.kind == 99) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else SynErr(127);
- while (la.kind == 49 || la.kind == 51) {
+ } else SynErr(128);
+ while (la.kind == 50 || la.kind == 52) {
SelectOrCallSuffix(ref e);
}
}
@@ -1544,13 +1561,13 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(9)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(128);
+ } else SynErr(129);
}
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 67 || la.kind == 68) {
+ while (la.kind == 68 || la.kind == 69) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1561,7 +1578,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 == 69 || la.kind == 70) {
+ if (la.kind == 70 || la.kind == 71) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1570,23 +1587,23 @@ List<Expression/*!*/>/*!*/ decreases) { }
void EquivOp() {
- if (la.kind == 67) {
+ if (la.kind == 68) {
Get();
- } else if (la.kind == 68) {
+ } else if (la.kind == 69) {
Get();
- } else SynErr(129);
+ } else SynErr(130);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(14)) {
- if (la.kind == 71 || la.kind == 72) {
+ if (la.kind == 72 || la.kind == 73) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 71 || la.kind == 72) {
+ while (la.kind == 72 || la.kind == 73) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1597,7 +1614,7 @@ List<Expression/*!*/>/*!*/ decreases) { x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 73 || la.kind == 74) {
+ while (la.kind == 74 || la.kind == 75) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1608,11 +1625,11 @@ List<Expression/*!*/>/*!*/ decreases) { }
void ImpliesOp() {
- if (la.kind == 69) {
+ if (la.kind == 70) {
Get();
- } else if (la.kind == 70) {
+ } else if (la.kind == 71) {
Get();
- } else SynErr(130);
+ } else SynErr(131);
}
void RelationalExpression(out Expression/*!*/ e0) {
@@ -1626,25 +1643,25 @@ List<Expression/*!*/>/*!*/ decreases) { }
void AndOp() {
- if (la.kind == 71) {
+ if (la.kind == 72) {
Get();
- } else if (la.kind == 72) {
+ } else if (la.kind == 73) {
Get();
- } else SynErr(131);
+ } else SynErr(132);
}
void OrOp() {
- if (la.kind == 73) {
+ if (la.kind == 74) {
Get();
- } else if (la.kind == 74) {
+ } else if (la.kind == 75) {
Get();
- } else SynErr(132);
+ } else SynErr(133);
}
void Term(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (la.kind == 84 || la.kind == 85) {
+ while (la.kind == 85 || la.kind == 86) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1654,7 +1671,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 75: {
+ case 76: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
@@ -1669,59 +1686,59 @@ List<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 76: {
+ case 77: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 77: {
+ case 78: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 78: {
+ case 79: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 79: {
+ case 80: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 60: {
+ case 61: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 80: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 81: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 83: {
+ case 84: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(133); break;
+ default: SynErr(134); break;
}
}
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 39 || la.kind == 86 || la.kind == 87) {
+ while (la.kind == 40 || la.kind == 87 || la.kind == 88) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1730,23 +1747,23 @@ List<Expression/*!*/>/*!*/ decreases) { void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 84) {
+ if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 85) {
+ } else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(134);
+ } else SynErr(135);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
- if (la.kind == 85) {
+ if (la.kind == 86) {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (la.kind == 88 || la.kind == 89) {
+ } else if (la.kind == 89 || la.kind == 90) {
NegOp();
x = t;
UnaryExpression(out e);
@@ -1755,29 +1772,29 @@ List<Expression/*!*/>/*!*/ decreases) { SelectExpression(out e);
} else if (StartOf(16)) {
ConstAtomExpression(out e);
- } else SynErr(135);
+ } else SynErr(136);
}
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 == 39) {
+ if (la.kind == 40) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 86) {
+ } else if (la.kind == 87) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 87) {
+ } else if (la.kind == 88) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(136);
+ } else SynErr(137);
}
void NegOp() {
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
- } else if (la.kind == 89) {
+ } else if (la.kind == 90) {
Get();
- } else SynErr(137);
+ } else SynErr(138);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -1785,17 +1802,17 @@ List<Expression/*!*/>/*!*/ decreases) { e = dummyExpr;
switch (la.kind) {
- case 90: {
+ case 91: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 91: {
+ case 92: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 92: {
+ case 93: {
Get();
e = new LiteralExpr(t);
break;
@@ -1805,11 +1822,11 @@ List<Expression/*!*/>/*!*/ decreases) { e = new LiteralExpr(t, n);
break;
}
- case 93: {
+ case 94: {
Get();
x = t;
Ident(out dtName);
- Expect(51);
+ Expect(52);
Ident(out id);
elements = new List<Expression/*!*/>();
if (la.kind == 30) {
@@ -1822,7 +1839,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new DatatypeValue(t, dtName.val, id.val, elements);
break;
}
- case 94: {
+ case 95: {
Get();
x = t;
Expect(30);
@@ -1831,7 +1848,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new FreshExpr(x, e);
break;
}
- case 95: {
+ case 96: {
Get();
x = t;
Expect(30);
@@ -1840,12 +1857,12 @@ List<Expression/*!*/>/*!*/ decreases) { e = new AllocatedExpr(x, e);
break;
}
- case 61: {
+ case 62: {
Get();
x = t;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(61);
+ Expect(62);
break;
}
case 7: {
@@ -1858,17 +1875,17 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(8);
break;
}
- case 49: {
+ case 50: {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(9)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(50);
+ Expect(51);
break;
}
- default: SynErr(138); break;
+ default: SynErr(139); break;
}
}
@@ -1907,10 +1924,10 @@ List<Expression/*!*/>/*!*/ decreases) { void ObjectExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
- if (la.kind == 97) {
+ if (la.kind == 98) {
Get();
e = new ThisExpr(t);
- } else if (la.kind == 98) {
+ } else if (la.kind == 99) {
Get();
x = t;
Expect(30);
@@ -1923,9 +1940,9 @@ List<Expression/*!*/>/*!*/ decreases) { QuantifierGuts(out e);
} else if (StartOf(9)) {
Expression(out e);
- } else SynErr(139);
+ } else SynErr(140);
Expect(31);
- } else SynErr(140);
+ } else SynErr(141);
}
void SelectOrCallSuffix(ref Expression/*!*/ e) {
@@ -1934,7 +1951,7 @@ 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 == 30) {
@@ -1947,24 +1964,24 @@ List<Expression/*!*/>/*!*/ decreases) { e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (la.kind == 49) {
+ } else if (la.kind == 50) {
Get();
x = t;
if (StartOf(9)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
anyDots = true;
if (StartOf(9)) {
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 == 17 || la.kind == 50) {
+ } else if (la.kind == 17 || la.kind == 51) {
while (la.kind == 17) {
Get();
Expression(out ee);
@@ -1975,12 +1992,12 @@ List<Expression/*!*/>/*!*/ decreases) { multipleIndices.Add(ee);
}
- } else SynErr(141);
- } else if (la.kind == 96) {
+ } else SynErr(142);
+ } else if (la.kind == 97) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(142);
+ } else SynErr(143);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
} else {
@@ -2001,8 +2018,8 @@ List<Expression/*!*/>/*!*/ decreases) { }
}
- Expect(50);
- } else SynErr(143);
+ Expect(51);
+ } else SynErr(144);
}
void QuantifierGuts(out Expression/*!*/ q) {
@@ -2014,13 +2031,13 @@ List<Expression/*!*/>/*!*/ decreases) { Triggers trigs = null;
Expression/*!*/ body;
- if (la.kind == 99 || la.kind == 100) {
+ if (la.kind == 100 || la.kind == 101) {
Forall();
x = t; univ = true;
- } else if (la.kind == 101 || la.kind == 102) {
+ } else if (la.kind == 102 || la.kind == 103) {
Exists();
x = t;
- } else SynErr(144);
+ } else SynErr(145);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -2044,19 +2061,19 @@ List<Expression/*!*/>/*!*/ decreases) { }
void Forall() {
- if (la.kind == 99) {
+ if (la.kind == 100) {
Get();
- } else if (la.kind == 100) {
+ } else if (la.kind == 101) {
Get();
- } else SynErr(145);
+ } else SynErr(146);
}
void Exists() {
- if (la.kind == 101) {
+ if (la.kind == 102) {
Get();
- } else if (la.kind == 102) {
+ } else if (la.kind == 103) {
Get();
- } else SynErr(146);
+ } else SynErr(147);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2069,16 +2086,16 @@ List<Expression/*!*/>/*!*/ decreases) { es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(147);
+ } else SynErr(148);
Expect(8);
}
void QSep() {
- if (la.kind == 103) {
+ if (la.kind == 104) {
Get();
- } else if (la.kind == 104) {
+ } else if (la.kind == 105) {
Get();
- } else SynErr(148);
+ } else SynErr(149);
}
void AttributeBody(ref Attributes attrs) {
@@ -2105,33 +2122,33 @@ 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, x,T,x,x, x,T,T,T, T,T,T,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x},
- {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, 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,T,T, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,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,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,T, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,T, x,x,x,x, x,x,x,x},
+ {x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,T,T, x,T,x,T, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,T, x,x,x,x, x,x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,T,T, x,T,x,T, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x},
+ {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,T,T, x,x,x,x, x,x,x,x}
};
} // end Parser
@@ -2140,18 +2157,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;
@@ -2187,126 +2206,127 @@ public class Errors { case 30: s = "\"(\" expected"; break;
case 31: s = "\")\" expected"; break;
case 32: s = "\"bool\" expected"; break;
- case 33: s = "\"int\" expected"; break;
- case 34: s = "\"set\" expected"; break;
- case 35: s = "\"seq\" expected"; break;
- case 36: s = "\"object\" expected"; break;
- case 37: s = "\"function\" expected"; break;
- case 38: s = "\"reads\" expected"; break;
- case 39: s = "\"*\" expected"; break;
- case 40: s = "\"`\" expected"; break;
- case 41: s = "\"match\" expected"; break;
- case 42: s = "\"case\" 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 = "\"while\" expected"; break;
- case 57: s = "\"invariant\" expected"; break;
- case 58: s = "\"call\" expected"; break;
- case 59: s = "\"foreach\" expected"; break;
- case 60: s = "\"in\" expected"; break;
- case 61: s = "\"|\" expected"; break;
- case 62: s = "\"assert\" expected"; break;
- case 63: s = "\"assume\" expected"; break;
- case 64: s = "\"use\" expected"; break;
- case 65: s = "\"print\" expected"; break;
- case 66: s = "\"then\" expected"; break;
- case 67: s = "\"<==>\" expected"; break;
- case 68: s = "\"\\u21d4\" expected"; break;
- case 69: s = "\"==>\" expected"; break;
- case 70: s = "\"\\u21d2\" expected"; break;
- case 71: s = "\"&&\" expected"; break;
- case 72: s = "\"\\u2227\" expected"; break;
- case 73: s = "\"||\" expected"; break;
- case 74: s = "\"\\u2228\" expected"; break;
- case 75: s = "\"==\" expected"; break;
- case 76: s = "\"<=\" expected"; break;
- case 77: s = "\">=\" expected"; break;
- case 78: s = "\"!=\" expected"; break;
- case 79: s = "\"!!\" expected"; break;
- case 80: s = "\"!in\" expected"; break;
- case 81: s = "\"\\u2260\" expected"; break;
- case 82: s = "\"\\u2264\" expected"; break;
- case 83: s = "\"\\u2265\" expected"; break;
- case 84: s = "\"+\" expected"; break;
- case 85: s = "\"-\" expected"; break;
- case 86: s = "\"/\" expected"; break;
- case 87: s = "\"%\" expected"; break;
- case 88: s = "\"!\" expected"; break;
- case 89: s = "\"\\u00ac\" expected"; break;
- case 90: s = "\"false\" expected"; break;
- case 91: s = "\"true\" expected"; break;
- case 92: s = "\"null\" expected"; break;
- case 93: s = "\"#\" expected"; break;
- case 94: s = "\"fresh\" expected"; break;
- case 95: s = "\"allocated\" expected"; break;
- case 96: s = "\"..\" expected"; break;
- case 97: s = "\"this\" expected"; break;
- case 98: s = "\"old\" 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 33: s = "\"nat\" expected"; break;
+ case 34: s = "\"int\" expected"; break;
+ case 35: s = "\"set\" expected"; break;
+ case 36: s = "\"seq\" expected"; break;
+ case 37: s = "\"object\" expected"; break;
+ case 38: s = "\"function\" expected"; break;
+ case 39: s = "\"reads\" expected"; break;
+ case 40: s = "\"*\" expected"; break;
+ case 41: s = "\"`\" expected"; break;
+ case 42: s = "\"match\" expected"; break;
+ case 43: s = "\"case\" 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 = "\"while\" expected"; break;
+ case 58: s = "\"invariant\" expected"; break;
+ case 59: s = "\"call\" expected"; break;
+ case 60: s = "\"foreach\" expected"; break;
+ case 61: s = "\"in\" expected"; break;
+ case 62: s = "\"|\" expected"; break;
+ case 63: s = "\"assert\" expected"; break;
+ case 64: s = "\"assume\" expected"; break;
+ case 65: s = "\"use\" expected"; break;
+ case 66: s = "\"print\" expected"; break;
+ case 67: s = "\"then\" expected"; break;
+ case 68: s = "\"<==>\" expected"; break;
+ case 69: s = "\"\\u21d4\" expected"; break;
+ case 70: s = "\"==>\" expected"; break;
+ case 71: s = "\"\\u21d2\" expected"; break;
+ case 72: s = "\"&&\" expected"; break;
+ case 73: s = "\"\\u2227\" expected"; break;
+ case 74: s = "\"||\" expected"; break;
+ case 75: s = "\"\\u2228\" expected"; break;
+ case 76: s = "\"==\" expected"; break;
+ case 77: s = "\"<=\" expected"; break;
+ case 78: s = "\">=\" expected"; break;
+ case 79: s = "\"!=\" expected"; break;
+ case 80: s = "\"!!\" expected"; break;
+ case 81: s = "\"!in\" expected"; break;
+ case 82: s = "\"\\u2260\" expected"; break;
+ case 83: s = "\"\\u2264\" expected"; break;
+ case 84: s = "\"\\u2265\" expected"; break;
+ case 85: s = "\"+\" expected"; break;
+ case 86: s = "\"-\" expected"; break;
+ case 87: s = "\"/\" expected"; break;
+ case 88: s = "\"%\" expected"; break;
+ case 89: s = "\"!\" expected"; break;
+ case 90: s = "\"\\u00ac\" expected"; break;
+ case 91: s = "\"false\" expected"; break;
+ case 92: s = "\"true\" expected"; break;
+ case 93: s = "\"null\" expected"; break;
+ case 94: s = "\"#\" expected"; break;
+ case 95: s = "\"fresh\" expected"; break;
+ case 96: s = "\"allocated\" expected"; break;
+ case 97: s = "\"..\" expected"; break;
+ case 98: s = "\"this\" expected"; break;
+ case 99: s = "\"old\" expected"; break;
+ case 100: s = "\"forall\" expected"; break;
+ case 101: s = "\"\\u2200\" expected"; break;
+ case 102: s = "\"exists\" expected"; break;
+ case 103: s = "\"\\u2203\" expected"; break;
+ case 104: s = "\"::\" expected"; break;
+ case 105: s = "\"\\u2022\" expected"; break;
+ case 106: s = "??? expected"; break;
+ case 107: s = "invalid ClassMemberDecl"; break;
+ case 108: s = "invalid FunctionDecl"; break;
case 109: s = "invalid MethodDecl"; break;
- case 110: s = "invalid Expression"; break;
- case 111: s = "invalid TypeAndToken"; break;
- case 112: s = "invalid MethodSpec"; break;
+ case 110: s = "invalid MethodDecl"; break;
+ case 111: s = "invalid Expression"; break;
+ case 112: s = "invalid TypeAndToken"; break;
case 113: s = "invalid MethodSpec"; break;
- case 114: s = "invalid ReferenceType"; break;
- case 115: s = "invalid FunctionSpec"; break;
- case 116: s = "invalid FunctionBody"; break;
- case 117: s = "invalid PossiblyWildFrameExpression"; break;
- case 118: s = "invalid PossiblyWildExpression"; break;
- case 119: s = "invalid MatchOrExpr"; break;
- case 120: s = "invalid Stmt"; break;
- case 121: s = "invalid OneStmt"; break;
- case 122: s = "invalid IfStmt"; break;
- case 123: s = "invalid ForeachStmt"; break;
- case 124: s = "invalid AssignRhs"; break;
- case 125: s = "invalid SelectExpression"; break;
- case 126: s = "invalid Guard"; break;
- case 127: s = "invalid CallStmtSubExpr"; break;
- case 128: s = "invalid AttributeArg"; break;
- case 129: s = "invalid EquivOp"; break;
- case 130: s = "invalid ImpliesOp"; break;
- case 131: s = "invalid AndOp"; break;
- case 132: s = "invalid OrOp"; break;
- case 133: s = "invalid RelOp"; break;
- case 134: s = "invalid AddOp"; break;
- case 135: s = "invalid UnaryExpression"; break;
- case 136: s = "invalid MulOp"; break;
- case 137: s = "invalid NegOp"; break;
- case 138: s = "invalid ConstAtomExpression"; break;
- case 139: s = "invalid ObjectExpression"; break;
+ case 114: s = "invalid MethodSpec"; break;
+ case 115: s = "invalid ReferenceType"; break;
+ case 116: s = "invalid FunctionSpec"; break;
+ case 117: s = "invalid FunctionBody"; break;
+ case 118: s = "invalid PossiblyWildFrameExpression"; break;
+ case 119: s = "invalid PossiblyWildExpression"; break;
+ case 120: s = "invalid MatchOrExpr"; break;
+ case 121: s = "invalid Stmt"; break;
+ case 122: s = "invalid OneStmt"; break;
+ case 123: s = "invalid IfStmt"; break;
+ case 124: s = "invalid ForeachStmt"; break;
+ case 125: s = "invalid AssignRhs"; break;
+ case 126: s = "invalid SelectExpression"; break;
+ case 127: s = "invalid Guard"; break;
+ case 128: s = "invalid CallStmtSubExpr"; break;
+ case 129: s = "invalid AttributeArg"; break;
+ case 130: s = "invalid EquivOp"; break;
+ case 131: s = "invalid ImpliesOp"; break;
+ case 132: s = "invalid AndOp"; break;
+ case 133: s = "invalid OrOp"; break;
+ case 134: s = "invalid RelOp"; break;
+ case 135: s = "invalid AddOp"; break;
+ case 136: s = "invalid UnaryExpression"; break;
+ case 137: s = "invalid MulOp"; break;
+ case 138: s = "invalid NegOp"; break;
+ case 139: s = "invalid ConstAtomExpression"; break;
case 140: s = "invalid ObjectExpression"; break;
- case 141: s = "invalid SelectOrCallSuffix"; break;
+ case 141: s = "invalid ObjectExpression"; break;
case 142: s = "invalid SelectOrCallSuffix"; break;
case 143: s = "invalid SelectOrCallSuffix"; break;
- case 144: s = "invalid QuantifierGuts"; break;
- case 145: s = "invalid Forall"; break;
- case 146: s = "invalid Exists"; break;
- case 147: s = "invalid AttributeOrTrigger"; break;
- case 148: s = "invalid QSep"; break;
+ case 144: s = "invalid SelectOrCallSuffix"; break;
+ case 145: s = "invalid QuantifierGuts"; break;
+ case 146: s = "invalid Forall"; break;
+ case 147: s = "invalid Exists"; break;
+ case 148: s = "invalid AttributeOrTrigger"; break;
+ case 149: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2314,8 +2334,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/Dafny/Resolver.cs b/Dafny/Resolver.cs index 6fe3a3c1..22a58a39 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -281,7 +281,7 @@ namespace Microsoft.Dafny { foreach (MemberDecl member in cl.Members) {
member.EnclosingClass = cl;
if (member is Field) {
- ResolveType(((Field)member).Type);
+ ResolveType(member.tok, ((Field)member).Type);
} else if (member is Function) {
Function f = (Function)member;
@@ -581,9 +581,9 @@ namespace Microsoft.Dafny { if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
- ResolveType(p.Type);
+ ResolveType(p.tok, p.Type);
}
- ResolveType(f.ResultType);
+ ResolveType(f.tok, f.ResultType);
scope.PopMarker();
}
@@ -679,14 +679,14 @@ namespace Microsoft.Dafny { if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
- ResolveType(p.Type);
+ ResolveType(p.tok, p.Type);
}
// resolve out-parameters
foreach (Formal p in m.Outs) {
if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
- ResolveType(p.Type);
+ ResolveType(p.tok, p.Type);
}
scope.PopMarker();
}
@@ -756,21 +756,29 @@ namespace Microsoft.Dafny { if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
- ResolveType(p.Type);
+ ResolveType(p.tok, p.Type);
}
scope.PopMarker();
}
- public void ResolveType(Type type) {
+ public void ResolveType(IToken tok, Type type) {
Contract.Requires(type != null);
if (type is BasicType) {
// nothing to resolve
} else if (type is CollectionType) {
- ResolveType(((CollectionType)type).Arg);
+ var t = (CollectionType)type;
+ var argType = t.Arg;
+ ResolveType(tok, argType);
+ if (argType.IsSubrangeType) {
+ Error(tok, "sorry, cannot instantiate collection type with a subrange type");
+ }
} else if (type is UserDefinedType) {
UserDefinedType t = (UserDefinedType)type;
foreach (Type tt in t.TypeArgs) {
- ResolveType(tt);
+ ResolveType(t.tok, tt);
+ if (tt.IsSubrangeType) {
+ Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");
+ }
}
TypeParameter tp = allTypeParameters.Find(t.Name);
if (tp != null) {
@@ -793,7 +801,7 @@ namespace Microsoft.Dafny { } else if (type is TypeProxy) {
TypeProxy t = (TypeProxy)type;
if (t.T != null) {
- ResolveType(t.T);
+ ResolveType(tok, t.T);
}
} else {
@@ -965,8 +973,12 @@ namespace Microsoft.Dafny { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected proxy type
}
- // do the merge
- proxy.T = t;
+ // do the merge, but never infer a subrange type
+ if (t is NatType) {
+ proxy.T = Type.Int;
+ } else {
+ proxy.T = t;
+ }
return true;
}
@@ -1241,7 +1253,7 @@ namespace Microsoft.Dafny { } else if (stmt is VarDecl) {
VarDecl s = (VarDecl)stmt;
if (s.OptionalType != null) {
- ResolveType(s.OptionalType);
+ ResolveType(stmt.Tok, s.OptionalType);
s.type = s.OptionalType;
}
if (s.Rhs != null) {
@@ -1343,7 +1355,7 @@ namespace Microsoft.Dafny { scope.PushMarker();
bool b = scope.Push(s.BoundVar.Name, s.BoundVar);
Contract.Assert(b); // since we just pushed a marker, we expect the Push to succeed
- ResolveType(s.BoundVar.Type);
+ ResolveType(s.BoundVar.tok, s.BoundVar.Type);
int prevErrorCount = ErrorCount;
ResolveExpression(s.Range, true, true);
@@ -1437,7 +1449,7 @@ namespace Microsoft.Dafny { if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate parameter name: {0}", v.Name);
}
- ResolveType(v.Type);
+ ResolveType(v.tok, v.Type);
if (ctor != null && i < ctor.Formals.Count) {
Formal formal = ctor.Formals[i];
Type st = SubstType(formal.Type, subst);
@@ -1609,7 +1621,7 @@ namespace Microsoft.Dafny { Contract.Requires(method != null);
Contract.Ensures(Contract.Result<Type>() != null);
- ResolveType(rr.EType);
+ ResolveType(stmt.Tok, rr.EType);
if (rr.ArrayDimensions == null) {
if (!rr.EType.IsRefType) {
Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);
@@ -1619,6 +1631,9 @@ namespace Microsoft.Dafny { rr.Type = rr.EType;
} else {
int i = 0;
+ if (rr.EType.IsSubrangeType) {
+ Error(stmt, "sorry, cannot instantiate 'array' type with a subrange type");
+ }
foreach (Expression dim in rr.ArrayDimensions) {
Contract.Assert(dim != null);
ResolveExpression(dim, true, specContext);
@@ -1807,7 +1822,7 @@ namespace Microsoft.Dafny { subst.Add(dt.TypeArgs[i], t);
}
expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);
- ResolveType(expr.Type);
+ ResolveType(expr.tok, expr.Type);
DatatypeCtor ctor;
if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {
@@ -2196,7 +2211,7 @@ namespace Microsoft.Dafny { if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate bound-variable name: {0}", v.Name);
}
- ResolveType(v.Type);
+ ResolveType(v.tok, v.Type);
}
ResolveExpression(e.Body, twoState, specContext);
Contract.Assert(e.Body.Type != null); // follows from postcondition of ResolveExpression
@@ -2304,7 +2319,7 @@ namespace Microsoft.Dafny { if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate parameter name: {0}", v.Name);
}
- ResolveType(v.Type);
+ ResolveType(v.tok, v.Type);
if (ctor != null && i < ctor.Formals.Count) {
Formal formal = ctor.Formals[i];
Type st = SubstType(formal.Type, subst);
@@ -2360,7 +2375,7 @@ namespace Microsoft.Dafny { bounds.Add(new QuantifierExpr.BoolBoundedPool());
} else {
// Go through the conjuncts of the range expression look for bounds.
- Expression lowerBound = null;
+ Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;
Expression upperBound = null;
foreach (var conjunct in NormalizedConjuncts(e.Body, e is ExistsExpr)) {
var c = conjunct as BinaryExpr;
@@ -2388,7 +2403,7 @@ namespace Microsoft.Dafny { }
break;
case BinaryExpr.ResolvedOpcode.EqCommon:
- if (bv.Type == Type.Int) {
+ if (bv.Type is IntType) {
var otherOperand = whereIsBv == 0 ? e1 : e0;
bounds.Add(new QuantifierExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));
goto CHECK_NEXT_BOUND_VARIABLE;
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs index e3c84a73..2846e17a 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.
@@ -209,23 +211,24 @@ public class UTF8Buffer: Buffer { public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- 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);
-}
+ const int maxT = 106;
+ const int noSym = 106;
+
+
+ [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;
@@ -291,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;
@@ -303,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);
@@ -320,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;
@@ -344,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;
@@ -359,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++;
@@ -367,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
@@ -419,7 +420,7 @@ void objectInvariant(){ return;
}
-
+
}
}
@@ -506,41 +507,42 @@ void objectInvariant(){ case "ensures": t.kind = 28; break;
case "decreases": t.kind = 29; break;
case "bool": t.kind = 32; break;
- case "int": t.kind = 33; break;
- case "set": t.kind = 34; break;
- case "seq": t.kind = 35; break;
- case "object": t.kind = 36; break;
- case "function": t.kind = 37; break;
- case "reads": t.kind = 38; break;
- case "match": t.kind = 41; break;
- case "case": t.kind = 42; 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 "while": t.kind = 56; break;
- case "invariant": t.kind = 57; break;
- case "call": t.kind = 58; break;
- case "foreach": t.kind = 59; break;
- case "in": t.kind = 60; break;
- case "assert": t.kind = 62; break;
- case "assume": t.kind = 63; break;
- case "use": t.kind = 64; break;
- case "print": t.kind = 65; break;
- case "then": t.kind = 66; break;
- case "false": t.kind = 90; break;
- case "true": t.kind = 91; break;
- case "null": t.kind = 92; break;
- case "fresh": t.kind = 94; break;
- case "allocated": t.kind = 95; break;
- case "this": t.kind = 97; break;
- case "old": t.kind = 98; break;
- case "forall": t.kind = 99; break;
- case "exists": t.kind = 101; break;
+ case "nat": t.kind = 33; break;
+ case "int": t.kind = 34; break;
+ case "set": t.kind = 35; break;
+ case "seq": t.kind = 36; break;
+ case "object": t.kind = 37; break;
+ case "function": t.kind = 38; break;
+ case "reads": t.kind = 39; break;
+ case "match": t.kind = 42; break;
+ case "case": t.kind = 43; 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 "while": t.kind = 57; break;
+ case "invariant": t.kind = 58; break;
+ case "call": t.kind = 59; break;
+ case "foreach": t.kind = 60; break;
+ case "in": t.kind = 61; break;
+ case "assert": t.kind = 63; break;
+ case "assume": t.kind = 64; break;
+ case "use": t.kind = 65; break;
+ case "print": t.kind = 66; break;
+ case "then": t.kind = 67; break;
+ case "false": t.kind = 91; break;
+ case "true": t.kind = 92; break;
+ case "null": t.kind = 93; break;
+ case "fresh": t.kind = 95; break;
+ case "allocated": t.kind = 96; break;
+ case "this": t.kind = 98; break;
+ case "old": t.kind = 99; break;
+ case "forall": t.kind = 100; break;
+ case "exists": t.kind = 102; break;
default: break;
}
}
@@ -557,10 +559,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: {
@@ -651,78 +656,78 @@ void objectInvariant(){ case 22:
{t.kind = 31; break;}
case 23:
- {t.kind = 39; break;}
- case 24:
{t.kind = 40; break;}
+ case 24:
+ {t.kind = 41; break;}
case 25:
- {t.kind = 43; break;}
+ {t.kind = 44; break;}
case 26:
- {t.kind = 47; break;}
+ {t.kind = 48; break;}
case 27:
- {t.kind = 49; break;}
- case 28:
{t.kind = 50; break;}
+ case 28:
+ {t.kind = 51; break;}
case 29:
if (ch == '>') {AddCh(); goto case 30;}
else {goto case 0;}
case 30:
- {t.kind = 67; break;}
- case 31:
{t.kind = 68; break;}
- case 32:
+ case 31:
{t.kind = 69; break;}
- case 33:
+ case 32:
{t.kind = 70; break;}
+ case 33:
+ {t.kind = 71; break;}
case 34:
if (ch == '&') {AddCh(); goto case 35;}
else {goto case 0;}
case 35:
- {t.kind = 71; break;}
- case 36:
{t.kind = 72; break;}
- case 37:
+ case 36:
{t.kind = 73; break;}
- case 38:
+ case 37:
{t.kind = 74; break;}
+ case 38:
+ {t.kind = 75; break;}
case 39:
- {t.kind = 77; break;}
- case 40:
{t.kind = 78; break;}
- case 41:
+ case 40:
{t.kind = 79; break;}
+ case 41:
+ {t.kind = 80; break;}
case 42:
if (ch == 'n') {AddCh(); goto case 43;}
else {goto case 0;}
case 43:
- {t.kind = 80; break;}
- case 44:
{t.kind = 81; break;}
- case 45:
+ case 44:
{t.kind = 82; break;}
- case 46:
+ case 45:
{t.kind = 83; break;}
- case 47:
+ case 46:
{t.kind = 84; break;}
- case 48:
+ case 47:
{t.kind = 85; break;}
- case 49:
+ case 48:
{t.kind = 86; break;}
- case 50:
+ case 49:
{t.kind = 87; break;}
+ case 50:
+ {t.kind = 88; break;}
case 51:
- {t.kind = 89; break;}
+ {t.kind = 90; break;}
case 52:
- {t.kind = 93; break;}
+ {t.kind = 94; break;}
case 53:
- {t.kind = 96; break;}
+ {t.kind = 97; break;}
case 54:
- {t.kind = 100; break;}
+ {t.kind = 101; break;}
case 55:
- {t.kind = 102; break;}
- case 56:
{t.kind = 103; break;}
- case 57:
+ case 56:
{t.kind = 104; break;}
+ case 57:
+ {t.kind = 105; break;}
case 58:
recEnd = pos; recKind = 20;
if (ch == '=') {AddCh(); goto case 26;}
@@ -741,40 +746,40 @@ void objectInvariant(){ else if (ch == '=') {AddCh(); goto case 66;}
else {goto case 0;}
case 62:
- recEnd = pos; recKind = 51;
+ recEnd = pos; recKind = 52;
if (ch == '.') {AddCh(); goto case 53;}
- else {t.kind = 51; break;}
+ else {t.kind = 52; break;}
case 63:
- recEnd = pos; recKind = 61;
+ recEnd = pos; recKind = 62;
if (ch == '|') {AddCh(); goto case 37;}
- else {t.kind = 61; break;}
+ else {t.kind = 62; break;}
case 64:
- recEnd = pos; recKind = 88;
+ recEnd = pos; recKind = 89;
if (ch == '=') {AddCh(); goto case 40;}
else if (ch == '!') {AddCh(); goto case 41;}
else if (ch == 'i') {AddCh(); goto case 42;}
- else {t.kind = 88; break;}
+ else {t.kind = 89; break;}
case 65:
- recEnd = pos; recKind = 76;
+ recEnd = pos; recKind = 77;
if (ch == '=') {AddCh(); goto case 29;}
- else {t.kind = 76; break;}
+ else {t.kind = 77; break;}
case 66:
- recEnd = pos; recKind = 75;
+ recEnd = pos; recKind = 76;
if (ch == '>') {AddCh(); goto case 32;}
- 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);
@@ -795,7 +800,7 @@ void objectInvariant(){ }
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 33b6d39d..2bb5a51e 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -960,7 +960,7 @@ namespace Microsoft.Dafny { } else {
// check well-formedness of the preconditions, and then assume each one of them
foreach (MaybeFreeExpression p in m.Req) {
- CheckWellformed(p.E, new WFOptions(), null, localVariables, builder, etran);
+ CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
// Note: the modifies clauses are not checked for well-formedness (is that sound?), because it used to
@@ -968,7 +968,7 @@ namespace Microsoft.Dafny { // absolutely well-defined.
// check well-formedness of the decreases clauses
foreach (Expression p in m.Decreases) {
- CheckWellformed(p, new WFOptions(), null, localVariables, builder, etran);
+ CheckWellformed(p, new WFOptions(), localVariables, builder, etran);
}
// play havoc with the heap according to the modifies clause
@@ -992,7 +992,7 @@ namespace Microsoft.Dafny { // check wellformedness of postconditions
foreach (MaybeFreeExpression p in m.Ens) {
- CheckWellformed(p.E, new WFOptions(), null, localVariables, builder, etran);
+ CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
}
@@ -1292,7 +1292,7 @@ namespace Microsoft.Dafny { // check well-formedness of the preconditions (including termination, but no reads checks), and then
// assume each one of them
foreach (Expression p in f.Req) {
- CheckWellformed(p, new WFOptions(f, null, false), null, locals, builder, etran);
+ CheckWellformed(p, new WFOptions(f, null, false), locals, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));
}
// Note: the reads clauses are not checked for well-formedness (is that sound?), because it used to
@@ -1300,7 +1300,7 @@ namespace Microsoft.Dafny { // absolutely well-defined.
// check well-formedness of the decreases clauses (including termination, but no reads checks)
foreach (Expression p in f.Decreases) {
- CheckWellformed(p, new WFOptions(f, null, false), null, locals, builder, etran);
+ CheckWellformed(p, new WFOptions(f, null, false), locals, builder, etran);
}
// Generate:
// if (*) {
@@ -1311,7 +1311,7 @@ namespace Microsoft.Dafny { // Here go the postconditions (termination checks included, but no reads checks)
StmtListBuilder postCheckBuilder = new StmtListBuilder();
foreach (Expression p in f.Ens) {
- CheckWellformed(p, new WFOptions(f, f, false), null, locals, postCheckBuilder, etran);
+ CheckWellformed(p, new WFOptions(f, f, false), locals, postCheckBuilder, etran);
// assume the postcondition for the benefit of checking the remaining postconditions
postCheckBuilder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));
}
@@ -1327,7 +1327,7 @@ namespace Microsoft.Dafny { Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals);
- CheckWellformed(f.Body, new WFOptions(f, null, true), funcAppl, locals, bodyCheckBuilder, etran);
+ CheckWellformedWithResult(f.Body, new WFOptions(f, null, true), funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);
// check that postconditions hold
foreach (Expression p in f.Ens) {
@@ -1443,7 +1443,12 @@ namespace Microsoft.Dafny { // create a substitution map from each formal parameter to the corresponding actual parameter
Dictionary<IVariable,Expression> substMap = new Dictionary<IVariable,Expression>();
for (int i = 0; i < e.Function.Formals.Count; i++) {
- substMap.Add(e.Function.Formals[i], e.Args[i]);
+ var formal = e.Function.Formals[i];
+ var s = CheckSubrange_Expr(e.Args[i].tok, etran.TrExpr(e.Args[i]), formal.Type);
+ if (s != null) {
+ r = BplAnd(r, s);
+ }
+ substMap.Add(formal, e.Args[i]);
}
// check that the preconditions for the call hold
foreach (Expression p in e.Function.Req) {
@@ -1453,7 +1458,16 @@ namespace Microsoft.Dafny { return r;
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
- return IsTotal(dtv.Arguments, etran);
+ var r = IsTotal(dtv.Arguments, etran);
+ for (int i = 0; i < dtv.Ctor.Formals.Count; i++) {
+ var formal = dtv.Ctor.Formals[i];
+ var arg = dtv.Arguments[i];
+ var s = CheckSubrange_Expr(arg.tok, etran.TrExpr(arg), formal.Type);
+ if (s != null) {
+ r = BplAnd(r, s);
+ }
+ }
+ return r;
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
return new Bpl.OldExpr(expr.tok, IsTotal(e.E, etran));
@@ -1727,10 +1741,14 @@ namespace Microsoft.Dafny { args.Add(Bpl.Expr.Literal(0));
kv = new Bpl.QKeyValue(expr.tok, "subsumption", args, null);
}
- CheckWellformed(expr, new WFOptions(kv), null, locals, builder, etran);
+ CheckWellformed(expr, new WFOptions(kv), locals, builder, etran);
builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran)));
}
+ void CheckWellformed(Expression expr, WFOptions options, Bpl.VariableSeq locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {
+ CheckWellformedWithResult(expr, options, null, null, locals, builder, etran);
+ }
+
/// <summary>
/// Adds to "builder" code that checks the well-formedness of "expr". Any local variables introduced
/// in this code are added to "locals".
@@ -1738,9 +1756,11 @@ namespace Microsoft.Dafny { /// assume the equivalent of "result == expr".
/// See class WFOptions for descriptions of the specified options.
/// </summary>
- void CheckWellformed(Expression expr, WFOptions options, Bpl.Expr result, Bpl.VariableSeq locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {
+ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr result, Type resultType,
+ Bpl.VariableSeq locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {
Contract.Requires(expr != null);
Contract.Requires(options != null);
+ Contract.Requires((result == null) == (resultType == null));
Contract.Requires(locals != null);
Contract.Requires(builder != null);
Contract.Requires(etran != null);
@@ -1751,11 +1771,11 @@ namespace Microsoft.Dafny { } else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
foreach (Expression el in e.Elements) {
- CheckWellformed(el, options, null, locals, builder, etran);
+ CheckWellformed(el, options, locals, builder, etran);
}
} else if (expr is FieldSelectExpr) {
FieldSelectExpr e = (FieldSelectExpr)expr;
- CheckWellformed(e.Obj, options, null, locals, builder, etran);
+ CheckWellformed(e.Obj, options, locals, builder, etran);
CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv);
if (options.DoReadsChecks && e.Field.IsMutable) {
builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field", options.AssertKv));
@@ -1763,16 +1783,16 @@ namespace Microsoft.Dafny { } else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
bool isSequence = e.Seq.Type is SeqType;
- CheckWellformed(e.Seq, options, null, locals, builder, etran);
+ CheckWellformed(e.Seq, options, locals, builder, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr e0 = null;
if (e.E0 != null) {
e0 = etran.TrExpr(e.E0);
- CheckWellformed(e.E0, options, null, locals, builder, etran);
+ CheckWellformed(e.E0, options, locals, builder, etran);
builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne), "index out of range", options.AssertKv));
}
if (e.E1 != null) {
- CheckWellformed(e.E1, options, null, locals, builder, etran);
+ CheckWellformed(e.E1, options, locals, builder, etran);
builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "end-of-range beyond length of " + (isSequence ? "sequence" : "array"), options.AssertKv));
}
if (options.DoReadsChecks && cce.NonNull(e.Seq.Type).IsArrayType) {
@@ -1782,11 +1802,11 @@ namespace Microsoft.Dafny { }
} else if (expr is MultiSelectExpr) {
MultiSelectExpr e = (MultiSelectExpr)expr;
- CheckWellformed(e.Array, options, null, locals, builder, etran);
+ CheckWellformed(e.Array, options, locals, builder, etran);
Bpl.Expr array = etran.TrExpr(e.Array);
int i = 0;
foreach (Expression idx in e.Indices) {
- CheckWellformed(idx, options, null, locals, builder, etran);
+ CheckWellformed(idx, options, locals, builder, etran);
Bpl.Expr index = etran.TrExpr(idx);
Bpl.Expr lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);
@@ -1797,23 +1817,23 @@ namespace Microsoft.Dafny { }
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
- CheckWellformed(e.Seq, options, null, locals, builder, etran);
+ CheckWellformed(e.Seq, options, locals, builder, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr index = etran.TrExpr(e.Index);
- CheckWellformed(e.Index, options, null, locals, builder, etran);
+ CheckWellformed(e.Index, options, locals, builder, etran);
builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range", options.AssertKv));
- CheckWellformed(e.Value, options, null, locals, builder, etran);
+ CheckWellformed(e.Value, options, locals, builder, etran);
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
Contract.Assert(e.Function != null); // follows from the fact that expr has been successfully resolved
// check well-formedness of receiver
- CheckWellformed(e.Receiver, options, null, locals, builder, etran);
+ CheckWellformed(e.Receiver, options, locals, builder, etran);
if (!e.Function.IsStatic && !(e.Receiver is ThisExpr)) {
CheckNonNull(expr.tok, e.Receiver, builder, etran, options.AssertKv);
}
// check well-formedness of the other parameters
foreach (Expression arg in e.Args) {
- CheckWellformed(arg, options, null, locals, builder, etran);
+ CheckWellformed(arg, options, locals, builder, etran);
}
// create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
Dictionary<IVariable,Expression> substMap = new Dictionary<IVariable,Expression>();
@@ -1827,6 +1847,7 @@ namespace Microsoft.Dafny { locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
Expression ee = e.Args[i];
+ CheckSubrange(ee.tok, etran.TrExpr(ee), p.Type, builder);
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), p.Type));
builder.Add(cmd);
}
@@ -1893,21 +1914,24 @@ namespace Microsoft.Dafny { } else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
- foreach (Expression arg in dtv.Arguments) {
- CheckWellformed(arg, options, null, locals, builder, etran);
+ for (int i = 0; i < dtv.Ctor.Formals.Count; i++) {
+ var formal = dtv.Ctor.Formals[i];
+ var arg = dtv.Arguments[i];
+ CheckWellformed(arg, options, locals, builder, etran);
+ CheckSubrange(arg.tok, etran.TrExpr(arg), formal.Type, builder);
}
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
- CheckWellformed(e.E, options, null, locals, builder, etran.Old);
+ CheckWellformed(e.E, options, locals, builder, etran.Old);
} else if (expr is FreshExpr) {
FreshExpr e = (FreshExpr)expr;
- CheckWellformed(e.E, options, null, locals, builder, etran);
+ CheckWellformed(e.E, options, locals, builder, etran);
} else if (expr is AllocatedExpr) {
AllocatedExpr e = (AllocatedExpr)expr;
- CheckWellformed(e.E, options, null, locals, builder, etran);
+ CheckWellformed(e.E, options, locals, builder, etran);
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
- CheckWellformed(e.E, options, null, locals, builder, etran);
+ CheckWellformed(e.E, options, locals, builder, etran);
if (e.Op == UnaryExpr.Opcode.SetChoose) {
Bpl.Expr emptySet = FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E), emptySet), "choose is defined only on nonempty sets"));
@@ -1916,30 +1940,30 @@ namespace Microsoft.Dafny { }
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
- CheckWellformed(e.E0, options, null, locals, builder, etran);
+ CheckWellformed(e.E0, options, locals, builder, etran);
switch (e.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.And:
case BinaryExpr.ResolvedOpcode.Imp:
{
Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
- CheckWellformed(e.E1, options, null, locals, b, etran);
+ CheckWellformed(e.E1, options, locals, b, etran);
builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.E0), b.Collect(expr.tok), null, null));
}
break;
case BinaryExpr.ResolvedOpcode.Or:
{
Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
- CheckWellformed(e.E1, options, null, locals, b, etran);
+ CheckWellformed(e.E1, options, locals, b, etran);
builder.Add(new Bpl.IfCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)), b.Collect(expr.tok), null, null));
}
break;
case BinaryExpr.ResolvedOpcode.Div:
case BinaryExpr.ResolvedOpcode.Mod:
- CheckWellformed(e.E1, options, null, locals, builder, etran);
+ CheckWellformed(e.E1, options, locals, builder, etran);
builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), Bpl.Expr.Literal(0)), "possible division by zero", options.AssertKv));
break;
default:
- CheckWellformed(e.E1, options, null, locals, builder, etran);
+ CheckWellformed(e.E1, options, locals, builder, etran);
break;
}
@@ -1960,20 +1984,20 @@ namespace Microsoft.Dafny { }
}
Expression body = Substitute(e.Body, null, substMap);
- CheckWellformed(body, options, null, locals, builder, etran);
+ CheckWellformed(body, options, locals, builder, etran);
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
- CheckWellformed(e.Test, options, null, locals, builder, etran);
+ CheckWellformed(e.Test, options, locals, builder, etran);
Bpl.StmtListBuilder bThen = new Bpl.StmtListBuilder();
Bpl.StmtListBuilder bElse = new Bpl.StmtListBuilder();
- CheckWellformed(e.Thn, options, null, locals, bThen, etran);
- CheckWellformed(e.Els, options, null, locals, bElse, etran);
+ CheckWellformed(e.Thn, options, locals, bThen, etran);
+ CheckWellformed(e.Els, options, locals, bElse, etran);
builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.Test), bThen.Collect(expr.tok), null, bElse.Collect(expr.tok)));
} else if (expr is MatchExpr) {
MatchExpr me = (MatchExpr)expr;
- CheckWellformed(me.Source, options, null, locals, builder, etran);
+ CheckWellformed(me.Source, options, locals, builder, etran);
Bpl.Expr src = etran.TrExpr(me.Source);
Bpl.IfCmd ifcmd = null;
StmtListBuilder elsBldr = new StmtListBuilder();
@@ -1984,7 +2008,7 @@ namespace Microsoft.Dafny { Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
Bpl.Expr ct = CtorInvocation(mc, etran, locals, b);
// generate: if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ...
- CheckWellformed(mc.Body, options, result, locals, b, etran);
+ CheckWellformedWithResult(mc.Body, options, result, resultType, locals, b, etran);
ifcmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifcmd, els);
els = null;
}
@@ -1996,7 +2020,10 @@ namespace Microsoft.Dafny { }
if (result != null) {
- builder.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Eq(result, etran.TrExpr(expr))));
+ Contract.Assert(resultType != null);
+ var bResult = etran.TrExpr(expr);
+ CheckSubrange(expr.tok, bResult, resultType, builder);
+ builder.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Eq(result, bResult)));
builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran)));
}
}
@@ -3250,7 +3277,9 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
Expression actual = s.Args[i];
TrStmt_CheckWellformed(actual, builder, locals, etran, true);
- Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(s.Tok, etran.TrExpr(actual), cce.NonNull(actual.Type), s.Method.Ins[i].Type));
+ var bActual = etran.TrExpr(actual);
+ CheckSubrange(actual.tok, bActual, p.Type, builder);
+ Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(s.Tok, bActual, cce.NonNull(actual.Type), s.Method.Ins[i].Type));
builder.Add(cmd);
ins.Add(lhs);
}
@@ -3611,7 +3640,12 @@ namespace Microsoft.Dafny { }
}
- if (type is BoolType || type is IntType) {
+ if (type is NatType) {
+ // nat:
+ // 0 <= x
+ return Bpl.Expr.Le(Bpl.Expr.Literal(0), x);
+
+ } else if (type is BoolType || type is IntType) {
// nothing todo
} else if (type is SetType) {
@@ -3684,7 +3718,7 @@ namespace Microsoft.Dafny { if (lhs is IdentifierExpr) {
var bLhs = (Bpl.IdentifierExpr)etran.TrExpr(lhs); // TODO: is this cast always justified?
- TrAssignmentRhs(tok, bLhs, lhs.Type, rhs, builder, locals, etran);
+ TrAssignmentRhs(tok, bLhs, lhs.Type, rhs, lhs.Type, builder, locals, etran);
} else if (lhs is FieldSelectExpr) {
var fse = (FieldSelectExpr)lhs;
@@ -3693,7 +3727,7 @@ namespace Microsoft.Dafny { // check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj]);
builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing method's modifies clause"));
- Bpl.Expr bRhs = TrAssignmentRhs(tok, null, fse.Field.Type, rhs, builder, locals, etran);
+ Bpl.Expr bRhs = TrAssignmentRhs(tok, null, fse.Field.Type, rhs, lhs.Type, builder, locals, etran);
var h = (Bpl.IdentifierExpr)etran.HeapExpr; // TODO: is this cast always justified?
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, new Bpl.IdentifierExpr(tok, GetField(fse.Field)), bRhs));
@@ -3711,7 +3745,7 @@ namespace Microsoft.Dafny { // check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj,index]);
builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
- Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, builder, locals, etran);
+ Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, lhs.Type, builder, locals, etran);
var h = (Bpl.IdentifierExpr)etran.HeapExpr; // TODO: is this cast always justified?
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, bRhs));
@@ -3733,7 +3767,7 @@ namespace Microsoft.Dafny { Bpl.Expr q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(ante, cons));
builder.Add(Assert(tok, q, "assignment may update an array element not in the enclosing method's modifies clause"));
// compute the RHS
- Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, builder, locals, etran);
+ Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, lhs.Type, builder, locals, etran);
// do the update: call UpdateArrayRange(arr, low, high, rhs);
builder.Add(new Bpl.CallCmd(tok, "UpdateArrayRange",
new Bpl.ExprSeq(obj, low, high, bRhs),
@@ -3748,7 +3782,7 @@ namespace Microsoft.Dafny { var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhs, "$index", predef.FieldName(mse.tok, predef.BoxType), builder, locals);
builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
- Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, builder, locals, etran);
+ Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, lhs.Type, builder, locals, etran);
var h = (Bpl.IdentifierExpr)etran.HeapExpr; // TODO: is this cast always justified?
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, bRhs));
@@ -3763,8 +3797,10 @@ namespace Microsoft.Dafny { /// <summary>
/// Generates an assignment of the translation of "rhs" to "bLhs" and then return "bLhs". If "bLhs" is
/// passed in as "null", this method will create a new temporary Boogie variable to hold the result.
+ /// Before the assignment, the generated code will check that "rhs" obeys any subrange requirements
+ /// entailed by "checkSubrangeType".
/// </summary>
- Bpl.IdentifierExpr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bLhs, Type lhsType, AssignmentRhs rhs,
+ Bpl.IdentifierExpr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bLhs, Type lhsType, AssignmentRhs rhs, Type checkSubrangeType,
Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {
Contract.Requires(tok != null);
Contract.Requires(rhs != null);
@@ -3787,6 +3823,7 @@ namespace Microsoft.Dafny { TrStmt_CheckWellformed(e.Expr, builder, locals, etran, true);
Bpl.Expr bRhs = etran.TrExpr(e.Expr);
+ CheckSubrange(tok, bRhs, checkSubrangeType, builder);
bRhs = etran.CondApplyBox(tok, bRhs, e.Expr.Type, lhsType);
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, bRhs);
@@ -3807,7 +3844,7 @@ namespace Microsoft.Dafny { if (tRhs.ArrayDimensions != null) {
int i = 0;
foreach (Expression dim in tRhs.ArrayDimensions) {
- CheckWellformed(dim, new WFOptions(), null, locals, builder, etran);
+ CheckWellformed(dim, new WFOptions(), locals, builder, etran);
if (tRhs.ArrayDimensions.Count == 1) {
builder.Add(Assert(tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(dim)),
tRhs.ArrayDimensions.Count == 1 ? "array size might be negative" : string.Format("array size (dimension {0}) might be negative", i)));
@@ -3857,6 +3894,29 @@ namespace Microsoft.Dafny { return bLhs;
}
+ void CheckSubrange(IToken tok, Expr bRhs, Type tp, StmtListBuilder builder) {
+ Contract.Requires(tok != null);
+ Contract.Requires(bRhs != null);
+ Contract.Requires(tp != null);
+ Contract.Requires(builder != null);
+
+ var isNat = CheckSubrange_Expr(tok, bRhs, tp);
+ if (isNat != null) {
+ builder.Add(Assert(tok, isNat, "value assigned to a nat must be non-negative"));
+ }
+ }
+
+ Bpl.Expr CheckSubrange_Expr(IToken tok, Expr bRhs, Type tp) {
+ Contract.Requires(tok != null);
+ Contract.Requires(bRhs != null);
+ Contract.Requires(tp != null);
+
+ if (tp is NatType) {
+ return Bpl.Expr.Le(Bpl.Expr.Literal(0), bRhs);
+ }
+ return null;
+ }
+
Bpl.AssumeCmd AssumeGoodHeap(IToken tok, ExpressionTranslator etran) {
Contract.Requires(tok != null);
Contract.Requires(etran != null);
@@ -4163,7 +4223,8 @@ namespace Microsoft.Dafny { for (int i = 0; i < dtv.Arguments.Count; i++) {
Expression arg = dtv.Arguments[i];
Type t = dtv.Ctor.Formals[i].Type;
- args.Add(CondApplyBox(expr.tok, TrExpr(arg), cce.NonNull(arg.Type), t));
+ var bArg = TrExpr(arg);
+ args.Add(CondApplyBox(expr.tok, bArg, cce.NonNull(arg.Type), t));
}
Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(dtv.tok, dtv.Ctor.FullName, predef.DatatypeType);
return new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index eb85403e..1ac8fc1c 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -65,6 +65,7 @@ class C { Dafny program verifier finished with 0 verified, 0 errors
-------------------- TypeTests.dfy --------------------
+TypeTests.dfy(95,9): Error: sorry, cannot instantiate collection type with a subrange type
TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
@@ -83,7 +84,52 @@ TypeTests.dfy(79,17): Error: member F in class C does not refer to a method TypeTests.dfy(80,17): Error: a method called as an initialization method must not have any result arguments
TypeTests.dfy(89,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
TypeTests.dfy(90,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
-18 resolution/type errors detected in TypeTests.dfy
+TypeTests.dfy(96,9): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(97,6): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(98,6): Error: sorry, cannot instantiate 'array' type with a subrange type
+22 resolution/type errors detected in TypeTests.dfy
+
+-------------------- NatTypes.dfy --------------------
+NatTypes.dfy(7,10): Error: value assigned to a nat must be non-negative
+Execution trace:
+ (0,0): anon0
+NatTypes.dfy(31,5): Error: value assigned to a nat must be non-negative
+Execution trace:
+ (0,0): anon0
+ NatTypes.dfy(19,3): anon10_LoopHead
+ (0,0): anon10_LoopBody
+ NatTypes.dfy(19,3): anon11_Else
+ (0,0): anon3
+ (0,0): anon12_Then
+ (0,0): anon9
+NatTypes.dfy(38,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
+NatTypes.dfy(40,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
+NatTypes.dfy(54,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+NatTypes.dfy(71,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Then
+NatTypes.dfy(89,9): Error: value assigned to a nat must be non-negative
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative
+Execution trace:
+ (0,0): anon6_Else
+ (0,0): anon7_Else
+ (0,0): anon8_Then
+
+Dafny program verifier finished with 12 verified, 8 errors
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy new file mode 100644 index 00000000..93bd4b65 --- /dev/null +++ b/Test/dafny0/NatTypes.dfy @@ -0,0 +1,110 @@ +method M(n: nat) {
+ assert 0 <= n;
+}
+
+method Main() {
+ call M(25);
+ call M(-25); // error: cannot pass -25 as a nat
+}
+
+var f: nat;
+
+method CheckField(x: nat, y: int)
+ requires 0 <= y;
+ modifies this;
+{
+ var y: nat := y;
+
+ assert 0 <= f;
+ while (0 < y)
+ {
+ f := f + 1;
+ if (15 < f) {
+ f := f - 12;
+ }
+ y := y - 1;
+ }
+ assert 0 <= f;
+
+ f := x; // no problem
+ f := x + 3; // no problem here either
+ f := x - 3; // error: cannot prove RHS is a nat
+}
+
+method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
+ if (0 < i) {
+ var n: nat := 5;
+ call j := Generic(i-1, n, -4);
+ assert 0 <= j; // error: the result is an int, not a nat
+ var q := FenEric(n, -4);
+ assert 0 <= q; // error: the result is an int, not a nat
+ }
+ r := t1;
+}
+
+function method FenEric<T>(t0: T, t1: T): T;
+
+datatype Pair<T> { Pr(T, T); }
+
+method K(n: nat, i: int) {
+ match (#Pair.Pr(n, i)) {
+ case Pr(k, l) =>
+ assert k == n; // fine: although the type of k is int, we know it's equal to n
+ assert 0 <= k;
+ assert 0 <= l; // error: l is an int
+ }
+}
+
+datatype List<T> {
+ Nil;
+ Cons(nat, T, List<T>);
+}
+
+method MatchIt(list: List<bool>) returns (k: nat)
+{
+ match (list) {
+ case Nil =>
+ case Cons(n, extra, tail) =>
+ call w := MatchIt(tail);
+ assert 0 <= w;
+ assert 0 <= n; // fine
+ assert 0 <= n - 10; // error: possible assertion failure
+ }
+
+ var m := Sum(list);
+ assert 0 <= m;
+ k := m;
+}
+
+class GenEric<T> {
+ var f: T;
+}
+
+function method GE<T>(d: GenEric<T>): bool { true }
+
+method TestGenEric() {
+ var ge;
+ if (ge != null) {
+ var b := GE(ge);
+ var n: nat := ge.f; // error: the generic instantiation uses int, not nat
+ }
+}
+
+function method Sum(list: List<object>): nat
+{
+ match list
+ case Nil => 0
+ case Cons(x, y, tail) => x + Sum(tail)
+}
+
+function BadSum(list: List<object>): nat
+{
+ match list
+ case Nil => 0
+ case Cons(x, y, tail) => x + BadSum(tail) - 30 // error: may not be a nat
+}
+
+function Abs(x: int): nat
+{
+ if 0 <= x then x else -x
+}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 93c4aec4..792c8fac 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -89,3 +89,12 @@ method ArrayRangeAssignments(a: array<C>) a[0..5] := new C; // this is not allowed
havoc a[1..4]; // this is not allowed
}
+
+// --------------------- tests of restrictions on subranges (nat)
+
+method K(s: set<nat>) { // error: not allowed to instantiate 'set' with 'nat'
+ var d: MutuallyRecursiveDataType<nat>; // error: not allowed to instantiate with 'nat'
+ var a := new nat[100]; // error: not allowed the type array<nat>
+ var b := new nat[100,200]; // error: not allowed the type array2<nat>
+}
+
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 6a2f2cb5..491b7b75 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -11,7 +11,8 @@ for %%f in (Simple.dfy) do ( %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f
)
-for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.dfy
+for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
+ FunctionSpecifications.dfy
Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy
Modules0.dfy Modules1.dfy BadFunction.dfy
Termination.dfy Use.dfy DTypes.dfy
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index a0f5f34c..818d7dc3 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -39,7 +39,7 @@ "assert" "assume" "break" "call" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print"
"old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "allocated" "use"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
- `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "int" "object" "set" "seq")) . font-lock-type-face)
+ `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "nat" "int" "object" "set" "seq")) . font-lock-type-face)
)
"Minimal highlighting for Dafny mode")
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 80082ec9..3302d368 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -22,7 +22,7 @@ namespace Demo "call", "if", "then", "else", "while", "invariant",
"break", "label", "return", "foreach", "havoc", "print", "use",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
- "int", "bool", "false", "true", "null",
+ "bool", "nat", "int", "false", "true", "null",
"function", "free",
"in", "forall", "exists",
"seq", "set", "array", "array2", "array3",
@@ -317,8 +317,9 @@ namespace Demo | "modifies"
| "reads"
| "decreases"
- | "int"
| "bool"
+ | "nat"
+ | "int"
| "false"
| "true"
| "null"
@@ -381,7 +382,7 @@ namespace Demo ;
typeDecl.Rule
- = (ToTerm("int") | "bool" | ident | "seq" | "set" | "array") + (("<" + MakePlusRule(typeDecl, ToTerm(","), typeDecl) + ">") | Empty)
+ = (ToTerm("int") | "nat" | "bool" | ident | "seq" | "set" | "array") + (("<" + MakePlusRule(typeDecl, ToTerm(","), typeDecl) + ">") | Empty)
| ToTerm("token") + "<" + (typeDecl + ".") + ident + ">"
;
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 30e44a90..c37ea13c 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -267,6 +267,7 @@ namespace DafnyLanguage case "method":
case "modifies":
case "module":
+ case "nat":
case "new":
case "null":
case "object":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 4a98fa4c..fccd3918 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -5,7 +5,7 @@ \usepackage{listings}
\lstdefinelanguage{dafny}{
- morekeywords={class,datatype,bool,int,object,set,seq,array,array2,array3,%
+ 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,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index bdf35f2e..7727e1f6 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -11,7 +11,7 @@ syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat foreach while syntax keyword dafnyStatement havoc assume assert return call new print break label syntax keyword dafnyKeyword var ghost returns null static this refines replaces by -syntax keyword dafnyType int bool seq set object array array2 array3 +syntax keyword dafnyType bool nat int seq set object array array2 array3 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant syntax keyword dafnyOperator forall exists old fresh allocated choose syntax keyword dafnyBoolean true false |