diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2012-01-03 16:20:30 -0800 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2012-01-03 16:20:30 -0800 |
| commit | 8ea7e9e82fef906f1a4727c48a292b8f93e51760 (patch) | |
| tree | 81c826ae601a43d936b232c43e3b7ae0b54f79d2 /BCT/BytecodeTranslator | |
| parent | 20189b94a9a13e186c07e92435d332b17ec4280c (diff) | |
For now, just ignore "address of" nodes and translate the expression of which
the address is being taken.
Diffstat (limited to 'BCT/BytecodeTranslator')
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 59b5d39f..46167ec2 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -337,12 +337,15 @@ namespace BytecodeTranslator }
} else {
this.Traverse(addressOf.Expression);
- var e = this.TranslatedExpressions.Pop();
-
- Bpl.Variable a = this.sink.CreateFreshLocal(addressOf.Type);
- this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
- this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(Bpl.Token.NoToken, Bpl.Expr.Ident(a), Bpl.Expr.Ident(this.sink.Heap.BoxField), e, AccessType.Heap, boogieT));
- this.TranslatedExpressions.Push(Bpl.Expr.Ident(a));
+ return;
+ // TODO: Sometimes the value must still be boxed: for anythign that is not going to be represented as a Ref in Boogie!
+ //this.Traverse(addressOf.Expression);
+ //var e = this.TranslatedExpressions.Pop();
+
+ //Bpl.Variable a = this.sink.CreateFreshLocal(addressOf.Type);
+ //this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
+ //this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(Bpl.Token.NoToken, Bpl.Expr.Ident(a), Bpl.Expr.Ident(this.sink.Heap.BoxField), e, AccessType.Heap, boogieT));
+ //this.TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
}
|