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, 21 insertions, 0 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 041998fa..108c0fd1 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -96,6 +96,15 @@ namespace BytecodeTranslator {
     }

 

     public override void Visit(IAddressDereference addressDereference) {

+      IBoundExpression be = addressDereference.Address as IBoundExpression;

+      if (be != null) {

+        IParameterDefinition pd = be.Definition as IParameterDefinition;

+        if (pd != null) {

+          var pv = this.sink.FindParameterVariable(pd);

+          TranslatedExpressions.Push(Bpl.Expr.Ident(pv));

+          return;

+        }

+      }

       this.Visit(addressDereference.Address);

       throw new NotImplementedException();

     }

@@ -123,6 +132,18 @@ namespace BytecodeTranslator {
           this.Visit(addressOf.Expression);

           return;

         }

+        IConversion/*?*/ conversion = deref.Address as IConversion;

+        if (conversion != null) {

+          IBoundExpression be = conversion.ValueToConvert as IBoundExpression;

+          if (be != null) {

+            IParameterDefinition pd = be.Definition as IParameterDefinition;

+            if (pd != null) {

+              var pv = this.sink.FindParameterVariable(pd);

+              TranslatedExpressions.Push(Bpl.Expr.Ident(pv));

+              return;

+            }

+          }

+        }

         if (targetExpression.Instance != null) {

           // TODO

           throw new NotImplementedException("targetExpr->AddrDeRef->InstanceNull");