first cut at handling generics

6 files changed, 144 insertions, 165 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 7dbf8d0f..29c0033f 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -424,18 +424,18 @@ namespace BytecodeTranslator
     /// </summary>

     /// <param name="methodCall"></param>

     /// <remarks>Stub, This one really needs comments!</remarks>

-    public override void Visit(IMethodCall methodCall)

-    {

-      var resolvedMethod = methodCall.MethodToCall.ResolvedMethod;

+    public override void Visit(IMethodCall methodCall) {

+      var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;

+

       if (resolvedMethod == Dummy.Method) {

         throw new TranslationException(

           ExceptionType.UnresolvedMethod,

           MemberHelper.GetMethodSignature(methodCall.MethodToCall, NameFormattingOptions.None));

       }

-        

-      #region Translate In Parameters

 

+      #region Translate In and Out Parameters

       var inexpr = new List<Bpl.Expr>();

+      var outvars = new List<Bpl.IdentifierExpr>();

 

       #region Create the 'this' argument for the function call

       Bpl.IdentifierExpr thisExpr = null;

@@ -443,8 +443,7 @@ namespace BytecodeTranslator
       List<IFieldDefinition> args = null;

       Bpl.Expr arrayExpr = null;

       Bpl.Expr indexExpr = null;

-      if (!methodCall.IsStaticCall)

-      {

+      if (!methodCall.IsStaticCall) {

         this.collectStructFields = true;

         this.structFields = new List<IFieldDefinition>();

         this.arrayExpr = null;

@@ -456,175 +455,145 @@ namespace BytecodeTranslator
         indexExpr = this.indexExpr;

 

         var e = this.TranslatedExpressions.Pop();

-        if (false && methodCall.MethodToCall.ContainingType.IsValueType)

-        {

-          // then the "this arg" was actually an AddressOf the struct

-          // but we are going to ignore that and just get the identifier

-          // that it was the address of

-          var nAry = e as Bpl.NAryExpr;

-          var nAryArgs = nAry.Args;

-          e = nAryArgs[0] as Bpl.IdentifierExpr;

-        }

         inexpr.Add(e);

-        if (e is Bpl.NAryExpr)

-        {

+        if (e is Bpl.NAryExpr) {

           e = ((Bpl.NAryExpr)e).Args[0];

         }

         thisExpr = e as Bpl.IdentifierExpr;

         locals = new List<Bpl.Variable>();

         Bpl.Variable x = thisExpr.Decl;

         locals.Add(x);

-        for (int i = 0; i < args.Count; i++)

-        {

+        for (int i = 0; i < args.Count; i++) {

           Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(args[i]));

           Bpl.Variable y = this.sink.CreateFreshLocal(args[i].Type);

           StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(y), this.sink.Heap.ReadHeap(Bpl.Expr.Ident(x), g, args[i].ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, y.TypedIdent.Type)));

           x = y;

           locals.Add(y);

         }

-        //thisExpr = Bpl.Expr.Ident(x);

-        //inexpr.Add(thisExpr);

+      }

+      if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {

+        outvars.Add(thisExpr);

       }

       #endregion

 

-      Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();

+      Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed = new Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr>();

+      Dictionary<IParameterDefinition, Bpl.IdentifierExpr> p2eMap = new Dictionary<IParameterDefinition, Bpl.IdentifierExpr>();

       IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();

       penum.MoveNext();

-      foreach (IExpression exp in methodCall.Arguments)

-      {

-        if (penum.Current == null)

-        {

-          throw new TranslationException("More Arguments than Parameters in functioncall");

+      foreach (IExpression exp in methodCall.Arguments) {

+        if (penum.Current == null) {

+          throw new TranslationException("More arguments than parameters in method call");

         }

         this.Visit(exp);

         Bpl.Expr e = this.TranslatedExpressions.Pop();

-

-        p2eMap.Add(penum.Current, e);

-        if (!penum.Current.IsOut)

-        {

+        if (penum.Current.Type is IGenericTypeParameter)

+          inexpr.Add(sink.Heap.Box(methodCall.Token(), this.sink.CciTypeToBoogie(exp.Type), e));

+        else

           inexpr.Add(e);

+        if (penum.Current.IsByReference) {

+          Bpl.IdentifierExpr unboxed = e as Bpl.IdentifierExpr;

+          if (unboxed == null) {

+            throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");

+          }

+          if (penum.Current.Type is IGenericTypeParameter) {

+            Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));

+            toBoxed[unboxed] = boxed;

+            outvars.Add(boxed);

+          }

+          else {

+            outvars.Add(unboxed);

+          }

         }

-

         penum.MoveNext();

       }

       #endregion

 

       Bpl.IToken cloc = methodCall.Token();

-

-      // meeting a constructor is always something special

-      if (false && resolvedMethod.IsConstructor)

-      {

-        // Todo: do something with the constructor call

-      }

-      else

-      {

-        // Todo: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!

-

-        #region Translate Out vars

-        var outvars = new List<Bpl.IdentifierExpr>();

-        if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {

-          outvars.Add(thisExpr);

+      if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

+        Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);

+        Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(cloc, v);

+        if (resolvedMethod.Type is IGenericTypeParameter) {

+          Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));

+          toBoxed[unboxed] = boxed;

+          outvars.Add(boxed);

         }

-        foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap)

-        {

-          if (kvp.Key.IsOut || kvp.Key.IsByReference)

-          {

-            Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;

-            if (iexp == null)

-            {

-              throw new TranslationException("Trying to pass complex expression as out in functioncall");

-            }

-            outvars.Add(iexp);

-          }

+        else {

+          outvars.Add(unboxed);

         }

-        #endregion

+        TranslatedExpressions.Push(unboxed);

+      }

+      var proc = this.sink.FindOrCreateProcedure(resolvedMethod);

+      string methodname = proc.Name;

 

-        if (methodCall.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void)

-        {

-          Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);

-          outvars.Add(new Bpl.IdentifierExpr(cloc, v));

-          TranslatedExpressions.Push(new Bpl.IdentifierExpr(cloc, v));

+      Bpl.QKeyValue attrib = null;

+      foreach (var a in resolvedMethod.Attributes) {

+        if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {

+          attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);

         }

-        var proc = this.sink.FindOrCreateProcedure(resolvedMethod);

-        string methodname = proc.Name;

+      }

 

