Cleaned up the sink: removed the OutVars, which was state the sink needed only for assigning the local copy of a method's parameter to the out parameter of the Boogie procedure. But now that is simplified: instead of three versions of each parameter (in, local, and out), there are only two: in and out. For a parameter that is *not* by reference and is *not* an out parameter (i.e., just a plain pass-by-value parameter), the "out" version is a local variable. Otherwise it is an out parameter of the Boogie procedure.

1 files changed, 0 insertions, 7 deletions

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index c528e846..8ca54050 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -141,13 +141,6 @@ namespace BytecodeTranslator
     public override void Visit(IReturnStatement returnStatement) {

       Bpl.IToken tok = TokenFor(returnStatement);

 

-      #region Copy values of all out parameters to outvariables

-      foreach (MethodParameter mp in this.sink.OutVars) {

-        StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

-          new Bpl.IdentifierExpr(tok, mp.outParameterCopy), new Bpl.IdentifierExpr(tok, mp.localParameter)));

-      }

-      #endregion

-

       if (returnStatement.Expression != null) {

         ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this);

         etrav.Visit(returnStatement.Expression);