diff options
| -rw-r--r-- | Source/Doomed/VCDoomed.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 33 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 | ||||
| -rw-r--r-- | Test/codeexpr/codeExprBug.bpl | 15 | ||||
| -rw-r--r-- | Test/codeexpr/codeExprBug.bpl.expect | 2 |
5 files changed, 22 insertions, 32 deletions
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index 9f1d8290..6dd3b5ca 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -616,7 +616,7 @@ namespace VC { InjectPreconditions(impl, cc);
// append postconditions, starting in exitBlock and continuing into other blocks, if needed
- exitBlock = InjectPostConditions(impl, exitBlock, gotoCmdOrigins);
+ InjectPostConditions(impl, exitBlock, gotoCmdOrigins);
}
#endregion
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 90e2a9c1..81231fd0 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -798,7 +798,7 @@ namespace VC { /// already been constructed for the implementation (and so
/// is already an element of impl.Blocks)
/// </param>
- protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins) {
+ protected static void InjectPostConditions(Implementation impl, Block unifiedExitBlock, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins) {
Contract.Requires(impl != null);
Contract.Requires(unifiedExitBlock != null);
Contract.Requires(gotoCmdOrigins != null);
@@ -814,53 +814,26 @@ namespace VC { }
Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
- Block insertionPoint = unifiedExitBlock;
- string LabelPrefix = "ReallyLastGeneratedExit";
- int k = 0;
// (free and checked) ensures clauses
foreach (Ensures ens in impl.Proc.Ensures) {
- cce.LoopInvariant(insertionPoint.TransferCmd is ReturnCmd);
-
Contract.Assert(ens != null);
if (!ens.Free) { // skip free ensures clauses
- Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition);
- CodeExpr be = ens.Condition as CodeExpr;
- if (be == null) {
- // This is the normal case, where the postcondition is an ordinary expression
+ Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition);
Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone());
ensCopy.Condition = e;
AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy);
c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced;
- insertionPoint.Cmds.Add(c);
+ unifiedExitBlock.Cmds.Add(c);
if (debugWriter != null) {
c.Emit(debugWriter, 1);
}
- } else {
- // This is a CodeExpr, so append all of its blocks (changing return expressions
- // to assert statements), insert a goto to its head block from the current insertion
- // point, and create a new empty block as the current insertion point.
- // Here goes: First, create the new block, which will become the new insertion
- // point and which will serve as a target for the CodeExpr. Steal the TransferCmd
- // from insertionPoint, since insertionPoint's TransferCmd will soon be replaced anyhow.
- Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new List<Cmd>(), insertionPoint.TransferCmd);
- k++;
- // Second, append the CodeExpr blocks to the implementation's blocks
- ThreadInCodeExpr(impl, nextIP, be, true, debugWriter);
- // Third, make the old insertion-point block goto the entry block of the CodeExpr
- Block beEntry = cce.NonNull(be.Blocks[0]);
- insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { beEntry.Label }, new List<Block> { beEntry });
- beEntry.Predecessors.Add(insertionPoint);
- // Fourth, update the insertion point
- insertionPoint = nextIP;
- }
}
}
if (debugWriter != null) {
debugWriter.WriteLine();
}
- return insertionPoint;
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 5a618b1d..3735388c 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2624,7 +2624,7 @@ namespace VC { InjectPreconditions(impl, cc);
// append postconditions, starting in exitBlock and continuing into other blocks, if needed
- exitBlock = InjectPostConditions(impl, exitBlock, gotoCmdOrigins);
+ InjectPostConditions(impl, exitBlock, gotoCmdOrigins);
}
#endregion
diff --git a/Test/codeexpr/codeExprBug.bpl b/Test/codeexpr/codeExprBug.bpl new file mode 100644 index 00000000..4eb86789 --- /dev/null +++ b/Test/codeexpr/codeExprBug.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure p() returns ($r: int);
+ ensures |{ $bb0: return ($r == 1); }|;
+
+implementation p() returns ($x: int)
+{
+ $x := 1;
+ return;
+}
+
+procedure q()
+ ensures |{ var $b: bool; $0: $b := true; goto $1; $1: return $b; }|;
+{
+}
diff --git a/Test/codeexpr/codeExprBug.bpl.expect b/Test/codeexpr/codeExprBug.bpl.expect new file mode 100644 index 00000000..3de74d3e --- /dev/null +++ b/Test/codeexpr/codeExprBug.bpl.expect @@ -0,0 +1,2 @@ +
+Boogie program verifier finished with 2 verified, 0 errors
|