diff options
author | 2011-12-28 19:42:08 -0800 | |
---|---|---|
committer | 2011-12-28 19:42:08 -0800 | |
commit | cc80320df0b652f25ffbd68a004b56c2ef34d981 (patch) | |
tree | dd778ae761f1e43e0b4c712040f1f6481c25c3b6 /BCT | |
parent | 3b28d9a89c618ff5a479a2e46a459d7a8b8b20ac (diff) | |
parent | b9f50d07fabfbbf4ae2684781178598d146e11ef (diff) |
Merge
Diffstat (limited to 'BCT')
-rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 5 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 17 |
2 files changed, 21 insertions, 1 deletions
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 9a48f1f0..eaef7e40 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -66,6 +66,9 @@ namespace BytecodeTranslator { [OptionDescription("File containing white/black list (optionally end file name with + for white list, - for black list, default is white list", ShortForm = "exempt")]
public string exemptionFile = "";
+ [OptionDescription("Instrument branches with unique counter values", ShortForm = "ib")]
+ public bool instrumentBranches = false;
+
}
public class BCT {
@@ -248,7 +251,7 @@ namespace BytecodeTranslator { }
var m2 = Decompiler.GetCodeModelFromMetadataModel(host, m, pdbReader) as IModule;
// The decompiler does not turn calls to Assert/Assume into Code Model nodes
- m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(m2);
+ m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(m2);
decompiledModules.Add(m2);
host.RegisterAsLatest(m2);
contractExtractors.Add(m2, host.GetContractExtractor(m2.UnitIdentity));
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 424064ff..43441642 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -198,6 +198,17 @@ namespace BytecodeTranslator StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
+
+ if (this.sink.Options.instrumentBranches) {
+ var tok = conditionalStatement.Token();
+ thenTraverser.StmtBuilder.Add(
+ new Bpl.AssumeCmd(tok, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.NextUniqueNumber()) }, null))
+ );
+ elseTraverser.StmtBuilder.Add(
+ new Bpl.AssumeCmd(tok, Bpl.Expr.True, new Bpl.QKeyValue(Bpl.Token.NoToken, "breadcrumb", new List<object> { Bpl.Expr.Literal(this.NextUniqueNumber()) }, null))
+ );
+ }
+
condTraverser.Traverse(conditionalStatement.Condition);
thenTraverser.Traverse(conditionalStatement.TrueBranch);
elseTraverser.Traverse(conditionalStatement.FalseBranch);
@@ -225,6 +236,12 @@ namespace BytecodeTranslator }
+ private static int counter = 0;
+ internal int NextUniqueNumber() {
+ return counter++;
+ }
+
+
/// <summary>
///
/// </summary>
|