diff options
| -rw-r--r-- | Source/Dafny/Translator.cs | 31 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 22 | ||||
| -rw-r--r-- | Test/dafny0/ControlStructures.dfy | 34 |
3 files changed, 58 insertions, 29 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 9628f14b..c961a94d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4883,12 +4883,8 @@ namespace Microsoft.Dafny { TrCallStmt((CallStmt)stmt, builder, locals, etran, null);
} else if (stmt is BlockStmt) {
- foreach (Statement ss in ((BlockStmt)stmt).Body) {
- TrStmt(ss, builder, locals, etran);
- if (ss.Labels != null) {
- builder.AddLabelCmd("after_" + ss.Labels.Data.UniqueId);
- }
- }
+ var s = (BlockStmt)stmt;
+ TrStmtList(s.Body, builder, locals, etran);
} else if (stmt is IfStmt) {
AddComment(builder, stmt, "if statement");
IfStmt s = (IfStmt)stmt;
@@ -5115,9 +5111,7 @@ namespace Microsoft.Dafny { }
// translate the body into b
- foreach (Statement ss in mc.Body) {
- TrStmt(ss, b, locals, etran);
- }
+ TrStmtList(mc.Body, b, locals, etran);
Bpl.Expr guard = Bpl.Expr.Eq(source, r);
ifCmd = new Bpl.IfCmd(mc.tok, guard, b.Collect(mc.tok), ifCmd, els);
@@ -5128,15 +5122,26 @@ namespace Microsoft.Dafny { } else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
- foreach (var ss in s.ResolvedStatements) {
- TrStmt(ss, builder, locals, etran);
- }
+ TrStmtList(s.ResolvedStatements, builder, locals, etran);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
}
+ void TrStmtList(List<Statement> stmts, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {
+ Contract.Requires(stmts != null);
+ Contract.Requires(builder != null);
+ Contract.Requires(locals != null);
+ Contract.Requires(etran != null);
+ foreach (Statement ss in stmts) {
+ TrStmt(ss, builder, locals, etran);
+ if (ss.Labels != null) {
+ builder.AddLabelCmd("after_" + ss.Labels.Data.UniqueId);
+ }
+ }
+ }
+
/// <summary>
/// Generate:
/// havoc Heap \ {this} \ _reads \ _new;
@@ -5600,6 +5605,8 @@ namespace Microsoft.Dafny { // $Heap[this, _new] := $iter_newUpdate;
cmd = Bpl.Cmd.SimpleAssign(iter.tok, currentHeap, ExpressionTranslator.UpdateHeap(iter.tok, currentHeap, th, nwField, updatedSetIE));
builder.Add(cmd);
+ // assume $IsGoodHeap($Heap)
+ builder.Add(AssumeGoodHeap(tok, etran));
}
void TrForallProof(ForallStmt s, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 40725691..7186f30f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -864,7 +864,7 @@ Execution trace: (0,0): anon89_Then
(0,0): anon61
-Dafny program verifier finished with 20 verified, 10 errors
+Dafny program verifier finished with 22 verified, 10 errors
-------------------- Termination.dfy --------------------
Termination.dfy(356,47): Error: failure to decrease termination measure
@@ -1672,36 +1672,36 @@ Execution trace: Dafny program verifier finished with 38 verified, 11 errors
-------------------- Superposition.dfy --------------------
- +
Verifying CheckWellformed$$_0_M0.C.M ...
[0 proof obligations] verified
- +
Verifying Impl$$_0_M0.C.M ...
[4 proof obligations] verified
- +
Verifying CheckWellformed$$_0_M0.C.P ...
[4 proof obligations] verified
- +
Verifying CheckWellformed$$_0_M0.C.Q ...
[3 proof obligations] error
Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon5_Else
- +
Verifying CheckWellformed$$_0_M0.C.R ...
[3 proof obligations] error
Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon5_Else
- +
Verifying CheckWellformed$$_1_M1.C.M ...
[0 proof obligations] verified
- +
Verifying Impl$$_1_M1.C.M ...
[1 proof obligation] verified
- +
Verifying CheckWellformed$$_1_M1.C.P ...
[1 proof obligation] error
Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.
@@ -1710,10 +1710,10 @@ Execution trace: (0,0): anon7_Else
(0,0): anon9_Then
(0,0): anon6
- +
Verifying CheckWellformed$$_1_M1.C.Q ...
[0 proof obligations] verified
- +
Verifying CheckWellformed$$_1_M1.C.R ...
[0 proof obligations] verified
diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy index 2136e2f1..95aff80e 100644 --- a/Test/dafny0/ControlStructures.dfy +++ b/Test/dafny0/ControlStructures.dfy @@ -238,28 +238,50 @@ method TheBreaker_SomeBad(M: int, N: int, O: int) assert M <= i || b == 12; // error: e == 37
}
+method BreakStatements(d: D, n: nat)
+{
+ var i := 0;
+ while i < n {
+ if i % 7 == 3 { break; }
+ match d {
+ case Green =>
+ case Blue =>
+ var j := 63;
+ while j < 3000
+ {
+ if j % n == 0 { break; } // in a previous version, this was translated into a malformed Boogie program
+ if j % (n+1) == 0 { break break; }
+ j := j + 1;
+ }
+ case Red =>
+ case Purple =>
+ }
+ i := i + 1;
+ }
+}
+
// --------------- paren-free syntax ---------------
method PF1(d: D)
requires d == D.Green;
{
- if d != D.Green { // guards can be written without parens
+ if d != D.Green { // guards can be written without parens
match d {
}
}
if { case false => assert false; case true => assert true; }
if {1, 2, 3} <= {1, 2} { // conflict between display set as guard and alternative statement is resolved
- assert false;
+ assert false;
}
while d != D.Green {
- assert false;
+ assert false;
}
while d != D.Green
- decreases 1;
+ decreases 1;
{
- assert false;
+ assert false;
}
while {1, 2, 3} <= {1, 2} {
- assert false;
+ assert false;
}
}
|