summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar qunyanm <qunyanm@hotmail.com>2015-11-16 12:27:44 -0800
committerGravatar qunyanm <qunyanm@hotmail.com>2015-11-16 12:27:44 -0800
commita799e128af68911228d081202ba0bd294ced4a4f (patch)
tree12562ee9b4b767d55221bddbc8bf849da7f0b3eb /Source
parent3f417a0223b4e5d0139c5b035e573895ac2ad84c (diff)
Use EndCurly token for the ReturnCmd when creating unifiedExit
Instead of using NoToken for the ReturnCmd, use the EndCurly, if it exists, when creating unifiedExit
Diffstat (limited to 'Source')
-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 b26750ab..0e5fce82 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(impl.StructuredStmts.EndCurly));
+ 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) {