summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Dafny/Dafny.atg10
-rw-r--r--Dafny/DafnyAst.ssc22
-rw-r--r--Dafny/Parser.ssc421
-rw-r--r--Dafny/Printer.ssc2
-rw-r--r--Dafny/Resolver.ssc25
-rw-r--r--Dafny/Scanner.ssc89
-rw-r--r--Dafny/SccGraph.ssc14
-rw-r--r--Dafny/Translator.ssc215
-rw-r--r--Test/VSI-Benchmarks/b2.dfy11
-rw-r--r--Test/dafny0/Answer20
-rw-r--r--Test/dafny0/BinaryTree.dfy2
-rw-r--r--Test/dafny0/Definedness.dfy2
-rw-r--r--Test/dafny0/ListContents.dfy2
-rw-r--r--Test/dafny0/Substitution.dfy2
-rw-r--r--Test/dafny0/SumOfCubes.dfy6
-rw-r--r--Test/dafny0/Use.dfy42
-rw-r--r--Util/Emacs/dafny-mode.el2
-rw-r--r--Util/latex/dafny.sty4
18 files changed, 407 insertions, 484 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 351905e1..6e3b68da 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -30,7 +30,7 @@ static int anonymousIds = 0;
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
- public bool IsUse;
+ public bool IsUnlimited;
}
// helper routine for parsing call statements
@@ -173,7 +173,7 @@ ClassMemberDecl<List<MemberDecl!\>! mm>
.)
{ "ghost" (. mmod.IsGhost = true; .)
| "static" (. mmod.IsStatic = true; .)
- | "use" (. mmod.IsUse = true; .)
+ | "unlimited" (. mmod.IsUnlimited = true; .)
}
( FieldDecl<mmod, mm>
| FunctionDecl<mmod, out f> (. mm.Add(f); .)
@@ -219,7 +219,7 @@ FieldDecl<MemberModifiers mmod, List<MemberDecl!\>! mm>
Token! id; Type! ty;
.)
"var"
- (. if (mmod.IsUse) { SemErr(token, "fields cannot be declared 'use'"); }
+ (. if (mmod.IsUnlimited) { SemErr(token, "fields cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(token, "fields cannot be declared 'static'"); }
.)
{ Attribute<ref attrs> }
@@ -302,7 +302,7 @@ MethodDecl<MemberModifiers mmod, out Method! m>
Statement! bb; BlockStmt body = null;
.)
"method"
- (. if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }
+ (. if (mmod.IsUnlimited) { SemErr(token, "methods cannot be declared 'unlimited'"); }
.)
{ Attribute<ref attrs> }
Ident<out id>
@@ -442,7 +442,7 @@ FunctionDecl<MemberModifiers mmod, out Function! f>
FunctionBody<out bb> (. body = bb; .)
)
(. parseVarScope.PopMarker();
- f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
+ f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
.)
.
diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc
index ae07c84a..dc787503 100644
--- a/Dafny/DafnyAst.ssc
+++ b/Dafny/DafnyAst.ssc
@@ -521,7 +521,8 @@ namespace Microsoft.Dafny
public class Function : MemberDecl, TypeParameter.ParentType {
public readonly bool IsStatic;
public readonly bool IsGhost; // functions are "ghost" by default; a non-ghost function is called a "function method"
- public readonly bool IsUse;
+ public readonly bool IsUnlimited;
+ public bool IsRecursive; // filled in during resolution
public readonly List<TypeParameter!>! TypeArgs;
public readonly List<Formal!>! Formals;
public readonly Type! ResultType;
@@ -530,11 +531,11 @@ namespace Microsoft.Dafny
public readonly List<Expression!>! Decreases;
public readonly Expression Body; // an extended expression
- public Function(Token! tok, string! name, bool isStatic, bool isGhost, bool isUse, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,
+ public Function(Token! tok, string! name, bool isStatic, bool isGhost, bool isUnlimited, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,
List<Expression!>! req, List<Expression!>! reads, List<Expression!>! decreases, Expression body, Attributes attributes) {
this.IsStatic = isStatic;
this.IsGhost = isGhost;
- this.IsUse = isUse;
+ this.IsUnlimited = isUnlimited;
this.TypeArgs = typeArgs;
this.Formals = formals;
this.ResultType = resultType;
@@ -1098,21 +1099,6 @@ namespace Microsoft.Dafny
}
}
- /// <summary>
- /// UseExpr's are used only temporarily during translation.
- /// </summary>
- public class UseExpr : FunctionCallExpr {
- [NotDelayed] [Captured]
- public UseExpr(FunctionCallExpr! fce)
- requires fce.Function != null && fce.Function.IsUse;
- {
- base(fce.tok, fce.Name, fce.Receiver, new List<Expression!>(fce.Args));
- this.Function = fce.Function;
- assume Type.Bool.IsPeerConsistent; // This would follow from BoolType being an Immutable type, or from Type.Bool being [Frozen]
- this.Type = Type.Bool;
- }
- }
-
public class OldExpr : Expression {
[Peer] public readonly Expression! E;
[Captured]
diff --git a/Dafny/Parser.ssc b/Dafny/Parser.ssc
index 0792f6bb..e0660c65 100644
--- a/Dafny/Parser.ssc
+++ b/Dafny/Parser.ssc
@@ -6,7 +6,7 @@ using Microsoft.Contracts;
namespace Microsoft.Dafny {
public class Parser {
- const int maxT = 97;
+ const int maxT = 98;
const bool T = true;
const bool x = false;
@@ -28,7 +28,7 @@ static int anonymousIds = 0;
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
- public bool IsUse;
+ public bool IsUnlimited;
}
// helper routine for parsing call statements
@@ -274,7 +274,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
mmod.IsStatic = true;
} else {
Get();
- mmod.IsUse = true;
+ mmod.IsUnlimited = true;
}
}
if (t.kind == 14) {
@@ -285,7 +285,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
} else if (t.kind == 19) {
MethodDecl(mmod, out m);
mm.Add(m);
- } else Error(98);
+ } else Error(99);
}
static void GenericParameters(List<TypeParameter!>! typeArgs) {
@@ -306,7 +306,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
Token! id; Type! ty;
Expect(14);
- if (mmod.IsUse) { SemErr(token, "fields cannot be declared 'use'"); }
+ if (mmod.IsUnlimited) { SemErr(token, "fields cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(token, "fields cannot be declared 'static'"); }
while (t.kind == 6) {
@@ -363,9 +363,9 @@ public static int Parse (List<ModuleDecl!>! modules) {
}
FunctionBody(out bb);
body = bb;
- } else Error(99);
+ } else Error(100);
parseVarScope.PopMarker();
- f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
+ f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
}
@@ -382,7 +382,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
Statement! bb; BlockStmt body = null;
Expect(19);
- if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }
+ if (mmod.IsUnlimited) { SemErr(token, "methods cannot be declared 'unlimited'"); }
while (t.kind == 6) {
Attribute(ref attrs);
@@ -408,7 +408,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
}
BlockStmt(out bb);
body = (BlockStmt)bb;
- } else Error(100);
+ } else Error(101);
parseVarScope.PopMarker();
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -540,7 +540,7 @@ public static int Parse (List<ModuleDecl!>! modules) {
} else if (t.kind == 1 || t.kind == 32) {
ReferenceType(out tok, out ty);
- } else Error(101);
+ } else Error(102);
}
static void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {
@@ -589,12 +589,12 @@ List<Expression!>! decreases) {
Expression(out e);
Expect(13);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(102);
+ } else Error(103);
} else if (t.kind == 25) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(103);
+ } else Error(104);
}
static void BlockStmt(out Statement! block) {
@@ -621,14 +621,14 @@ List<Expression!>! decreases) {
Get();
x = token;
Expression(out e);
- Expect(56);
+ Expect(57);
Expression(out e0);
Expect(46);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(9)) {
EquivExpression(out e);
- } else Error(104);
+ } else Error(105);
}
static void Expressions(List<Expression!>! args) {
@@ -669,7 +669,7 @@ List<Expression!>! decreases) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else Error(105);
+ } else Error(106);
}
static void FunctionSpec(List<Expression!>! reqs, List<Expression!>! reads, List<Expression!>! decreases) {
@@ -689,7 +689,7 @@ List<Expression!>! decreases) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(106);
+ } else Error(107);
}
static void FunctionBody(out Expression! e) {
@@ -699,7 +699,7 @@ List<Expression!>! decreases) {
MatchExpression(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(107);
+ } else Error(108);
Expect(7);
}
@@ -721,7 +721,7 @@ List<Expression!>! decreases) {
e = new WildcardExpr(token);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(108);
+ } else Error(109);
}
static void MatchExpression(out Expression! e) {
@@ -776,7 +776,7 @@ List<Expression!>! decreases) {
ss.Add(s);
} else if (t.kind == 9 || t.kind == 14) {
VarDeclStmts(ss);
- } else Error(109);
+ } else Error(110);
}
static void OneStmt(out Statement! s) {
@@ -792,15 +792,15 @@ List<Expression!>! decreases) {
AssumeStmt(out s);
break;
}
- case 11: {
+ case 55: {
UseStmt(out s);
break;
}
- case 55: {
+ case 56: {
PrintStmt(out s);
break;
}
- case 1: case 26: case 89: case 90: {
+ case 1: case 26: case 90: case 91: {
AssignStmt(out s);
break;
}
@@ -854,7 +854,7 @@ List<Expression!>! decreases) {
s = new ReturnStmt(x);
break;
}
- default: Error(110); break;
+ default: Error(111); break;
}
}
@@ -895,7 +895,7 @@ List<Expression!>! decreases) {
static void UseStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(11);
+ Expect(55);
x = token;
Expression(out e);
Expect(13);
@@ -906,7 +906,7 @@ List<Expression!>! decreases) {
Token! x; Attributes.Argument! arg;
List<Attributes.Argument!> args = new List<Attributes.Argument!>();
- Expect(55);
+ Expect(56);
x = token;
AttributeArg(out arg);
args.Add(arg);
@@ -1023,7 +1023,7 @@ List<Expression!>! decreases) {
} else if (t.kind == 6) {
BlockStmt(out s);
els = s;
- } else Error(111);
+ } else Error(112);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -1105,7 +1105,7 @@ List<Expression!>! decreases) {
}
Expect(27);
Expect(6);
- while (t.kind == 11 || t.kind == 53 || t.kind == 54) {
+ while (t.kind == 53 || t.kind == 54 || t.kind == 55) {
if (t.kind == 53) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
@@ -1123,7 +1123,7 @@ List<Expression!>! decreases) {
} else if (t.kind == 44) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(112);
+ } else Error(113);
Expect(7);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1149,7 +1149,7 @@ List<Expression!>! decreases) {
} else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(113);
+ } else Error(114);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -1157,10 +1157,10 @@ List<Expression!>! decreases) {
Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 89 || t.kind == 90) {
+ } else if (t.kind == 26 || t.kind == 90 || t.kind == 91) {
ObjectExpression(out e);
- } else Error(114);
- while (t.kind == 84 || t.kind == 86) {
+ } else Error(115);
+ while (t.kind == 85 || t.kind == 87) {
SelectOrCallSuffix(ref e);
}
}
@@ -1201,7 +1201,7 @@ List<Expression!>! decreases) {
} else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(115);
+ } else Error(116);
Expect(27);
}
@@ -1240,11 +1240,11 @@ List<Expression!>! decreases) {
e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 89 || t.kind == 90) {
+ } else if (t.kind == 26 || t.kind == 90 || t.kind == 91) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(116);
- while (t.kind == 84 || t.kind == 86) {
+ } else Error(117);
+ while (t.kind == 85 || t.kind == 87) {
SelectOrCallSuffix(ref e);
}
}
@@ -1257,13 +1257,13 @@ List<Expression!>! decreases) {
} else if (StartOf(7)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else Error(117);
+ } else Error(118);
}
static void EquivExpression(out Expression! e0) {
Token! x; Expression! e1;
ImpliesExpression(out e0);
- while (t.kind == 57 || t.kind == 58) {
+ while (t.kind == 58 || t.kind == 59) {
EquivOp();
x = token;
ImpliesExpression(out e1);
@@ -1274,7 +1274,7 @@ List<Expression!>! decreases) {
static void ImpliesExpression(out Expression! e0) {
Token! x; Expression! e1;
LogicalExpression(out e0);
- if (t.kind == 59 || t.kind == 60) {
+ if (t.kind == 60 || t.kind == 61) {
ImpliesOp();
x = token;
ImpliesExpression(out e1);
@@ -1283,23 +1283,23 @@ List<Expression!>! decreases) {
}
static void EquivOp() {
- if (t.kind == 57) {
+ if (t.kind == 58) {
Get();
- } else if (t.kind == 58) {
+ } else if (t.kind == 59) {
Get();
- } else Error(118);
+ } else Error(119);
}
static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(13)) {
- if (t.kind == 61 || t.kind == 62) {
+ if (t.kind == 62 || t.kind == 63) {
AndOp();
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (t.kind == 61 || t.kind == 62) {
+ while (t.kind == 62 || t.kind == 63) {
AndOp();
x = token;
RelationalExpression(out e1);
@@ -1310,7 +1310,7 @@ List<Expression!>! decreases) {
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (t.kind == 63 || t.kind == 64) {
+ while (t.kind == 64 || t.kind == 65) {
OrOp();
x = token;
RelationalExpression(out e1);
@@ -1321,11 +1321,11 @@ List<Expression!>! decreases) {
}
static void ImpliesOp() {
- if (t.kind == 59) {
+ if (t.kind == 60) {
Get();
- } else if (t.kind == 60) {
+ } else if (t.kind == 61) {
Get();
- } else Error(119);
+ } else Error(120);
}
static void RelationalExpression(out Expression! e0) {
@@ -1339,25 +1339,25 @@ List<Expression!>! decreases) {
}
static void AndOp() {
- if (t.kind == 61) {
+ if (t.kind == 62) {
Get();
- } else if (t.kind == 62) {
+ } else if (t.kind == 63) {
Get();
- } else Error(120);
+ } else Error(121);
}
static void OrOp() {
- if (t.kind == 63) {
+ if (t.kind == 64) {
Get();
- } else if (t.kind == 64) {
+ } else if (t.kind == 65) {
Get();
- } else Error(121);
+ } else Error(122);
}
static void Term(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 74 || t.kind == 75) {
+ while (t.kind == 75 || t.kind == 76) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1367,7 +1367,7 @@ List<Expression!>! decreases) {
static void RelOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (t.kind) {
- case 65: {
+ case 66: {
Get();
x = token; op = BinaryExpr.Opcode.Eq;
break;
@@ -1382,22 +1382,22 @@ List<Expression!>! decreases) {
x = token; op = BinaryExpr.Opcode.Gt;
break;
}
- case 66: {
+ case 67: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 67: {
+ case 68: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- case 68: {
+ case 69: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 69: {
+ case 70: {
Get();
x = token; op = BinaryExpr.Opcode.Disjoint;
break;
@@ -1407,34 +1407,34 @@ List<Expression!>! decreases) {
x = token; op = BinaryExpr.Opcode.In;
break;
}
- case 70: {
+ case 71: {
Get();
x = token; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 71: {
+ case 72: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 72: {
+ case 73: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 73: {
+ case 74: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(122); break;
+ default: Error(123); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 35 || t.kind == 76 || t.kind == 77) {
+ while (t.kind == 35 || t.kind == 77 || t.kind == 78) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1443,23 +1443,23 @@ List<Expression!>! decreases) {
static void AddOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 74) {
+ if (t.kind == 75) {
Get();
x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 75) {
+ } else if (t.kind == 76) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(123);
+ } else Error(124);
}
static void UnaryExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 75) {
+ if (t.kind == 76) {
Get();
x = token;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 78 || t.kind == 79) {
+ } else if (t.kind == 79 || t.kind == 80) {
NegOp();
x = token;
UnaryExpression(out e);
@@ -1468,7 +1468,7 @@ List<Expression!>! decreases) {
SelectExpression(out e);
} else if (StartOf(15)) {
ConstAtomExpression(out e);
- } else Error(124);
+ } else Error(125);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
@@ -1476,21 +1476,21 @@ List<Expression!>! decreases) {
if (t.kind == 35) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 76) {
+ } else if (t.kind == 77) {
Get();
x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 77) {
+ } else if (t.kind == 78) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(125);
+ } else Error(126);
}
static void NegOp() {
- if (t.kind == 78) {
+ if (t.kind == 79) {
Get();
- } else if (t.kind == 79) {
+ } else if (t.kind == 80) {
Get();
- } else Error(126);
+ } else Error(127);
}
static void ConstAtomExpression(out Expression! e) {
@@ -1498,17 +1498,17 @@ List<Expression!>! decreases) {
e = dummyExpr;
switch (t.kind) {
- case 80: {
+ case 81: {
Get();
e = new LiteralExpr(token, false);
break;
}
- case 81: {
+ case 82: {
Get();
e = new LiteralExpr(token, true);
break;
}
- case 82: {
+ case 83: {
Get();
e = new LiteralExpr(token);
break;
@@ -1518,11 +1518,11 @@ List<Expression!>! decreases) {
e = new LiteralExpr(token, n);
break;
}
- case 83: {
+ case 84: {
Get();
x = token;
Ident(out dtName);
- Expect(84);
+ Expect(85);
Ident(out id);
elements = new List<Expression!>();
if (t.kind == 26) {
@@ -1535,7 +1535,7 @@ List<Expression!>! decreases) {
e = new DatatypeValue(token, dtName.val, id.val, elements);
break;
}
- case 85: {
+ case 86: {
Get();
x = token;
Expect(26);
@@ -1562,17 +1562,17 @@ List<Expression!>! decreases) {
Expect(7);
break;
}
- case 86: {
+ case 87: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(7)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(87);
+ Expect(88);
break;
}
- default: Error(127); break;
+ default: Error(128); break;
}
}
@@ -1611,10 +1611,10 @@ List<Expression!>! decreases) {
static void ObjectExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 89) {
+ if (t.kind == 90) {
Get();
e = new ThisExpr(token);
- } else if (t.kind == 90) {
+ } else if (t.kind == 91) {
Get();
x = token;
Expect(26);
@@ -1627,9 +1627,9 @@ List<Expression!>! decreases) {
QuantifierGuts(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(128);
+ } else Error(129);
Expect(27);
- } else Error(129);
+ } else Error(130);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1637,7 +1637,7 @@ List<Expression!>! decreases) {
Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 84) {
+ if (t.kind == 85) {
Get();
Ident(out id);
if (t.kind == 26) {
@@ -1650,14 +1650,14 @@ List<Expression!>! decreases) {
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 86) {
+ } else if (t.kind == 87) {
Get();
x = token;
if (StartOf(7)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 42 || t.kind == 88) {
- if (t.kind == 88) {
+ if (t.kind == 42 || t.kind == 89) {
+ if (t.kind == 89) {
Get();
anyDots = true;
if (StartOf(7)) {
@@ -1670,11 +1670,11 @@ List<Expression!>! decreases) {
e1 = ee;
}
}
- } else if (t.kind == 88) {
+ } else if (t.kind == 89) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(130);
+ } else Error(131);
assert !anyDots ==> e0 != null;
if (anyDots) {
assert e0 != null || e1 != null;
@@ -1687,8 +1687,8 @@ List<Expression!>! decreases) {
e = new SeqUpdateExpr(x, e, e0, e1);
}
- Expect(87);
- } else Error(131);
+ Expect(88);
+ } else Error(132);
}
static void QuantifierGuts(out Expression! q) {
@@ -1701,13 +1701,13 @@ List<Expression!>! decreases) {
Triggers trigs = null;
Expression! body;
- if (t.kind == 91 || t.kind == 92) {
+ if (t.kind == 92 || t.kind == 93) {
Forall();
x = token; univ = true;
- } else if (t.kind == 93 || t.kind == 94) {
+ } else if (t.kind == 94 || t.kind == 95) {
Exists();
x = token;
- } else Error(132);
+ } else Error(133);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1731,19 +1731,19 @@ List<Expression!>! decreases) {
}
static void Forall() {
- if (t.kind == 91) {
+ if (t.kind == 92) {
Get();
- } else if (t.kind == 92) {
+ } else if (t.kind == 93) {
Get();
- } else Error(133);
+ } else Error(134);
}
static void Exists() {
- if (t.kind == 93) {
+ if (t.kind == 94) {
Get();
- } else if (t.kind == 94) {
+ } else if (t.kind == 95) {
Get();
- } else Error(134);
+ } else Error(135);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -1756,16 +1756,16 @@ List<Expression!>! decreases) {
es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(135);
+ } else Error(136);
Expect(7);
}
static void QSep() {
- if (t.kind == 95) {
+ if (t.kind == 96) {
Get();
- } else if (t.kind == 96) {
+ } else if (t.kind == 97) {
Get();
- } else Error(136);
+ } else Error(137);
}
static void AttributeBody(ref Attributes attrs) {
@@ -1815,7 +1815,7 @@ List<Expression!>! decreases) {
case 8: s = "class expected"; break;
case 9: s = "ghost expected"; break;
case 10: s = "static expected"; break;
- case 11: s = "use expected"; break;
+ case 11: s = "unlimited expected"; break;
case 12: s = "datatype expected"; break;
case 13: s = "; expected"; break;
case 14: s = "var expected"; break;
@@ -1859,88 +1859,89 @@ List<Expression!>! decreases) {
case 52: s = "| expected"; break;
case 53: s = "assert expected"; break;
case 54: s = "assume expected"; break;
- case 55: s = "print expected"; break;
- case 56: s = "then expected"; break;
- case 57: s = "<==> expected"; break;
- case 58: s = "\\u21d4 expected"; break;
- case 59: s = "==> expected"; break;
- case 60: s = "\\u21d2 expected"; break;
- case 61: s = "&& expected"; break;
- case 62: s = "\\u2227 expected"; break;
- case 63: s = "|| expected"; break;
- case 64: s = "\\u2228 expected"; break;
- case 65: s = "== expected"; break;
- case 66: s = "<= expected"; break;
- case 67: s = ">= expected"; break;
- case 68: s = "!= expected"; break;
- case 69: s = "!! expected"; break;
- case 70: s = "!in expected"; break;
- case 71: s = "\\u2260 expected"; break;
- case 72: s = "\\u2264 expected"; break;
- case 73: s = "\\u2265 expected"; break;
- case 74: s = "+ expected"; break;
- case 75: s = "- expected"; break;
- case 76: s = "/ expected"; break;
- case 77: s = "% expected"; break;
- case 78: s = "! expected"; break;
- case 79: s = "\\u00ac expected"; break;
- case 80: s = "false expected"; break;
- case 81: s = "true expected"; break;
- case 82: s = "null expected"; break;
- case 83: s = "# expected"; break;
- case 84: s = ". expected"; break;
- case 85: s = "fresh expected"; break;
- case 86: s = "[ expected"; break;
- case 87: s = "] expected"; break;
- case 88: s = ".. expected"; break;
- case 89: s = "this expected"; break;
- case 90: s = "old expected"; break;
- case 91: s = "forall expected"; break;
- case 92: s = "\\u2200 expected"; break;
- case 93: s = "exists expected"; break;
- case 94: s = "\\u2203 expected"; break;
- case 95: s = ":: expected"; break;
- case 96: s = "\\u2022 expected"; break;
- case 97: s = "??? expected"; break;
- case 98: s = "invalid ClassMemberDecl"; break;
- case 99: s = "invalid FunctionDecl"; break;
- case 100: s = "invalid MethodDecl"; break;
- case 101: s = "invalid TypeAndToken"; break;
- case 102: s = "invalid MethodSpec"; break;
+ case 55: s = "use expected"; break;
+ case 56: s = "print expected"; break;
+ case 57: s = "then expected"; break;
+ case 58: s = "<==> expected"; break;
+ case 59: s = "\\u21d4 expected"; break;
+ case 60: s = "==> expected"; break;
+ case 61: s = "\\u21d2 expected"; break;
+ case 62: s = "&& expected"; break;
+ case 63: s = "\\u2227 expected"; break;
+ case 64: s = "|| expected"; break;
+ case 65: s = "\\u2228 expected"; break;
+ case 66: s = "== expected"; break;
+ case 67: s = "<= expected"; break;
+ case 68: s = ">= expected"; break;
+ case 69: s = "!= expected"; break;
+ case 70: s = "!! expected"; break;
+ case 71: s = "!in expected"; break;
+ case 72: s = "\\u2260 expected"; break;
+ case 73: s = "\\u2264 expected"; break;
+ case 74: s = "\\u2265 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 = "\\u00ac expected"; break;
+ case 81: s = "false expected"; break;
+ case 82: s = "true expected"; break;
+ case 83: s = "null expected"; break;
+ case 84: s = "# expected"; break;
+ case 85: s = ". expected"; break;
+ case 86: s = "fresh expected"; break;
+ case 87: s = "[ expected"; break;
+ case 88: s = "] expected"; break;
+ case 89: s = ".. expected"; break;
+ case 90: s = "this expected"; break;
+ case 91: s = "old expected"; break;
+ case 92: s = "forall expected"; break;
+ case 93: s = "\\u2200 expected"; break;
+ case 94: s = "exists expected"; break;
+ case 95: s = "\\u2203 expected"; break;
+ case 96: s = ":: expected"; break;
+ case 97: s = "\\u2022 expected"; break;
+ case 98: s = "??? expected"; break;
+ case 99: s = "invalid ClassMemberDecl"; break;
+ case 100: s = "invalid FunctionDecl"; break;
+ case 101: s = "invalid MethodDecl"; break;
+ case 102: s = "invalid TypeAndToken"; break;
case 103: s = "invalid MethodSpec"; break;
- case 104: s = "invalid Expression"; break;
- case 105: s = "invalid ReferenceType"; break;
- case 106: s = "invalid FunctionSpec"; break;
- case 107: s = "invalid FunctionBody"; break;
- case 108: s = "invalid PossiblyWildExpression"; break;
- case 109: s = "invalid Stmt"; break;
- case 110: s = "invalid OneStmt"; break;
- case 111: s = "invalid IfStmt"; break;
- case 112: s = "invalid ForeachStmt"; break;
- case 113: s = "invalid AssignRhs"; break;
- case 114: s = "invalid SelectExpression"; break;
- case 115: s = "invalid Guard"; break;
- case 116: s = "invalid CallStmtSubExpr"; break;
- case 117: s = "invalid AttributeArg"; break;
- case 118: s = "invalid EquivOp"; break;
- case 119: s = "invalid ImpliesOp"; break;
- case 120: s = "invalid AndOp"; break;
- case 121: s = "invalid OrOp"; break;
- case 122: s = "invalid RelOp"; break;
- case 123: s = "invalid AddOp"; break;
- case 124: s = "invalid UnaryExpression"; break;
- case 125: s = "invalid MulOp"; break;
- case 126: s = "invalid NegOp"; break;
- case 127: s = "invalid ConstAtomExpression"; break;
- case 128: s = "invalid ObjectExpression"; break;
+ case 104: s = "invalid MethodSpec"; break;
+ case 105: s = "invalid Expression"; break;
+ case 106: s = "invalid ReferenceType"; break;
+ case 107: s = "invalid FunctionSpec"; break;
+ case 108: s = "invalid FunctionBody"; break;
+ case 109: s = "invalid PossiblyWildExpression"; break;
+ case 110: s = "invalid Stmt"; break;
+ case 111: s = "invalid OneStmt"; break;
+ case 112: s = "invalid IfStmt"; break;
+ case 113: s = "invalid ForeachStmt"; break;
+ case 114: s = "invalid AssignRhs"; break;
+ case 115: s = "invalid SelectExpression"; break;
+ case 116: s = "invalid Guard"; break;
+ case 117: s = "invalid CallStmtSubExpr"; break;
+ case 118: s = "invalid AttributeArg"; break;
+ case 119: s = "invalid EquivOp"; break;
+ case 120: s = "invalid ImpliesOp"; break;
+ case 121: s = "invalid AndOp"; break;
+ case 122: s = "invalid OrOp"; break;
+ case 123: s = "invalid RelOp"; break;
+ case 124: s = "invalid AddOp"; break;
+ case 125: s = "invalid UnaryExpression"; break;
+ case 126: s = "invalid MulOp"; break;
+ case 127: s = "invalid NegOp"; break;
+ case 128: s = "invalid ConstAtomExpression"; break;
case 129: s = "invalid ObjectExpression"; break;
- case 130: s = "invalid SelectOrCallSuffix"; break;
+ case 130: s = "invalid ObjectExpression"; break;
case 131: s = "invalid SelectOrCallSuffix"; break;
- case 132: s = "invalid QuantifierGuts"; break;
- case 133: s = "invalid Forall"; break;
- case 134: s = "invalid Exists"; break;
- case 135: s = "invalid AttributeOrTrigger"; break;
- case 136: s = "invalid QSep"; break;
+ case 132: s = "invalid SelectOrCallSuffix"; break;
+ case 133: s = "invalid QuantifierGuts"; break;
+ case 134: s = "invalid Forall"; break;
+ case 135: s = "invalid Exists"; break;
+ case 136: s = "invalid AttributeOrTrigger"; break;
+ case 137: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
@@ -1948,24 +1949,24 @@ List<Expression!>! decreases) {
}
static 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, T,x,x,x, T,T,T,T, 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,T,T,T, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,T,x,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,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,x,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,x,x, x,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,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,x,x, x,x,T,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,T,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,T, x,x,x,x, x,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,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,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, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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,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,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,T,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x},
- {x,T,T,T, 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,x,x, x,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,T, x,x,T,T, T,T,T,T, x,T,T,x, 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, T,x,x,x, T,T,T,T, 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,T,T,T, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,x,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,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,T,T,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,x,x, x,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,x,T,T, x,x,T,T, x,x,x,x, x,x,x,x},
+ {x,T,x,x, x,x,T,x, x,T,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, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x},
+ {x,T,T,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,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, T,x,x,T, T,T,T,T, T,x,T,T, x,x,T,T, x,x,x,x, x,x,x,x},
+ {x,T,T,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,T, x,x,x,x, x,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,x,T,T, 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,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,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,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,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,T,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T, 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,x,x, x,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,x,T,T, x,x,T,T, x,x,x,x, x,x,x,x}
};
diff --git a/Dafny/Printer.ssc b/Dafny/Printer.ssc
index 1779f46b..a49d1a7e 100644
--- a/Dafny/Printer.ssc
+++ b/Dafny/Printer.ssc
@@ -177,7 +177,7 @@ namespace Microsoft.Dafny {
public void PrintFunction(Function! f, int indent) {
Indent(indent);
string k = "function";
- if (f.IsUse) { k = "use " + k; }
+ if (f.IsUnlimited) { k = "unlimited " + k; }
if (f.IsStatic) { k = "static " + k; }
if (!f.IsGhost) { k += " method"; }
PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs);
diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc
index db6e667a..e0efaa3c 100644
--- a/Dafny/Resolver.ssc
+++ b/Dafny/Resolver.ssc
@@ -92,6 +92,24 @@ namespace Microsoft.Dafny {
foreach (ModuleDecl m in prog.Modules) {
ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
}
+ // compute IsRecursive bit for mutually recursive functions
+ foreach (ModuleDecl m in prog.Modules) {
+ foreach (TopLevelDecl decl in m.TopLevelDecls) {
+ ClassDecl cl = decl as ClassDecl;
+ if (cl != null) {
+ foreach (MemberDecl member in cl.Members) {
+ Function fn = member as Function;
+ if (fn != null && !fn.IsRecursive) { // note, self-recursion has already been determined
+ int n = m.CallGraph.GetSCCSize(fn);
+ if (2 <= n) {
+ // the function is mutually recursive (note, the SCC does not determine self recursion)
+ fn.IsRecursive = true;
+ }
+ }
+ }
+ }
+ }
+ }
}
public void RegisterTopLevelDecls(List<TopLevelDecl!>! declarations) {
@@ -808,10 +826,6 @@ namespace Microsoft.Dafny {
break;
}
}
- FunctionCallExpr fce = expr as FunctionCallExpr;
- if (fce == null || fce.Function == null || !fce.Function.IsUse) {
- Error(s.Expr, "use statement must indicate a function declared as use");
- }
} else if (stmt is PredicateStmt) {
PredicateStmt s = (PredicateStmt)stmt;
s.IsGhost = true;
@@ -1590,6 +1604,9 @@ namespace Microsoft.Dafny {
if (callerModule == calleeModule) {
// intra-module call; this is allowed; add edge in module's call graph
callerModule.CallGraph.AddEdge(currentFunction, function);
+ if (currentFunction == function) {
+ currentFunction.IsRecursive = true; // self recursion (mutual recursion is determined elsewhere)
+ }
} else if (calleeModule.IsDefaultModule) {
// all is fine: everything implicitly imports the default module
} else if (importGraph.Reaches(callerModule, calleeModule)) {
diff --git a/Dafny/Scanner.ssc b/Dafny/Scanner.ssc
index 7e954005..56c6f0be 100644
--- a/Dafny/Scanner.ssc
+++ b/Dafny/Scanner.ssc
@@ -133,7 +133,7 @@ public class Scanner {
start[8804] = 38;
start[8805] = 39;
}
- const int noSym = 97;
+ const int noSym = 98;
static short[] start = new short[16385];
@@ -280,7 +280,7 @@ public class Scanner {
case "class": t.kind = 8; break;
case "ghost": t.kind = 9; break;
case "static": t.kind = 10; break;
- case "use": t.kind = 11; break;
+ case "unlimited": t.kind = 11; break;
case "datatype": t.kind = 12; break;
case "var": t.kind = 14; break;
case "method": t.kind = 19; break;
@@ -313,16 +313,17 @@ public class Scanner {
case "in": t.kind = 51; break;
case "assert": t.kind = 53; break;
case "assume": t.kind = 54; break;
- case "print": t.kind = 55; break;
- case "then": t.kind = 56; break;
- case "false": t.kind = 80; break;
- case "true": t.kind = 81; break;
- case "null": t.kind = 82; break;
- case "fresh": t.kind = 85; break;
- case "this": t.kind = 89; break;
- case "old": t.kind = 90; break;
- case "forall": t.kind = 91; break;
- case "exists": t.kind = 93; break;
+ case "use": t.kind = 55; break;
+ case "print": t.kind = 56; break;
+ case "then": t.kind = 57; break;
+ case "false": t.kind = 81; break;
+ case "true": t.kind = 82; break;
+ case "null": t.kind = 83; break;
+ case "fresh": t.kind = 86; break;
+ case "this": t.kind = 90; break;
+ case "old": t.kind = 91; break;
+ case "forall": t.kind = 92; break;
+ case "exists": t.kind = 94; break;
default: break;
}
@@ -388,83 +389,83 @@ public class Scanner {
else {t.kind = 52; goto done;}
case 19:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
- else {t.kind = 66; goto done;}
+ else {t.kind = 67; goto done;}
case 20:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 21;}
else {t.kind = noSym; goto done;}
case 21:
- {t.kind = 57; goto done;}
- case 22:
{t.kind = 58; goto done;}
+ case 22:
+ {t.kind = 59; goto done;}
case 23:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
- else {t.kind = 65; goto done;}
+ else {t.kind = 66; goto done;}
case 24:
- {t.kind = 59; goto done;}
- case 25:
{t.kind = 60; goto done;}
+ case 25:
+ {t.kind = 61; goto done;}
case 26:
if (ch == '&') {buf.Append(ch); NextCh(); goto case 27;}
else {t.kind = noSym; goto done;}
case 27:
- {t.kind = 61; goto done;}
- case 28:
{t.kind = 62; goto done;}
- case 29:
+ case 28:
{t.kind = 63; goto done;}
- case 30:
+ case 29:
{t.kind = 64; goto done;}
+ case 30:
+ {t.kind = 65; goto done;}
case 31:
- {t.kind = 67; goto done;}
+ {t.kind = 68; goto done;}
case 32:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 33;}
else if (ch == '!') {buf.Append(ch); NextCh(); goto case 34;}
else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 35;}
- else {t.kind = 78; goto done;}
+ else {t.kind = 79; goto done;}
case 33:
- {t.kind = 68; goto done;}
- case 34:
{t.kind = 69; goto done;}
+ case 34:
+ {t.kind = 70; goto done;}
case 35:
if (ch == 'n') {buf.Append(ch); NextCh(); goto case 36;}
else {t.kind = noSym; goto done;}
case 36:
- {t.kind = 70; goto done;}
- case 37:
{t.kind = 71; goto done;}
- case 38:
+ case 37:
{t.kind = 72; goto done;}
- case 39:
+ case 38:
{t.kind = 73; goto done;}
- case 40:
+ case 39:
{t.kind = 74; goto done;}
- case 41:
+ case 40:
{t.kind = 75; goto done;}
- case 42:
+ case 41:
{t.kind = 76; goto done;}
- case 43:
+ case 42:
{t.kind = 77; goto done;}
+ case 43:
+ {t.kind = 78; goto done;}
case 44:
- {t.kind = 79; goto done;}
+ {t.kind = 80; goto done;}
case 45:
- {t.kind = 83; goto done;}
+ {t.kind = 84; goto done;}
case 46:
if (ch == '.') {buf.Append(ch); NextCh(); goto case 49;}
- else {t.kind = 84; goto done;}
+ else {t.kind = 85; goto done;}
case 47:
- {t.kind = 86; goto done;}
- case 48:
{t.kind = 87; goto done;}
- case 49:
+ case 48:
{t.kind = 88; goto done;}
+ case 49:
+ {t.kind = 89; goto done;}
case 50:
- {t.kind = 92; goto done;}
+ {t.kind = 93; goto done;}
case 51:
- {t.kind = 94; goto done;}
- case 52:
{t.kind = 95; goto done;}
- case 53:
+ case 52:
{t.kind = 96; goto done;}
+ case 53:
+ {t.kind = 97; goto done;}
case 54: {t.kind = 0; goto done;}
}
done:
diff --git a/Dafny/SccGraph.ssc b/Dafny/SccGraph.ssc
index 1ca7125b..0498f55d 100644
--- a/Dafny/SccGraph.ssc
+++ b/Dafny/SccGraph.ssc
@@ -147,6 +147,20 @@ namespace Microsoft.Dafny {
}
/// <summary>
+ /// Idempotently adds 'n' as a vertex and then returns the size of the set of Node's in the strongly connected component
+ /// that contains 'n'.
+ /// </summary>
+ public int GetSCCSize(Node n)
+ ensures 1 <= result;
+ {
+ Vertex v = GetVertex(n);
+ ComputeSCCs();
+ Vertex repr = v.SccRepresentative;
+ assert repr != null && repr.SccMembers != null; // follows from postcondition of ComputeSCCs
+ return repr.SccMembers.Count;
+ }
+
+ /// <summary>
/// This method sets the SccRepresentative fields of the graph's vertices so that two
/// vertices have the same representative iff they are in the same strongly connected
/// component.
diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index 9b17d628..7a802ecd 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -403,8 +403,8 @@ namespace Microsoft.Dafny {
Bpl.Axiom ax = FunctionAxiom(f, f.Body, null, null, null);
sink.TopLevelDeclarations.Add(ax);
}
- if (f.IsUse) {
- AddUseAxioms(f);
+ if (f.IsRecursive && !f.IsUnlimited) {
+ AddLimitedAxioms(f);
}
}
AddFrameAxiom(f);
@@ -450,7 +450,7 @@ namespace Microsoft.Dafny {
// If a specialization is provided, occurrences of "specializationFormal" in "body" are also replaced by
// that expression.
//
- // The translation of "body" uses the #alt form of all "use" functions.
+ // The translation of "body" uses the #limited form whenever the callee is in the same SCC of the call graph.
//
// Note, an antecedent $Heap[this,alloc] is intentionally left out: including it would only weaken
// the axiom. Moreover, leaving it out does not introduce any soundness problem, because the Dafny
@@ -526,16 +526,15 @@ namespace Microsoft.Dafny {
substMap.Add(specializationFormal, r);
body = Substitute(body, null, substMap);
}
- Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(funcAppl, etran.AltFunctions.TrExpr(body))));
+ Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(body))));
return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax));
}
- void AddUseAxioms(Function! f)
- requires f.IsUse;
+ void AddLimitedAxioms(Function! f)
+ requires f.IsRecursive && !f.IsUnlimited;
requires sink != null && predef != null;
{
- // axiom (forall formals :: { f(args) } f(args) == f#alt(args))
- // axiom (forall formals :: { f#use(args) } f#use(args) ==> f(args) == f#alt(args))
+ // axiom (forall formals :: { f(args) } f(args) == f#limited(args))
Bpl.VariableSeq formals = new Bpl.VariableSeq();
Bpl.ExprSeq args = new Bpl.ExprSeq();
@@ -561,19 +560,13 @@ namespace Microsoft.Dafny {
Bpl.FunctionCall origFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
Bpl.Expr origFuncAppl = new Bpl.NAryExpr(f.tok, origFuncID, args);
- Bpl.FunctionCall altFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#alt", TrType(f.ResultType)));
- Bpl.Expr altFuncAppl = new Bpl.NAryExpr(f.tok, altFuncID, args);
- Bpl.FunctionCall useFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#use", Bpl.Type.Bool));
- Bpl.Expr useFuncAppl = new Bpl.NAryExpr(f.tok, useFuncID, args);
+ Bpl.FunctionCall limitedFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#limited", TrType(f.ResultType)));
+ Bpl.Expr limitedFuncAppl = new Bpl.NAryExpr(f.tok, limitedFuncID, args);
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(origFuncAppl));
- Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(origFuncAppl, altFuncAppl));
- sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
-
- tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(useFuncAppl));
- ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(useFuncAppl, Bpl.Expr.Eq(origFuncAppl, altFuncAppl)));
+ Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(origFuncAppl, limitedFuncAppl));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
}
@@ -827,108 +820,6 @@ namespace Microsoft.Dafny {
builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));
}
-#if OLD_FRAME_AXIOM
- /// <summary>
- /// Generates:
- /// axiom (forall h0: HeapType, h1: HeapType, formals... ::
- /// { F(h0,formals), F(h1,formals) }
- /// heaps are well-formed and formals are allocated
- /// AND
- /// (forall(alpha) o: ref, f: Field alpha ::
- /// o != null AND h0[o,alloc] AND h1[o,alloc] AND
- /// o in reads clause of formals in h0
- /// IMPLIES h0[o,f] == h1[o,f])
- /// AND
- /// (forall(alpha) o: ref, f: Field alpha ::
- /// o != null AND h1[o,alloc] AND h0[o,alloc] AND
- /// o in reads clause of formals in h1
- /// IMPLIES h0[o,f] == h1[o,f])
- /// IMPLIES
- /// F(h0,formals) == F(h1,formals)
- /// );
- /// Note, the second h?[o,alloc] in the antecedent of each inner forall above is sound
- /// because user expressions are not allowed to quantify over all allocated objects, and
- /// in particular, they have no way to depend on the .alloc field of an object.
- ///
- /// If the function is a "use" function, then "F "in the last line is replaced by "F#alt".
- /// </summary>
- void AddFrameAxiom(Function! f)
- requires sink != null && predef != null;
- {
- Bpl.BoundVariable h0Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h0", predef.HeapType));
- Bpl.BoundVariable h1Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h1", predef.HeapType));
- Bpl.Expr h0 = new Bpl.IdentifierExpr(f.tok, h0Var);
- Bpl.Expr h1 = new Bpl.IdentifierExpr(f.tok, h1Var);
- ExpressionTranslator etran0 = new ExpressionTranslator(this, predef, h0);
- ExpressionTranslator etran1 = new ExpressionTranslator(this, predef, h1);
-
- Bpl.Expr wellFormed = Bpl.Expr.And(
- FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr),
- FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran1.HeapExpr));
-
- Bpl.TypeVariable alpha = new Bpl.TypeVariable(f.tok, "alpha");
- Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));
- Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);
- Bpl.BoundVariable fieldVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$f", predef.FieldName(f.tok, alpha)));
- Bpl.Expr field = new Bpl.IdentifierExpr(f.tok, fieldVar);
- Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
- Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o)));
- Bpl.Expr unchanged = Bpl.Expr.Eq(Bpl.Expr.SelectTok(f.tok, h0, o, field), Bpl.Expr.SelectTok(f.tok, h1, o, field));
-
- Bpl.Expr r0 = InRWClause(f.tok, o, f.Reads, etran0, null, null);
- Bpl.Expr r1 = InRWClause(f.tok, o, f.Reads, etran1, null, null);
- Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),
- Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged));
- Bpl.Expr q1 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),
- Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r1), unchanged));
-
- // bvars: h0, h1, formals
- // f0args: h0, formals
- // f1args: h1, formals
- Bpl.VariableSeq bvars = new Bpl.VariableSeq();
- Bpl.ExprSeq f0args = new Bpl.ExprSeq();
- Bpl.ExprSeq f1args = new Bpl.ExprSeq();
- bvars.Add(h0Var); bvars.Add(h1Var);
- f0args.Add(h0);
- f1args.Add(h1);
- if (!f.IsStatic) {
- Bpl.BoundVariable thVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
- Bpl.Expr th = new Bpl.IdentifierExpr(f.tok, thVar);
- bvars.Add(thVar);
- f0args.Add(th);
- f1args.Add(th);
-
- Type thisType = Resolver.GetThisType(f.tok, (!)f.EnclosingClass);
- Bpl.Expr wh = Bpl.Expr.And(Bpl.Expr.Neq(th, predef.Null),
- Bpl.Expr.And(etran0.GoodRef(f.tok, th, thisType), etran1.GoodRef(f.tok, th, thisType)));
- wellFormed = Bpl.Expr.And(wellFormed, wh);
- }
-
- foreach (Formal p in f.Formals) {
- Bpl.BoundVariable bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
- bvars.Add(bv);
- Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);
- f0args.Add(formal);
- f1args.Add(formal);
- Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran0);
- if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
- wh = GetWhereClause(p.tok, formal, p.Type, etran1);
- if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
- }
-
- Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.IsUse ? f.FullName + "#alt" : f.FullName, TrType(f.ResultType)));
- Bpl.Expr F0 = new Bpl.NAryExpr(f.tok, fn, f0args);
- Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);
- Bpl.Expr eq = Bpl.Expr.Eq(F0, F1);
- Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(F0, F1));
-
- Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
- Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,
- Bpl.Expr.Imp(wellFormed,
- Bpl.Expr.Imp(Bpl.Expr.And(q0, q1), eq)));
- sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, "frame axiom for " + f.FullName));
- }
-#else
/// <summary>
/// Generates:
/// axiom (forall h0: HeapType, h1: HeapType, formals... ::
@@ -944,7 +835,7 @@ namespace Microsoft.Dafny {
/// F(h0,formals) == F(h1,formals)
/// );
///
- /// If the function is a "use" function, then "F "in the last line is replaced by "F#alt".
+ /// If the function is a recursive, non-unlimited function, then the same axiom is also produced for "F#limited" instead of "F".
/// </summary>
void AddFrameAxiom(Function! f)
requires sink != null && predef != null;
@@ -1008,19 +899,27 @@ namespace Microsoft.Dafny {
if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
}
- Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.IsUse ? f.FullName + "#alt" : f.FullName, TrType(f.ResultType)));
- Bpl.Expr F0 = new Bpl.NAryExpr(f.tok, fn, f0args);
- Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);
- Bpl.Expr eq = Bpl.Expr.Eq(F0, F1);
- Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(heapSucc, F1));
-
- Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
- Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,
- Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc),
- Bpl.Expr.Imp(q0, eq)));
- sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, "frame axiom for " + f.FullName));
+ string axiomComment = "frame axiom for " + f.FullName;
+ Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
+ while (fn != null) {
+ Bpl.Expr F0 = new Bpl.NAryExpr(f.tok, fn, f0args);
+ Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);
+ Bpl.Expr eq = Bpl.Expr.Eq(F0, F1);
+ Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(heapSucc, F1));
+
+ Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
+ Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,
+ Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc),
+ Bpl.Expr.Imp(q0, eq)));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, axiomComment));
+ if (axiomComment != null && f.IsRecursive && !f.IsUnlimited) {
+ fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#limited", TrType(f.ResultType)));
+ axiomComment = null; // the comment goes only with the first frame axiom
+ } else {
+ break; // no more frame axioms to produce
+ }
+ }
}
-#endif
Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, List<Expression!>! rw, ExpressionTranslator! etran,
Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap)
@@ -1585,13 +1484,9 @@ namespace Microsoft.Dafny {
Bpl.Function func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);
sink.TopLevelDeclarations.Add(func);
- if (f.IsUse) {
- Bpl.Function altF = new Bpl.Function(f.tok, f.FullName + "#alt", args, res);
- sink.TopLevelDeclarations.Add(altF);
-
- Bpl.Formal boolRes = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
- Bpl.Function useF = new Bpl.Function(f.tok, f.FullName + "#use", args, boolRes);
- sink.TopLevelDeclarations.Add(useF);
+ if (f.IsRecursive && !f.IsUnlimited) {
+ Bpl.Function limitedF = new Bpl.Function(f.tok, f.FullName + "#limited", args, res);
+ sink.TopLevelDeclarations.Add(limitedF);
}
}
@@ -2651,7 +2546,7 @@ namespace Microsoft.Dafny {
public readonly Bpl.Expr! HeapExpr;
public readonly PredefinedDecls! predef;
public readonly Translator! translator;
- readonly bool applyAltFunctions;
+ readonly Function applyLimited_CurrentFunction;
public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Token! heapToken) {
this.translator = translator;
@@ -2665,27 +2560,25 @@ namespace Microsoft.Dafny {
this.HeapExpr = heap;
}
- ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Bpl.Expr! heap, bool applyAltFunctions) {
+ ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Bpl.Expr! heap, Function applyLimited_CurrentFunction) {
this.translator = translator;
this.predef = predef;
this.HeapExpr = heap;
- this.applyAltFunctions = applyAltFunctions;
+ this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
}
ExpressionTranslator oldEtran;
public ExpressionTranslator! Old {
get {
if (oldEtran == null) {
- oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyAltFunctions);
+ oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyLimited_CurrentFunction);
}
return oldEtran;
}
}
- public ExpressionTranslator! AltFunctions {
- get {
- return new ExpressionTranslator(translator, predef, HeapExpr, true);
- }
+ public ExpressionTranslator! LimitedFunctions(Function! applyLimited_CurrentFunction) {
+ return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction);
}
public Bpl.IdentifierExpr! TheFrame(Token! tok)
@@ -2795,10 +2688,13 @@ namespace Microsoft.Dafny {
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
string nm = ((!)e.Function).FullName;
- if (e is UseExpr) {
- nm += "#use";
- } else if (this.applyAltFunctions && e.Function.IsUse) {
- nm += "#alt";
+ if (this.applyLimited_CurrentFunction != null && e.Function.IsRecursive && !e.Function.IsUnlimited) {
+ ModuleDecl module = ((!)e.Function.EnclosingClass).Module;
+ if (module == ((!)applyLimited_CurrentFunction.EnclosingClass).Module) {
+ if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) {
+ nm += "#limited";
+ }
+ }
}
Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(expr.tok, nm, translator.TrType((!)e.Type));
Bpl.ExprSeq args = new Bpl.ExprSeq();
@@ -3019,17 +2915,26 @@ namespace Microsoft.Dafny {
translator.FunctionCall(tok, BuiltinFunction.SeqSameUntil, null, e0, e1, len0));
}
- public Bpl.Expr! TrUseExpr(FunctionCallExpr! e) {
- Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(e.tok, ((!)e.Function).FullName + "#use", translator.TrType((!)e.Type));
+ public Bpl.Expr! TrUseExpr(FunctionCallExpr! e)
+ requires e.Function != null && e.Type != null;
+ {
+ Function fn = e.Function;
Bpl.ExprSeq args = new Bpl.ExprSeq();
args.Add(HeapExpr);
- if (!e.Function.IsStatic) {
+ if (!fn.IsStatic) {
args.Add(TrExpr(e.Receiver));
}
foreach (Expression ee in e.Args) {
args.Add(TrExpr(ee));
}
- return new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args);
+ Bpl.Expr f0 = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(e.tok, fn.FullName, translator.TrType(e.Type))), args);
+ Bpl.Expr f1;
+ if (fn.IsRecursive && !fn.IsUnlimited) {
+ f1 = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(e.tok, fn.FullName + "#limited", translator.TrType(e.Type))), args);
+ } else {
+ f1 = f0;
+ }
+ return Bpl.Expr.Eq(f0, f1);
}
public Bpl.Expr! CondApplyBox(Token! tok, Bpl.Expr! e, Type! fromType, Type! toType) {
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 86c12854..ec255ed1 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -53,10 +53,10 @@ class Array {
i := i + 1;
}
}
- function method Length(): int
+ function method Length(): int
reads this;
{ |contents| }
- function method Get(i: int): int
+ function method Get(i: int): int
requires 0 <= i && i < |contents|;
reads this;
{ contents[i] }
@@ -88,14 +88,9 @@ method Main() {
method TestSearch(a: Array, key: int)
requires a != null;
- requires (forall i, j ::
- 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
+ requires (forall i, j :: 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
{
- assert (forall i, j ::
- 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
var b := new Benchmark2;
- assert (forall i, j ::
- 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
call r := b.BinarySearch(a, key);
print "Looking for key=", key, ", result=", r, "\n";
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3718618e..7ac8ff37 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -321,35 +321,35 @@ Dafny program verifier finished with 10 verified, 0 errors
Dafny program verifier finished with 13 verified, 0 errors
-------------------- Use.dfy --------------------
-Use.dfy(14,18): Error: assertion violation
+Use.dfy(16,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(24,18): Error: assertion violation
+Use.dfy(26,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(33,18): Error: assertion violation
+Use.dfy(35,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(52,12): Error: assertion violation
+Use.dfy(54,12): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(82,17): Error: assertion violation
+Use.dfy(84,17): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(124,23): Error: assertion violation
+Use.dfy(126,23): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(136,5): Error: assertion violation
+Use.dfy(138,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(136,5): Error: assertion violation
+Use.dfy(138,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(207,19): Error: assertion violation
+Use.dfy(209,19): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 38 verified, 9 errors
+Dafny program verifier finished with 39 verified, 9 errors
-------------------- DTypes.dfy --------------------
DTypes.dfy(15,14): Error: assertion violation
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 714e9d58..8b4892dd 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -64,10 +64,12 @@ class IntSet {
m := n;
} else {
if (x < n.data) {
+ assert n.right == null || n.right.Valid();
call t := InsertHelper(x, n.left);
n.left := t;
n.footprint := n.footprint + n.left.footprint;
} else {
+ assert n.left == null || n.left.Valid();
call t := InsertHelper(x, n.right);
n.right := t;
n.footprint := n.footprint + n.right.footprint;
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 4bf6ae30..b69fa4f6 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -176,7 +176,7 @@ class StatementTwoShoes {
}
}
- use function G(w: int): int { 5 }
+ function G(w: int): int { 5 }
function method H(x: int): int;
method V(s: set<StatementTwoShoes>, a: int, b: int)
diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
index 7f0085e0..62636ce5 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny0/ListContents.dfy
@@ -5,7 +5,7 @@ class Node<T> {
var data: T;
var next: Node<T>;
- use function Valid(): bool
+ function Valid(): bool
reads this, footprint;
{
this in this.footprint && null !in this.footprint &&
diff --git a/Test/dafny0/Substitution.dfy b/Test/dafny0/Substitution.dfy
index 195c9257..9668afb9 100644
--- a/Test/dafny0/Substitution.dfy
+++ b/Test/dafny0/Substitution.dfy
@@ -67,7 +67,7 @@ static function Substitute(e: Expression, v: int, val: int): Expression
case Nary(op, args) => #Expression.Nary(op, SubstSeq(e, args, v, val))
}
-use static function SubstSeq(/*ghost*/ parent: Expression,
+static function SubstSeq(/*ghost*/ parent: Expression,
q: seq<Expression>, v: int, val: int): seq<Expression>
requires (exists op,args :: parent == #Expression.Nary(op, args) && q <= args);
decreases parent, false, q;
diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy
index 42a82fe6..f3359778 100644
--- a/Test/dafny0/SumOfCubes.dfy
+++ b/Test/dafny0/SumOfCubes.dfy
@@ -1,5 +1,5 @@
class SumOfCubes {
- static use function SumEmUp(n: int, m: int): int
+ static function SumEmUp(n: int, m: int): int
requires 0 <= n && n <= m;
decreases m - n;
{
@@ -42,7 +42,7 @@ class SumOfCubes {
call Lemma3(0, k);
}
- static use function GSum(k: int): int
+ static function GSum(k: int): int
requires 0 <= k;
decreases k;
{
@@ -87,7 +87,7 @@ class SumOfCubes {
}
}
- static use function SumEmDown(n: int, m: int): int
+ static function SumEmDown(n: int, m: int): int
requires 0 <= n && n <= m;
decreases m;
{
diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index 58cb6bea..aaf41190 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -1,10 +1,12 @@
class T {
var x: int;
- use function F(y: int): int
+ function F(y: int): int
+ decreases false;
{
- 2*y
+ 2*y + (if 1 < 0 then FEntry(y) else 0)
}
+ function FEntry(y: int): int decreases true; { F(y) }
method M(s: set<T>) {
use F(4);
@@ -14,9 +16,9 @@ class T {
assert F(72) == 14; // error (just plain wrong)
}
- use function FF(y: int): int
+ function FF(y: int): int
{
- F(y)
+ FEntry(y)
}
method MM() {
@@ -33,11 +35,11 @@ class T {
assert FF(9) == 18; // error (definition of F not engaged; the use of FF does not help)
}
- use function G(y: int): bool
+ function G(y: int): bool decreases false;
{
- 0 <= y
+ 0 <= y || (1 < 0 && GG(y))
}
- use function GG(y: int): bool
+ unlimited function GG(y: int): bool decreases true;
{
G(y)
}
@@ -52,13 +54,13 @@ class T {
assert !GG(-7); // error (the negation disables the expansion of GG in the assert)
}
- use function H(): int
- reads this;
+ function H(): int
+ reads this; decreases false;
{
- x
+ x + (if 1 < 0 then HH() else 0)
}
- use function HH(): int
- reads this;
+ unlimited function HH(): int
+ reads this; decreases true;
{
H()
}
@@ -125,13 +127,13 @@ class T {
// case nothing is known about how H() changed
}
- use function K(): bool
- reads this;
+ function K(): bool
+ reads this; decreases false;
{
- x <= 100
+ x <= 100 || (1 < 0 && KK())
}
- use function KK(): bool
- reads this;
+ unlimited function KK(): bool
+ reads this; decreases true;
{
K()
}
@@ -148,7 +150,7 @@ class T {
requires KK();
modifies this;
{
- use K(); // KK in the precondition and KK's definition give K#alt, which this use expands
+ use K(); // KK in the precondition and KK's definition give K#limited, which this use expands
x := x - 1;
assert KK(); // the assert expands KK to K, definition of K expands K
}
@@ -174,7 +176,7 @@ class T {
}
class Recursive {
- use function Gauss(n: int): int
+ function Gauss(n: int): int
requires 0 <= n;
decreases n;
{
@@ -195,7 +197,7 @@ class Recursive {
}
}
- use function Fib(n: int): int
+ function Fib(n: int): int
requires 0 <= n;
decreases n;
{
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 34fc96f2..7b5de59a 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -30,7 +30,7 @@
]\\)*" . font-lock-comment-face)
`(,(dafny-regexp-opt '(
- "class" "datatype" "function" "frame" "ghost" "var" "method"
+ "class" "datatype" "function" "frame" "ghost" "var" "method" "unlimited"
"module" "imports" "static"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 2b9918f9..1f891a71 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -6,9 +6,9 @@
\lstdefinelanguage{dafny}{
morekeywords={class,datatype,bool,int,object,set,seq,%
- function,returns,
+ function,unlimited,
ghost,var,static,
- method,module,imports,in,
+ method,returns,module,imports,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
match,case,false,true,null,old,fresh,this,
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 10:10:49 +0000