summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg7
-rw-r--r--Source/Dafny/DafnyAst.cs9
-rw-r--r--Source/Dafny/Parser.cs5
-rw-r--r--Source/Dafny/Printer.cs4
-rw-r--r--Source/Dafny/Resolver.cs5
-rw-r--r--Source/Dafny/Translator.cs178
-rw-r--r--Test/dafny0/Answer103
-rw-r--r--Test/dafny0/LoopModifies.dfy293
-rw-r--r--Test/dafny0/runtest.bat2
-rw-r--r--_admin/Boogie/aste/summary.log15
10 files changed, 538 insertions, 83 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index e117ad67..033bc239 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -843,7 +843,7 @@ WhileStmt<out Statement/*!*/ stmt>
Expression guard;
List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
- List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();
+ List<FrameExpression/*!*/> mod = null;
Statement/*!*/ body;
IToken bodyStart, bodyEnd;
List<GuardedAlternative> alternatives;
@@ -866,7 +866,7 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
= (. bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
decreases = new List<Expression/*!*/>();
- mod = new List<FrameExpression/*!*/>();
+ mod = null;
.)
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
@@ -875,7 +875,8 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
Expression<out e> (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
";"
| "decreases" DecreasesList<decreases, true> ";"
- | "modifies" [ FrameExpression<out fe> (. mod.Add(fe); .)
+ | "modifies" (. mod = mod ?? new List<FrameExpression>(); .)
+ [ FrameExpression<out fe> (. mod.Add(fe); .)
{ "," FrameExpression<out fe> (. mod.Add(fe); .)
}
] ";"
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index dc925519..0fd83011 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1661,11 +1661,12 @@ namespace Microsoft.Dafny {
public readonly List<MaybeFreeExpression/*!*/>/*!*/ Invariants;
public readonly List<Expression/*!*/>/*!*/ Decreases;
public readonly List<FrameExpression/*!*/>/*!*/ Mod;
+ public readonly bool explictModifies;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Invariants));
Contract.Invariant(cce.NonNullElements(Decreases));
- Contract.Invariant(cce.NonNullElements(Mod));
+ Contract.Invariant(Mod == null || cce.NonNullElements(Mod));
}
public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)
: base(tok)
@@ -1673,7 +1674,7 @@ namespace Microsoft.Dafny {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(invariants));
Contract.Requires(cce.NonNullElements(decreases));
- Contract.Requires(cce.NonNullElements(mod));
+ Contract.Requires(mod == null || cce.NonNullElements(mod));
this.Invariants = invariants;
this.Decreases = decreases;
@@ -1691,7 +1692,7 @@ namespace Microsoft.Dafny {
}
public WhileStmt(IToken tok, Expression guard,
- List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod,
+ List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/> mod,
Statement/*!*/ body)
: base(tok, invariants, decreases, mod) {
Contract.Requires(tok != null);
@@ -1709,7 +1710,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(Alternatives != null);
}
public AlternativeLoopStmt(IToken tok,
- List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod,
+ List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/> mod,
List<GuardedAlternative> alternatives)
: base(tok, invariants, decreases, mod) {
Contract.Requires(tok != null);
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d11e8f08..b77f5e65 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1189,7 +1189,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression guard;
List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
- List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();
+ List<FrameExpression/*!*/> mod = null;
Statement/*!*/ body;
IToken bodyStart, bodyEnd;
List<GuardedAlternative> alternatives;
@@ -1393,7 +1393,7 @@ List<Expression/*!*/>/*!*/ decreases) {
bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
decreases = new List<Expression/*!*/>();
- mod = new List<FrameExpression/*!*/>();
+ mod = null;
while (StartOf(13)) {
if (la.kind == 29 || la.kind == 59) {
@@ -1412,6 +1412,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(17);
} else {
Get();
+ mod = mod ?? new List<FrameExpression>();
if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index a8970f05..9970d61a 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -507,6 +507,10 @@ namespace Microsoft.Dafny {
PrintSpec("invariant", s.Invariants, indent + IndentAmount);
PrintSpecLine("decreases", s.Decreases, indent + IndentAmount);
+ if (s.Mod != null)
+ {
+ PrintFrameSpecLine("modifies", s.Mod, indent + IndentAmount);
+ }
Indent(indent);
PrintStatement(s.Body, indent);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 17309836..c0bf4392 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1512,6 +1512,11 @@ namespace Microsoft.Dafny {
}
// any type is fine
}
+ if(s.Mod != null) {
+ foreach (FrameExpression fe in s.Mod) {
+ ResolveFrameExpression(fe, "modifies");
+ }
+ }
s.IsGhost = bodyMustBeSpecOnly;
loopStack.Add(s); // push
if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 07e328a0..b2c46c8a 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1003,7 +1003,7 @@ namespace Microsoft.Dafny {
// play havoc with the heap according to the modifies clause
builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
// assume the usual two-state boilerplate information
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, currentMethod, etran.Old, etran)) {
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, currentMethod.Mod, etran.Old, etran, etran.Old)) {
if (tri.IsFree) {
builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));
}
@@ -1049,7 +1049,7 @@ namespace Microsoft.Dafny {
Contract.Requires(predef != null);
// set up the information used to verify the method's modifies clause
- DefineFrame(m.tok, m.Mod, builder, localVariables);
+ DefineFrame(m.tok, m.Mod, builder, localVariables, null);
}
Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {
@@ -1065,7 +1065,7 @@ namespace Microsoft.Dafny {
return CaptureState(tok, null);
}
- void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables){
+ void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables, string name){
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(frameClause));
Contract.Requires(builder != null);
@@ -1074,9 +1074,9 @@ namespace Microsoft.Dafny {
ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);
// Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool
- Bpl.IdentifierExpr theFrame = etran.TheFrame(tok); // this is a throw-away expression, used only to extract the name and type of the $_Frame variable
+ Bpl.IdentifierExpr theFrame = etran.TheFrame(tok); // this is a throw-away expression, used only to extract the type of the $_Frame variable
Contract.Assert(theFrame.Type != null); // follows from the postcondition of TheFrame
- Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, theFrame.Name, theFrame.Type));
+ Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name ?? theFrame.Name, theFrame.Type));
localVariables.Add(frame);
// $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause);
Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
@@ -1099,14 +1099,14 @@ namespace Microsoft.Dafny {
{
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(calleeFrame));
- Contract.Requires(receiverReplacement != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ Contract.Requires((receiverReplacement == null) == (substMap == null));
+ Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Requires(etran != null);
Contract.Requires(builder != null);
Contract.Requires(errorMessage != null);
Contract.Requires(predef != null);
- // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in calleeFrame ==> $_Frame[o,f]);
+ // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> $_Frame[o,f]);
Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
@@ -1230,7 +1230,7 @@ namespace Microsoft.Dafny {
Contract.Requires(f != null);
Contract.Requires(etran != null);
Contract.Requires(cce.NonNullElements(rw));
- Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Requires(predef != null);
Contract.Requires((receiverReplacement == null) == (substMap == null));
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
@@ -1241,8 +1241,8 @@ namespace Microsoft.Dafny {
Bpl.Expr disjunction = null;
foreach (FrameExpression rwComponent in rw) {
Expression e = rwComponent.E;
- if (substMap != null) {
- Contract.Assert(receiverReplacement != null);
+ if (receiverReplacement != null) {
+ Contract.Assert(substMap != null);
e = Substitute(e, receiverReplacement, substMap);
}
Bpl.Expr disjunct;
@@ -1355,7 +1355,7 @@ namespace Microsoft.Dafny {
}
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
- DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals);
+ DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals, null);
CheckWellformedWithResult(f.Body, new WFOptions(f, null, true), funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);
// check that postconditions hold
@@ -2539,7 +2539,7 @@ namespace Microsoft.Dafny {
}
comment = null;
}
- if (!skipEnsures) foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m, etran.Old, etran)) {
+ if (!skipEnsures) foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod, etran.Old, etran, etran.Old)) {
ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
}
}
@@ -2766,15 +2766,15 @@ namespace Microsoft.Dafny {
/// <summary>
/// There are 3 states of interest when generating two-state boilerplate:
- /// S0. the beginning of the method, which is where the modifies clause is interpreted
+ /// S0. the beginning of the method or loop, which is where the modifies clause is interpreted
/// S1. the pre-state of the two-state interval
/// S2. the post-state of the two-state interval
- /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
+ /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0.
/// </summary>
- List<BoilerplateTriple/*!*/>/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, Method/*!*/ method, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran)
+ List<BoilerplateTriple/*!*/>/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)
{
Contract.Requires(tok != null);
- Contract.Requires(method != null);
+ Contract.Requires(modifiesClause != null);
Contract.Requires(etranPre != null);
Contract.Requires(etran != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<BoilerplateTriple>>()));
@@ -2782,7 +2782,7 @@ namespace Microsoft.Dafny {
List<BoilerplateTriple> boilerplate = new List<BoilerplateTriple>();
// the frame condition, which is free since it is checked with every heap update and call
- boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, method.Mod, etranPre, etran), null, "frame condition"));
+ boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, etranPre, etran, etranMod), null, "frame condition"));
// HeapSucc(S1, S2)
Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);
@@ -2792,13 +2792,13 @@ namespace Microsoft.Dafny {
}
/// <summary>
- /// There are 3 states of interest when generating a freame condition:
- /// S0. the beginning of the method, which is where the modifies clause is interpreted
+ /// There are 3 states of interest when generating a frame condition:
+ /// S0. the beginning of the method/loop, which is where the modifies clause is interpreted
/// S1. the pre-state of the two-state interval
/// S2. the post-state of the two-state interval
- /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
+ /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0.
/// </summary>
- Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran)
+ Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)
{
Contract.Requires(tok != null);
Contract.Requires(etran != null);
@@ -2820,15 +2820,43 @@ namespace Microsoft.Dafny {
Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, o, f);
Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);
- Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.Old.IsAlloced(tok, o));
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranMod.IsAlloced(tok, o));
Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
- consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etran.Old, null, null));
+ consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etranMod, null, null));
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
}
-
+ Bpl.Expr/*!*/ FrameConditionUsingDefinedFrame(IToken/*!*/ tok, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(etran != null);
+ Contract.Requires(etranPre != null);
+ Contract.Requires(predef != null);
+ Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
+
+ // generate:
+ // (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] }
+ // o != null && old($Heap)[o,alloc] ==>
+ // $Heap[o,f] == PreHeap[o,f] ||
+ // $_Frame[o,f])
+ Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
+ Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
+ Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
+
+ Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, o, f);
+ Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranPre.IsAlloced(tok, o));
+ Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
+
+ consequent = Bpl.Expr.Or(consequent, Bpl.Expr.SelectTok(tok, etranMod.TheFrame(tok), o, f));
+
+ Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
+ return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
+ }
// ----- Type ---------------------------------------------------------------------------------
Bpl.Type TrType(Type type)
@@ -3120,7 +3148,7 @@ namespace Microsoft.Dafny {
AddComment(builder, stmt, "while statement");
var s = (WhileStmt)stmt;
TrLoop(s, s.Guard,
- delegate(Bpl.StmtListBuilder bld) { TrStmt(s.Body, bld, locals, etran); },
+ delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrStmt(s.Body, bld, locals, e); },
builder, locals, etran);
} else if (stmt is AlternativeLoopStmt) {
@@ -3129,7 +3157,7 @@ namespace Microsoft.Dafny {
var tru = new LiteralExpr(s.Tok, true);
tru.Type = Type.Bool; // resolve here
TrLoop(s, tru,
- delegate(Bpl.StmtListBuilder bld) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, etran); },
+ delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, e); },
builder, locals, etran);
} else if (stmt is ForeachStmt) {
@@ -3322,7 +3350,7 @@ namespace Microsoft.Dafny {
}
}
- delegate void BodyTranslator(Bpl.StmtListBuilder builder);
+ delegate void BodyTranslator(Bpl.StmtListBuilder builder, ExpressionTranslator etran);
void TrLoop(LoopStmt s, Expression Guard, BodyTranslator bodyTr,
Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {
@@ -3343,6 +3371,17 @@ namespace Microsoft.Dafny {
locals.Add(preLoopHeapVar);
Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(s.Tok, preLoopHeapVar);
ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);
+ ExpressionTranslator updatedFrameEtran;
+ string loopFrameName = "#_Frame#" + loopId;
+ if(s.Mod != null)
+ updatedFrameEtran = new ExpressionTranslator(etran, loopFrameName);
+ else
+ updatedFrameEtran = etran;
+
+ if (s.Mod != null) { // check that the modifies is a strict subset
+ CheckFrameSubset(s.Tok, s.Mod, null, null, etran, builder, "loop modifies clause may violate context's modifies clause", null);
+ DefineFrame(s.Tok, s.Mod, builder, locals, loopFrameName);
+ }
builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr));
List<Bpl.Expr> initDecr = null;
@@ -3390,14 +3429,19 @@ namespace Microsoft.Dafny {
TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true);
}
// include boilerplate invariants
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, currentMethod, etranPreLoop, etran)) {
- if (tri.IsFree) {
- invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));
- } else {
- Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant
- invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));
- }
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, currentMethod.Mod, etranPreLoop, etran, etran.Old))
+ {
+ if (tri.IsFree) {
+ invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));
+ }
+ else {
+ Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant
+ invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));
+ }
}
+ // add a free invariant which says that the heap hasn't changed outside of the modifies clause.
+ invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));
+
// include a free invariant that says that all completed iterations so far have only decreased the termination metric
if (initDecr != null) {
List<IToken> toks = new List<IToken>();
@@ -3430,11 +3474,11 @@ namespace Microsoft.Dafny {
// termination checking
if (Contract.Exists(theDecreases, e => e is WildcardExpr)) {
// omit termination checking for this loop
- bodyTr(loopBodyBuilder);
+ bodyTr(loopBodyBuilder, updatedFrameEtran);
} else {
List<Bpl.Expr> oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$");
// time for the actual loop body
- bodyTr(loopBodyBuilder);
+ bodyTr(loopBodyBuilder, updatedFrameEtran);
// check definedness of decreases expressions
List<IToken> toks = new List<IToken>();
List<Type> types = new List<Type>();
@@ -3585,8 +3629,8 @@ namespace Microsoft.Dafny {
ins.Add(param);
}
- // Check modifies clause
- CheckFrameSubset(tok, method.Mod, receiver, substMap, etran, builder, "call may violate caller's modifies clause", null);
+ // Check modifies clause of a subcall is a subset of the current frame.
+ CheckFrameSubset(tok, method.Mod, receiver, substMap, etran, builder, "call may violate context's modifies clause", null);
// Check termination
ModuleDecl module = cce.NonNull(method.EnclosingClass).Module;
@@ -4133,7 +4177,7 @@ namespace Microsoft.Dafny {
"$obj" + i, predef.RefType, builder, locals);
prevObj[i] = obj;
// check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj]);
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing context's modifies clause"));
// check that this LHS is not the same as any previous LHSs
for (int j = 0; j < i; j++) {
@@ -4164,7 +4208,7 @@ namespace Microsoft.Dafny {
prevObj[i] = obj;
prevIndex[i] = fieldName;
// check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj,index]);
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause"));
// check that this LHS is not the same as any previous LHSs
for (int j = 0; j < i; j++) {
@@ -4195,7 +4239,7 @@ namespace Microsoft.Dafny {
"$index" + i, predef.FieldName(mse.tok, predef.BoxType), builder, locals);
prevObj[i] = obj;
prevIndex[i] = fieldName;
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause"));
// check that this LHS is not the same as any previous LHSs
for (int j = 0; j < i; j++) {
@@ -4376,6 +4420,7 @@ namespace Microsoft.Dafny {
public readonly PredefinedDecls predef;
public readonly Translator translator;
public readonly string This;
+ public readonly string modifiesFrame = "$_Frame"; // the name of the context's frame variable.
readonly Function applyLimited_CurrentFunction;
readonly int layerOffset = 0;
public int Statistics_FunctionCount = 0;
@@ -4420,18 +4465,34 @@ namespace Microsoft.Dafny {
this.HeapExpr = heap;
this.This = thisVar;
}
-
- ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset) {
- Contract.Requires(translator != null);
- Contract.Requires(predef != null);
- Contract.Requires(heap != null);
- Contract.Requires(applyLimited_CurrentFunction != null);
- this.translator = translator;
- this.predef = predef;
- this.HeapExpr = heap;
- this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
- this.This = "this";
- this.layerOffset = layerOffset;
+
+ ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset)
+ {
+ Contract.Requires(translator != null);
+ Contract.Requires(predef != null);
+ Contract.Requires(heap != null);
+ Contract.Requires(applyLimited_CurrentFunction != null);
+ this.translator = translator;
+ this.predef = predef;
+ this.HeapExpr = heap;
+ this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
+ this.This = "this";
+ this.layerOffset = layerOffset;
+ }
+
+ public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame)
+ {
+ Contract.Requires(etran != null);
+ Contract.Requires(modifiesFrame != null);
+ this.translator = etran.translator;
+ this.HeapExpr = etran.HeapExpr;
+ this.predef = etran.predef;
+ this.This = etran.This;
+ this.applyLimited_CurrentFunction = etran.applyLimited_CurrentFunction;
+ this.layerOffset = etran.layerOffset;
+ this.Statistics_FunctionCount = etran.Statistics_FunctionCount;
+ this.oldEtran = etran.oldEtran;
+ this.modifiesFrame = modifiesFrame;
}
ExpressionTranslator oldEtran;
@@ -4476,7 +4537,7 @@ namespace Microsoft.Dafny {
Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta");
Bpl.Type fieldAlpha = predef.FieldName(tok, alpha);
Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.TypeSeq(predef.RefType, fieldAlpha), Bpl.Type.Bool);
- return new Bpl.IdentifierExpr(tok, "$_Frame", ty);
+ return new Bpl.IdentifierExpr(tok, this.modifiesFrame ?? "$_Frame", ty);
}
public Bpl.IdentifierExpr Tick() {
@@ -5941,11 +6002,12 @@ namespace Microsoft.Dafny {
static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
Contract.Requires(expr != null);
+ Contract.Requires(receiverReplacement != null);
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(Contract.Result<Expression>() != null);
Expression newExpr = null; // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end
-
+
if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) {
// nothing to substitute
} else if (expr is ThisExpr) {
@@ -6103,8 +6165,10 @@ namespace Microsoft.Dafny {
static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,
Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
Contract.Requires(cce.NonNullElements(elist));
- Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ Contract.Requires((receiverReplacement == null) == (substMap == null));
+ Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));
+
List<Expression> newElist = null; // initialized lazily
for (int i = 0; i < elist.Count; i++)
{cce.LoopInvariant( newElist == null || newElist.Count == i);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 29b8e708..da82fd59 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -147,16 +147,16 @@ Execution trace:
SmallTests.dfy(81,5): anon9_LoopHead
(0,0): anon9_LoopBody
(0,0): anon10_Then
-SmallTests.dfy(116,5): Error: call may violate caller's modifies clause
+SmallTests.dfy(116,5): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(129,9): Error: call may violate caller's modifies clause
+SmallTests.dfy(129,9): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(131,9): Error: call may violate caller's modifies clause
+SmallTests.dfy(131,9): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
@@ -453,7 +453,7 @@ ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
9 parse errors detected in ParseErrors.dfy
-------------------- Array.dfy --------------------
-Array.dfy(10,8): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
@@ -468,13 +468,13 @@ Execution trace:
Array.dfy(48,20): Error: assertion violation
Execution trace:
(0,0): anon0
-Array.dfy(56,8): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(56,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
-Array.dfy(63,8): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
@@ -493,10 +493,10 @@ Execution trace:
(0,0): anon7_Else
(0,0): anon8_Then
(0,0): anon9_Then
-Array.dfy(131,6): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(131,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-Array.dfy(138,6): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(138,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -632,7 +632,7 @@ Basics.dfy(147,10): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon3
-Basics.dfy(147,10): Error: assignment may update an object not in the enclosing method's modifies clause
+Basics.dfy(147,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3
@@ -1000,3 +1000,88 @@ RefinementErrors.dfy(42,9): Error: Refined class has a member with the same name
RefinementErrors.dfy(12,10): Error: Refinement methods can only be declared in refinement classes: M
RefinementErrors.dfy(34,10): Error: Different number of output variables
6 resolution/type errors detected in RefinementErrors.dfy
+
+-------------------- LoopModifies.dfy --------------------
+LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+LoopModifies.dfy(17,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(14,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(14,4): anon10_Else
+ (0,0): anon5
+ LoopModifies.dfy(14,4): anon12_Else
+ (0,0): anon7
+LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(42,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(42,4): anon10_Else
+ (0,0): anon5
+ LoopModifies.dfy(42,4): anon12_Else
+ (0,0): anon7
+LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(57,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(57,4): anon10_Else
+ (0,0): anon5
+ LoopModifies.dfy(57,4): anon12_Else
+ (0,0): anon7
+LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+LoopModifies.dfy(98,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(90,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(90,4): anon10_Else
+ (0,0): anon5
+ LoopModifies.dfy(90,4): anon12_Else
+ (0,0): anon7
+LoopModifies.dfy(146,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(134,4): anon17_LoopHead
+ (0,0): anon17_LoopBody
+ LoopModifies.dfy(134,4): anon18_Else
+ (0,0): anon5
+ LoopModifies.dfy(134,4): anon20_Else
+ (0,0): anon7
+ LoopModifies.dfy(139,7): anon21_LoopHead
+ (0,0): anon21_LoopBody
+ LoopModifies.dfy(139,7): anon22_Else
+ (0,0): anon12
+ LoopModifies.dfy(139,7): anon24_Else
+ (0,0): anon14
+LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(193,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(193,4): anon10_Else
+ (0,0): anon5
+ LoopModifies.dfy(193,4): anon12_Else
+ (0,0): anon7
+LoopModifies.dfy(260,10): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(248,4): anon17_LoopHead
+ (0,0): anon17_LoopBody
+ LoopModifies.dfy(248,4): anon18_Else
+ (0,0): anon5
+ LoopModifies.dfy(248,4): anon20_Else
+ (0,0): anon7
+ LoopModifies.dfy(256,7): anon21_LoopHead
+ (0,0): anon21_LoopBody
+ LoopModifies.dfy(256,7): anon22_Else
+ (0,0): anon12
+ LoopModifies.dfy(256,7): anon24_Else
+ (0,0): anon14
+
+Dafny program verifier finished with 21 verified, 9 errors
diff --git a/Test/dafny0/LoopModifies.dfy b/Test/dafny0/LoopModifies.dfy
new file mode 100644
index 00000000..17a4228e
--- /dev/null
+++ b/Test/dafny0/LoopModifies.dfy
@@ -0,0 +1,293 @@
+
+// regular modifies sanity test:
+method Testing1(a: array<int>)
+ requires a != null && a.Length > 0;
+{
+ a[0] := 0;
+}
+
+// array inside while loop, without explict modifies clause:
+method Testing2(a: array<int>)
+ requires a != null && a.Length > 0;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// array inside while loop, without explict modifies clause:
+method Testing2A(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ {
+ // now there is no problem.
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// array inside while loop, with explict modifies clause:
+method Testing3(a: array<int>)
+ requires a != null && a.Length > 0;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// modifies restricts:
+method Testing4(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+ // should be ok.
+ a[0] := 1;
+}
+
+// modifies not a subset:
+method Testing5(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// modifies is a subset, but modifications occur outside:
+method Testing6(a: array<int>, b: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ modifies a, b;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ // cool.
+ a[0] := i;
+
+ // not cool.
+ b[0] := i;
+ i := i + 1;
+ }
+}
+
+// heap outside modifies is actually preserved:
+method Testing7(a: array<int>, b: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ requires a != b;
+ modifies a, b;
+{
+ var i := 0;
+ b[0] := 4;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ // still good.
+ a[0] := i;
+ i := i + 1;
+ }
+ // this is new, and good:
+ assert b[0] == 4;
+}
+
+// modifies actually restrict frame when nested:
+method Testing8(a: array<int>, b: array<int>, c: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ requires c != null && c.Length > 0;
+ requires a != b && b != c && c != a;
+ modifies a, b, c;
+{
+ var i := 0;
+ b[0] := 4;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a, b;
+ {
+ var j := 0;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies a;
+ {
+ // happy:
+ a[0] := j;
+ // not happy:
+ b[0] := i;
+ j := j + 1;
+ }
+ i := i + 1;
+ }
+ c[0] := 1;
+}
+
+// heap outside modifies preserved when nested:
+method Testing9(a: array<int>, b: array<int>, c: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ requires c != null && c.Length > 0;
+ requires a != b && b != c && c != a;
+ modifies a, b, c;
+{
+ var i := 0;
+ b[0] := 4;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a, b;
+ {
+ var j := 0;
+ b[0] := i;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies a;
+ {
+ a[0] := j;
+ j := j + 1;
+ }
+ assert b[0] == i;
+ i := i + 1;
+ }
+ c[0] := 1;
+}
+
+// allocation, fresh tests:
+
+// allocated things not automatically in modifies of loops:
+method Testing10(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ var arr := new int[1];
+ arr[0] := 1; // good, even though not in method modifies.
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ arr[0] := 1; // bad.
+ i := i + 1;
+ }
+}
+
+// unless no modifies given, in which case the context is used:
+method Testing10a(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ var arr := new int[1];
+ arr[0] := 1; // still good.
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ {
+ arr[0] := 1; // no modifies, so allowed to touch arr.
+ i := i + 1;
+ }
+}
+
+// arr still accessible after loop that can't touch it.
+method Testing11()
+{
+ var i := 0;
+ var arr := new int[1];
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies;
+ {
+ arr := new int[1];
+ arr[0] := 1;
+ var j := 0;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies;
+ {
+ // can't touch arr in here.
+ j := j + 1;
+ }
+ arr[0] := 2;
+ i := i + 1;
+ }
+}
+
+// allocation inside a loop is still ok:
+method Testing11a(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ var arr := new int[1];
+ arr[0] := 1; // can modify arr, even though it
+ // is not in modifies because it is fresh.
+ var j := 0;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies a;
+ {
+ arr[0] := 3; // can't touch arr, as allocated before modifies captured.
+ j := j + 1;
+ }
+ i := i + 1;
+ }
+}
+
+class Elem
+{
+ var i: int;
+}
+
+// capture of modifies clause at beginning of loop:
+method Testing12(a: Elem, b: Elem, c: Elem)
+ requires a != null && b != null && c != null;
+ requires a != b && b != c && c != a; // all different.
+ modifies a, b, c;
+{
+ var i := 0;
+ var S := {a, b, c};
+ // S "captured" here for purposes of modifies clause.
+ while(S != {})
+ modifies S;
+ decreases S;
+ {
+ var j := choose S;
+ // these still good, even though S shrinks to not include them.
+ a.i := i;
+ b.i := i;
+ c.i := i;
+ S := S - {j};
+ i := i + 1;
+ }
+} \ No newline at end of file
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index aed9ee8a..3c64f623 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -18,7 +18,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
- Refinement.dfy RefinementErrors.dfy) do (
+ Refinement.dfy RefinementErrors.dfy LoopModifies.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 %* %%f
diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index 915f69c3..8818d766 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,9 +1,9 @@
-# Aste started: 2011-06-27 07:00:20
+# Aste started: 2011-06-29 07:00:18
# Host id: Boogiebox
-# [2011-06-27 07:03:29] SpecSharp revision: 2197d90f87f3
-# [2011-06-27 07:03:29] SscBoogie revision: 2197d90f87f3
-# [2011-06-27 07:04:52] Boogie revision: f08b2671b170
-[2011-06-27 07:07:35] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
+# [2011-06-29 07:03:22] SpecSharp revision: 7d3617d74144
+# [2011-06-29 07:03:22] SscBoogie revision: 7d3617d74144
+# [2011-06-29 07:04:40] Boogie revision: e77f2e437ca0
+[2011-06-29 07:07:23] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
@@ -31,5 +31,6 @@
warning CS0162: Unreachable code detected
warning CS0162: Unreachable code detected
warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.
-[2011-06-27 07:49:48] 0 out of 30 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
-# [2011-06-27 07:50:49] Released nightly of Boogie
+[2011-06-29 07:49:41] 1 out of 30 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
+['dafny0']
+# [2011-06-29 07:50:44] Released nightly of Boogie
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 14:12:35 +0000