diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-06-23 10:05:51 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-06-23 10:05:51 -0700 |
| commit | 1bd25853970d7c3abfed38f72904d8eac8ae50d7 (patch) | |
| tree | 1a48bd4aaef9125ef3411c5721a27a3eb292ec00 | |
| parent | 2b81b9d7e787409913f4c0488c0b3310a4e9e5a0 (diff) | |
bug fix in translation of dispatch continuation
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 1 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 1298d4e1..c187444f 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -356,6 +356,7 @@ namespace BytecodeTranslator { this.privateTypes.AddRange(helperTypes);
}
//method.Body.Dispatch(stmtTraverser);
+ stmtTraverser.StmtBuilder.Add(new Bpl.ReturnCmd(Bpl.Token.NoToken));
stmtTraverser.GenerateDispatchContinuation();
#endregion
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 31771f9c..b0821dcd 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -95,7 +95,7 @@ namespace BytecodeTranslator }
public void GenerateDispatchContinuation() {
- // Iterate over all labels in sink.cciLabels and sink.boogieLabels and generate dispatch based on sink.LabelVariable
+ // Iterate over all labels in sink.cciLabels and generate dispatch based on sink.LabelVariable
this.StmtBuilder.AddLabelCmd("DispatchContinuation");
Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(true), TranslationHelper.BuildStmtList(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false))), null, null);
Bpl.IdentifierExpr labelExpr = Bpl.Expr.Ident(this.sink.LabelVariable);
|