-        Bpl.QKeyValue attrib = null;

-        foreach (var a in resolvedMethod.Attributes)

-        {

-          if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute"))

-          {

-            attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);

-          }

+      Bpl.CallCmd call;

+      bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");

+      bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");

+      if (isEventAdd || isEventRemove) {

+        var mName = resolvedMethod.Name.Value;

+        var eventName = mName.Substring(mName.IndexOf('_') + 1);

+        var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));

+        Contract.Assert(eventDef != Dummy.Event);

+        Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);

+        Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);

+

+        if (methodCall.IsStaticCall) {

+          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));

+          inexpr.Insert(0, Bpl.Expr.Ident(local));

+        }

+        else {

+          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));

+          inexpr[0] = Bpl.Expr.Ident(local);

         }

 

-        Bpl.CallCmd call;

-        bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");

-        bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");

-        if (isEventAdd || isEventRemove)

-        {

-          var mName = resolvedMethod.Name.Value;

-          var eventName = mName.Substring(mName.IndexOf('_')+1);

-          var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));

-          Contract.Assert(eventDef != Dummy.Event);

-          Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);

-          Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);

-

-          if (methodCall.IsStaticCall)

-          {

-            this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));

-            inexpr.Insert(0, Bpl.Expr.Ident(local));

-          }

-          else 

-          {

-            this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));

-            inexpr[0] = Bpl.Expr.Ident(local);

-          }

-

-          System.Diagnostics.Debug.Assert(outvars.Count == 0);

-          outvars.Add(Bpl.Expr.Ident(local));

-          string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;

-          call = new Bpl.CallCmd(methodCall.Token(), methodName, inexpr, outvars);

-          this.StmtTraverser.StmtBuilder.Add(call);

-          if (methodCall.IsStaticCall)

-          {

-            this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));

-          }

-          else

-          {

-            this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));

-          }

+        System.Diagnostics.Debug.Assert(outvars.Count == 0);

+        outvars.Add(Bpl.Expr.Ident(local));

+        string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;

+        call = new Bpl.CallCmd(methodCall.Token(), methodName, inexpr, outvars);

+        this.StmtTraverser.StmtBuilder.Add(call);

+        if (methodCall.IsStaticCall) {

+          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));

         }

-        else

-        {

-          if (attrib != null)

-            call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);

-          else

-            call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);

-          this.StmtTraverser.StmtBuilder.Add(call);

+        else {

+          this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));

         }

+      }

+      else {

+        if (attrib != null)

+          call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);

+        else

+          call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);

+        this.StmtTraverser.StmtBuilder.Add(call);

+      }

 

-        if (!methodCall.IsStaticCall) {

-          Debug.Assert(args != null && locals != null);

-          int count = args.Count;

-          Bpl.Variable x = locals[count];

+      foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {

+        this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));

+      }

+

