diff options
author | 2010-04-19 23:03:19 +0000 | |
---|---|---|
committer | 2010-04-19 23:03:19 +0000 | |
commit | b51c9db20a47aa974d44fbbc8b2b4671b1049bb7 (patch) | |
tree | 8c486a29f2b840c7e385751e16e24de7e3bae8e0 | |
parent | e6e2ac05b16701ed0f033b468b00a1b026c49f74 (diff) |
Fixed bug in interprocedural counterexample generation
-rw-r--r-- | Source/VCGeneration/VC.ssc | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index faa9e55b..5debbfc3 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -1593,7 +1593,7 @@ namespace VC assert traceNodes.Contains(entryBlock);
trace.Add(entryBlock);
- Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program);
+ Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<Absy!, Counterexample!>());
if (newCounterexample == null) return;
@@ -2141,9 +2141,8 @@ namespace VC return null;
}
- static Counterexample TraceCounterexample(Block! b, Hashtable! traceNodes, BlockSeq! trace, ErrorModel errModel, Dictionary<Incarnation, Absy!>! incarnationOriginMap, Dictionary<string!, LazyInliningInfo!>! implName2LazyInliningInfo, DeclFreeProverContext! context, Program! program)
+ static Counterexample TraceCounterexample(Block! b, Hashtable! traceNodes, BlockSeq! trace, ErrorModel errModel, Dictionary<Incarnation, Absy!>! incarnationOriginMap, Dictionary<string!, LazyInliningInfo!>! implName2LazyInliningInfo, DeclFreeProverContext! context, Program! program, Dictionary<Absy!, Counterexample!>! calleeCounterexamples)
{
- Dictionary<Absy!, Counterexample!> calleeCounterexamples = new Dictionary<Absy!, Counterexample!>();
// After translation, all potential errors come from asserts.
CmdSeq! cmds = b.Cmds;
TransferCmd! transferCmd = (!)b.TransferCmd;
@@ -2197,7 +2196,7 @@ namespace VC {
if (traceNodes.Contains(bb)){
trace.Add(bb);
- return TraceCounterexample(bb, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program);
+ return TraceCounterexample(bb, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program, calleeCounterexamples);
}
}
}
|