diff options
| author |  qunyanm <qunyanm@hotmail.com> | 2015-11-16 11:03:28 -0800 |
|---|---|---|
| committer | qunyanm <qunyanm@hotmail.com> | 2015-11-16 11:03:28 -0800 |
| commit | 3f417a0223b4e5d0139c5b035e573895ac2ad84c (patch) | |
| tree | f70c01baa8ba5841597f9eb54077d639d73046c3 | |
| parent | 75a179354ea7b78682904575d5692efa0068fcf0 (diff) | |
Use EndCurly token for the ReturnCmd when creating unifiedExit
Instead of using NoToken for the ReturnCmd, use the EndCurly when
creating unifiedExit.
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index ae0a1147..b26750ab 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1133,7 +1133,7 @@ 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 = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(impl.StructuredStmts.EndCurly)); Contract.Assert(unifiedExit != null); foreach (Block b in impl.Blocks) { if (b.TransferCmd is ReturnCmd) { |