+      if (!methodCall.IsStaticCall) {

+        Debug.Assert(args != null && locals != null);

+        int count = args.Count;

+        Bpl.Variable x = locals[count];

+        count--;

+        while (0 <= count) {

+          IFieldDefinition currField = args[count];

+          Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(currField));

+          Bpl.Variable y = locals[count];

+          StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), Bpl.Expr.Ident(y), g, Bpl.Expr.Ident(x), currField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, x.TypedIdent.Type));

+          x = y;

           count--;

-          while (0 <= count)

-          {

-            IFieldDefinition currField = args[count];

-            Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(currField));

-            Bpl.Variable y = locals[count];

-            StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), Bpl.Expr.Ident(y), g, Bpl.Expr.Ident(x), currField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, x.TypedIdent.Type));

-            x = y;

-            count--;

-          }

-          if (indexExpr != null) {

-            Debug.Assert(arrayExpr != null);

-            StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, arrayExpr, indexExpr, Bpl.Expr.Ident(x), AccessType.Array, x.TypedIdent.Type));

-          }

         }

-

+        if (indexExpr != null) {

+          Debug.Assert(arrayExpr != null);

+          StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, arrayExpr, indexExpr, Bpl.Expr.Ident(x), AccessType.Array, x.TypedIdent.Type));

+        }

       }

-

     }

 

     #endregion

@@ -756,7 +725,7 @@ namespace BytecodeTranslator
     /// </summary>

     public override void Visit(ICreateObjectInstance createObjectInstance)

     {

-      TranslateObjectCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance.Type, createObjectInstance);

+      TranslateObjectCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance);

     }

 

     public override void Visit(ICreateArray createArrayInstance)

@@ -788,35 +757,32 @@ namespace BytecodeTranslator
       TranslatedExpressions.Push(Bpl.Expr.Ident(a));

     }

 

-    private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, ITypeReference ctorType, IExpression creationAST)

+    private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, IExpression creationAST)

     {

+      var resolvedMethod = Sink.Unspecialize(ctor).ResolvedMethod;

       Bpl.IToken token = creationAST.Token();

-

+      

       var a = this.sink.CreateFreshLocal(creationAST.Type);

 

       // First generate an Alloc() call

       this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));

 

       // Second, generate the call to the appropriate ctor

-      var proc = this.sink.FindOrCreateProcedure(ctor.ResolvedMethod);

+      var proc = this.sink.FindOrCreateProcedure(resolvedMethod);

       Bpl.ExprSeq inexpr = new Bpl.ExprSeq();

       inexpr.Add(Bpl.Expr.Ident(a));

-      IEnumerator<IParameterDefinition> penum = ctor.ResolvedMethod.Parameters.GetEnumerator();

+      IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();

       penum.MoveNext();

-      foreach (IExpression exp in arguments)

-      {

-        if (penum.Current == null)

-        {

+      foreach (IExpression exp in arguments) {

+        if (penum.Current == null) {

           throw new TranslationException("More Arguments than Parameters in functioncall");

         }

         this.Visit(exp);

         Bpl.Expr e = this.TranslatedExpressions.Pop();

-

-        if (!penum.Current.IsOut)

-        {

+        if (penum.Current.Type is IGenericTypeParameter)

+          inexpr.Add(sink.Heap.Box(ctor.Token(), this.sink.CciTypeToBoogie(exp.Type), e));

+        else

           inexpr.Add(e);

-        }

-

         penum.MoveNext();

       }

 

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 812fddb1..6d03ef9f 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -148,6 +148,9 @@ namespace BytecodeTranslator {
     [RepresentationFor("Real2Box", "function Real2Box(Real): Box;")]

     public Bpl.Function Real2Box = null;

 

+    [RepresentationFor("Box2Box", "function {:inline true} Box2Box(b: Box): Box { b }")]

+    public Bpl.Function Box2Box = null;

+

     public Bpl.Expr Box(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {

       Bpl.Function conversion;

       if (boogieType == Bpl.Type.Bool)

@@ -160,6 +163,8 @@ namespace BytecodeTranslator {
         conversion = this.Ref2Box;

       else if (boogieType == RealType)

         conversion = this.Real2Box;

+      else if (boogieType == BoxType)

+        conversion = this.Box2Box;

       else

         throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));

 

@@ -183,6 +188,8 @@ namespace BytecodeTranslator {
         conversion = this.Box2Ref;

       else if (boogieType == RealType)

         conversion = this.Box2Real;

+      else if (boogieType == BoxType)

+        conversion = this.Box2Box;

       else

         throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));

 

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 1fa59767..58bec27f 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -262,7 +262,7 @@ namespace BytecodeTranslator {
         #region Create Local Vars For Implementation

         List<Bpl.Variable> vars = new List<Bpl.Variable>();

         foreach (MethodParameter mparam in formalMap.Values) {

-          if (!(mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut))

+          if (!mparam.underlyingParameter.IsByReference)

             vars.Add(mparam.outParameterCopy);

         }

         foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 629e7e54..b8d8334d 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -99,6 +99,9 @@ namespace BytecodeTranslator {
         return Bpl.Expr.Ident(this.Heap.DefaultStruct);

       } else if (bplType == this.Heap.RefType) {

         return Bpl.Expr.Ident(this.Heap.NullRef);

+      }

+      else if (bplType == this.Heap.BoxType) {

+        return Bpl.Expr.Ident(this.Heap.DefaultBox);

       } else {

         throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(type)));

       }

@@ -113,9 +116,11 @@ namespace BytecodeTranslator {
         return heap.RealType;

       else if (type.ResolvedType.IsStruct)

         return heap.StructType;

-      else if (type.IsEnum) {

+      else if (type.IsEnum)

         return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer

-      } else

+      else if (type is IGenericTypeParameter) 

+        return heap.BoxType;

+      else

         return heap.RefType;

     }

 

@@ -134,6 +139,14 @@ namespace BytecodeTranslator {
       return v;

     }

 

+    public Bpl.Variable CreateFreshLocal(Bpl.Type t) {

+      Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location

+      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));

+      ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie

+      localVarMap.Add(dummy, v);

+      return v;

+    }

