diff options
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 11 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 9 | ||||
| -rw-r--r-- | BCT/RegressionTests/RegressionTestInput/Class1.cs | 11 |
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;
+ }
+
+ }
+
}
|