1 files changed, 37 insertions, 0 deletions
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index f65c4732..5c78298b 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -85,6 +85,7 @@ namespace BytecodeTranslator {
       } else if (typeDefinition.IsStruct) {
         sink.FindOrCreateType(typeDefinition);
         CreateDefaultStructConstructor(typeDefinition);
+        CreateStructCopyConstructor(typeDefinition);
         base.Visit(typeDefinition);
       } else {
         Console.WriteLine("Unknown kind of type definition '{0}' was found",
@@ -133,6 +134,42 @@ namespace BytecodeTranslator {
       impl.Proc = (Bpl.Procedure) proc; // TODO: get rid of cast
       this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
     }
+    
+    private void CreateStructCopyConstructor(ITypeDefinition typeDefinition) {
+      Contract.Requires(typeDefinition.IsStruct);
+
+      var proc = this.sink.FindOrCreateProcedureForStructCopy(typeDefinition);
+
+      var stmtBuilder = new Bpl.StmtListBuilder();
+
+      foreach (var f in typeDefinition.Fields) {
+        var boogieType = sink.CciTypeToBoogie(f.Type);
+        var fExp = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(f));
+        var e = this.sink.Heap.ReadHeap(Bpl.Expr.Ident(proc.InParams[0]), fExp, AccessType.Struct, boogieType);
+        var o = Bpl.Expr.Ident(proc.InParams[1]);
+        var c = this.sink.Heap.WriteHeap(Bpl.Token.NoToken, o, fExp, e, AccessType.Struct, boogieType);
+        stmtBuilder.Add(c);
+      }
+
+      var lit = Bpl.Expr.Literal(1);
+      lit.Type = Bpl.Type.Int;
+      var args = new List<object> { lit };
+      var attrib = new Bpl.QKeyValue(typeDefinition.Token(), "inline", args, null); // TODO: Need to have it be {:inine 1} (and not just {:inline})?
+      Bpl.Implementation impl =
+        new Bpl.Implementation(Bpl.Token.NoToken,
+        proc.Name,
+        new Bpl.TypeVariableSeq(),
+        proc.InParams,
+        proc.OutParams,
+        new Bpl.VariableSeq(),
+        stmtBuilder.Collect(Bpl.Token.NoToken),
+        attrib,
+        new Bpl.Errors()
+        );
+
+      impl.Proc = (Bpl.Procedure)proc; // TODO: get rid of cast
+      this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
+    }
 
     private bool sawCctor = false;