+

     /// <summary>

     /// State that gets re-initialized per method

     /// </summary>

@@ -335,10 +348,9 @@ namespace BytecodeTranslator {
         MethodParameter mp;

         var formalMap = new Dictionary<IParameterDefinition, MethodParameter>();

         foreach (IParameterDefinition formal in method.Parameters) {

-

           mp = new MethodParameter(formal, this.CciTypeToBoogie(formal.Type));

           if (mp.inParameterCopy != null) in_count++;

-          if (mp.outParameterCopy != null && (formal.IsByReference || formal.IsOut))

+          if (mp.outParameterCopy != null && formal.IsByReference)

             out_count++;

           formalMap.Add(formal, mp);

         }

@@ -397,7 +409,7 @@ namespace BytecodeTranslator {
             invars[i++] = mparam.inParameterCopy;

           }

           if (mparam.outParameterCopy != null) {

-            if (mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut)

+            if (mparam.underlyingParameter.IsByReference)

               outvars[j++] = mparam.outParameterCopy;

           }

         }

@@ -563,7 +575,7 @@ namespace BytecodeTranslator {
       this.FindOrCreateProcedure(method);

       return this.declaredMethods[method.InternedKey];

     }

-    private static IMethodReference Unspecialize(IMethodReference method) {

+    public static IMethodReference Unspecialize(IMethodReference method) {

       IMethodReference result = method;

       var gmir = result as IGenericMethodInstanceReference;

       if (gmir != null) {

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 42b1a4d0..54ed1700 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -37,22 +37,18 @@ namespace BytecodeTranslator {
     public IParameterDefinition underlyingParameter;

 

     public MethodParameter(IParameterDefinition parameterDefinition, Bpl.Type ptype) {

-

       this.underlyingParameter = parameterDefinition;

 

       var parameterToken = parameterDefinition.Token();

       var typeToken = parameterDefinition.Type.Token();

       var parameterName = parameterDefinition.Name.Value;

 

-      if (!parameterDefinition.IsOut) {

-        this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);

-      }

-      if (parameterDefinition.IsByReference || parameterDefinition.IsOut) {

+      this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);

+      if (parameterDefinition.IsByReference) {

         this.outParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$out", ptype), false);

       } else {

         this.outParameterCopy = new Bpl.LocalVariable(parameterToken, new Bpl.TypedIdent(typeToken, parameterName, ptype));

       }

-      

     }

 

     public override string ToString() {

diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index f4cc59af..92154020 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -149,13 +149,11 @@ namespace BytecodeTranslator {
 

         Bpl.IToken token = methodCall.Token();

 

-        // TODO: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!

-

         #region Translate Out vars

         var outvars = new List<Bpl.IdentifierExpr>();

 

         foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap) {

-          if (kvp.Key.IsOut || kvp.Key.IsByReference) {

+          if (kvp.Key.IsByReference) {

             Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;

             if (iexp == null) {

               throw new TranslationException("Trying to pass complex expression as out in functioncall");