summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs7
1 files changed, 6 insertions, 1 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 6a2eec29..8c54bdf0 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1133,7 +1133,12 @@ namespace VC {
}
if (returnBlocks > 1) {
string unifiedExitLabel = "GeneratedUnifiedExit";
- Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(Token.NoToken));
+ Block unifiedExit;
+ if (impl.StructuredStmts != null) {
+ unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(impl.StructuredStmts.EndCurly));
+ } else {
+ unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(Token.NoToken));
+ }
Contract.Assert(unifiedExit != null);
foreach (Block b in impl.Blocks) {
if (b.TransferCmd is ReturnCmd) {