Fixed struct copy constructor implementation.

3 files changed, 25 insertions, 6 deletions

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 72b4d1df..eb8f96e1 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -275,6 +275,8 @@ namespace BytecodeTranslator {
         new Bpl.AssumeCmd(tok, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, this.sink.Heap.DynamicType(o), this.sink.FindOrCreateTypeReference(typeDefinition, true)))

         );

 

+      var localVars = new Bpl.VariableSeq();

+

       foreach (var f in typeDefinition.Fields) {

         if (f.IsStatic) continue;

 

@@ -285,8 +287,13 @@ namespace BytecodeTranslator {
           // generate a call to the copy constructor to copy the contents of f

           var proc2 = this.sink.FindOrCreateProcedureForStructCopy(f.Type);

           var e = this.sink.Heap.ReadHeap(Bpl.Expr.Ident(proc.InParams[0]), fExp, AccessType.Struct, boogieType);

-          var cmd = new Bpl.CallCmd(tok, proc2.Name, new List<Bpl.Expr> { e, }, new List<Bpl.IdentifierExpr>{ o, });

+          var bplLocal = this.sink.CreateFreshLocal(f.Type);

+          var localExpr = Bpl.Expr.Ident(bplLocal);

+          localVars.Add(bplLocal);

+          var cmd = new Bpl.CallCmd(tok, proc2.Name, new List<Bpl.Expr> { e, }, new List<Bpl.IdentifierExpr>{ localExpr, });

           stmtBuilder.Add(cmd);

+          var c = this.sink.Heap.WriteHeap(tok, o, fExp, localExpr, AccessType.Struct, boogieType);

+          stmtBuilder.Add(c);

         } else {

           // just generate a normal assignment to the field f

           var e = this.sink.Heap.ReadHeap(Bpl.Expr.Ident(proc.InParams[0]), fExp, AccessType.Struct, boogieType);

@@ -305,7 +312,7 @@ namespace BytecodeTranslator {
         new Bpl.TypeVariableSeq(),

         proc.InParams,

         proc.OutParams,

-        new Bpl.VariableSeq(),

+        localVars,

         stmtBuilder.Collect(Bpl.Token.NoToken),

         attrib,

         new Bpl.Errors()

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index ddcb2c07..5217df14 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -197,10 +197,11 @@ namespace BytecodeTranslator {
         var fileName = assemblyNames[0];

         fileName = Path.GetFileNameWithoutExtension(fileName);

         string outputFileName = fileName + ".bpl";

-        Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);

-        Prelude.Emit(writer);

-        pgm.Emit(writer);

-        writer.Close();

+        using (var writer = new Microsoft.Boogie.TokenTextWriter(outputFileName)) {

+          Prelude.Emit(writer);

+          pgm.Emit(writer);

+          writer.Close();

+        }

         return 0; // success

       } catch (Exception e) { // swallow everything and just return an error code

         Console.WriteLine("The byte-code translator failed: {0}", e.Message);

diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
index 6dfccde6..51a4ba86 100644
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -198,4 +198,15 @@ namespace RegressionTestInput {
     public int x;

   }

 

+  public struct StructContainingStruct {

+    public double d;

+    public S s;

+

+    public StructContainingStruct ReturnCopy(StructContainingStruct s) {

+      StructContainingStruct t = s;

+      return t;

+    }

+

+  }

+

 }