Initial implementation of return statments with parameters.

1 files changed, 4 insertions, 0 deletions

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index b2c46c8a..e16470c3 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3036,7 +3036,11 @@ namespace Microsoft.Dafny {
         var s = (BreakStmt)stmt;

         builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.UniqueId)));

       } else if (stmt is ReturnStmt) {

+        var s = (ReturnStmt)stmt;

         AddComment(builder, stmt, "return statement");

+        if (s.hiddenUpdate != null) {

+          TrStmt(s.hiddenUpdate, builder, locals, etran);

+        }

         builder.Add(new Bpl.ReturnCmd(stmt.Tok));

       } else if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;