summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Akash Lal <akashl@microsoft.com>2015-05-25 18:24:58 +0530
committerGravatar Akash Lal <akashl@microsoft.com>2015-05-25 18:24:58 +0530
commit7971dd771c21090edf5d9bc8a3c3766daed529e0 (patch)
treea141e2de3cd126437957ee231a73867f2eecefb4
parent846dd8fd2c345e20e3d85d4a07d73ddfab5ac45c (diff)
Allow for extra instrumentation on program before vc gen
-rw-r--r--Source/VCGeneration/StratifiedVC.cs14
1 files changed, 10 insertions, 4 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 69b7c8cc..43b5f88a 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -365,13 +365,16 @@ namespace VC {
public Dictionary<Block, List<CallSite>> callSites;
public Dictionary<Block, List<CallSite>> recordProcCallSites;
public bool initialized { get; private set; }
+ // Instrumentation to apply after PassiveImpl, but before VCGen
+ Action<Implementation> PassiveImplInstrumentation;
// boolControlVC (block -> its Bool variable)
public Dictionary<Block, VCExprVar> blockToControlVar;
- public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen) {
+ public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen, Action<Implementation> PassiveImplInstrumentation) {
vcgen = stratifiedVcGen;
impl = implementation;
+ this.PassiveImplInstrumentation = PassiveImplInstrumentation;
List<Variable> functionInterfaceVars = new List<Variable>();
foreach (Variable v in vcgen.program.GlobalVariables) {
@@ -581,6 +584,9 @@ namespace VC {
vcgen.ConvertCFG2DAG(impl);
vcgen.PassifyImpl(impl, out mvInfo);
+ if (PassiveImplInstrumentation != null)
+ PassiveImplInstrumentation(impl);
+
VCExpressionGenerator gen = proverInterface.VCExprGen;
var exprGen = proverInterface.Context.ExprGen;
var translator = proverInterface.Context.BoogieExprTranslator;
@@ -636,12 +642,12 @@ namespace VC {
public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
public ProverInterface prover;
- public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers, Action<Implementation> PassiveImplInstrumentation)
: base(program, logFilePath, appendLogFile, checkers) {
implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();
prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
foreach (var impl in program.Implementations) {
- implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);
+ implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this, PassiveImplInstrumentation);
}
GenerateRecordFunctions();
}
@@ -847,7 +853,7 @@ namespace VC {
}
public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
- : base(program, logFilePath, appendLogFile, checkers) {
+ : base(program, logFilePath, appendLogFile, checkers, null) {
PersistCallTree = false;
procsThatReachedRecBound = new HashSet<string>();
procsToSkip = new HashSet<string>();