From a799e128af68911228d081202ba0bd294ced4a4f Mon Sep 17 00:00:00 2001
From: qunyanm <qunyanm@hotmail.com>
Date: Mon, 16 Nov 2015 12:27:44 -0800
Subject: 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
---
 Source/VCGeneration/ConditionGeneration.cs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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) {
-- 
cgit v1.2.3