summaryrefslogtreecommitdiff
path: root/Dafny
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-04-19 16:48:32 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-04-19 16:48:32 -0700
commita0ccbb8461b68eb4a61ba78e0efced94423e93c7 (patch)
tree41bd0df0cf2afbb78c7cd7f500840397fe332269 /Dafny
parent9313173a5462dd6bf0ac386c6ac129d6284e9f4d (diff)
Dafny: added type "nat"
Diffstat (limited to 'Dafny')
-rw-r--r--Dafny/Dafny.atg1
-rw-r--r--Dafny/DafnyAst.cs20
-rw-r--r--Dafny/Parser.cs685
-rw-r--r--Dafny/Resolver.cs57
-rw-r--r--Dafny/Scanner.cs265
-rw-r--r--Dafny/Translator.cs163
6 files changed, 653 insertions, 538 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);
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-21 23:00:37 +0000