Fixed field update and field dereference.

3 files changed, 25 insertions, 13 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 20dd5d2e..f6998862 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -289,9 +289,8 @@ namespace BytecodeTranslator {
       if (buildSelectExpr) {

         List<Bpl.Expr> elist = new List<Bpl.Expr>();

 

-        while (TranslatedExpressions.Count > 0) {

-          elist.Add(TranslatedExpressions.Pop());

-        }

+        elist.Add(TranslatedExpressions.Pop());

+        elist.Add(TranslatedExpressions.Pop());

         TranslatedExpressions.Push(Bpl.Expr.Select(new Bpl.IdentifierExpr(field.Token(), HeapVariable), elist));

       }

     }

@@ -403,14 +402,24 @@ namespace BytecodeTranslator {
 

       this.Visit(assignment.Target);

 

-      Bpl.Expr targetexp = this.TranslatedExpressions.Pop();

-      Bpl.IdentifierExpr idexp = targetexp as Bpl.IdentifierExpr;

-      if (idexp != null) {

-        StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(assignment.Token(),

-          idexp, sourceexp));

-        return;

+      if (this.TranslatedExpressions.Count == 1) { // I think this is defintely the wrong test. there might be other stuff on the stack if the assignment is not a top-level statement!

+        Bpl.Expr targetexp = this.TranslatedExpressions.Pop();

+        Bpl.IdentifierExpr idexp = targetexp as Bpl.IdentifierExpr;

+        if (idexp != null) {

+          StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(assignment.Token(),

+            idexp, sourceexp));

+          return;

+        } else {

+          throw new TranslationException("Trying to create a SimpleAssign with complex/illegal lefthand side");

+        }

       } else {

-        throw new TranslationException("Trying to create a SimpleAssign with complex/illegal lefthand side");

+        // Assume it is always 2? What should we check?

+        Bpl.ExprSeq args = new Bpl.ExprSeq();

+        args.Add(this.TranslatedExpressions.Pop());

+        args.Add(this.TranslatedExpressions.Pop());

+        StmtTraverser.StmtBuilder.Add(

+          Bpl.Cmd.MapAssign(assignment.Token(),

+          new Bpl.IdentifierExpr(assignment.Token(), this.HeapVariable), args, sourceexp));

       }

 

     }

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index c24f6df9..7f6d95b7 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -91,7 +91,7 @@ namespace BytecodeTranslator {
         int in_count = 0;

         int out_count = 0;

         MethodParameter mp;

-        foreach (IParameterDefinition formal in method.ResolvedMethod.Parameters) {

+        foreach (IParameterDefinition formal in method.Parameters) {

 

           mp = new MethodParameter(formal);

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

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 756f127f..d421c573 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -40,7 +40,7 @@ namespace BytecodeTranslator {
 

       this.underlyingParameter = parameterDefinition;

 

-      Bpl.Type ptype = Bpl.Type.Int;

+      Bpl.Type ptype = TranslationHelper.CciTypeToBoogie(parameterDefinition.Type);

 

       var parameterToken = parameterDefinition.Token();

       var typeToken = parameterDefinition.Type.Token();

@@ -86,7 +86,10 @@ namespace BytecodeTranslator {
     #region Temp Stuff that must be replaced as soon as there is real code to deal with this

 

     public static Bpl.Type CciTypeToBoogie(ITypeReference type) {

-      return Bpl.Type.Int;

+      if (TypeHelper.IsPrimitiveInteger(type))

+        return Bpl.Type.Int;

+      else

+        return Bpl.Type.Int; // BUG! This is where we need to return "ref" for a reference type

     }

 

     public static Bpl.Variable TempHeapVar() {