summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-05-08 02:19:17 +0000
committerGravatar rustanleino <unknown>2010-05-08 02:19:17 +0000
commite8cfbc8ad2c41ef051431b665c4c43e68cc0ff68 (patch)
tree19bc97f1123e86864c5d5e9574ef3bf3e2cd4436
parente90be508dcf82fd35d88107186059bb37f534acb (diff)
Dafny:
Previously, a "use" function was one whose definition was applied only in limited ways, namely when the function was uttered in a program (possibly in a "use" statement). Now, recursive functions are always limited, unless declared with the new modifier "unlimited". Non-recursive functions are always unlimited. Also new is that only function calls within the same SCC of the call graph use the limited form of the callee. The "use" modifier is no longer supported. The "use" statement is still supported, now for both limited and unlimited functions; but it's probably better and easier to just explicitly mention a function in an assertion, if needed.
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-06 12:10:14 +0000