diff options
| author |  schaef <unknown> | 2009-12-18 13:41:32 +0000 |
|---|---|---|
| committer | schaef <unknown> | 2009-12-18 13:41:32 +0000 |
| commit | d5f09caee2ca7395d0a3dae6c29d7d10a6bc1de9 (patch) | |
| tree | ca6bc4de686a6e14cc32971483a1e675ef7c5315 /Source/VCGeneration/DoomErrorHandler.ssc | |
| parent | 9447617aefbe9706b0d74a827181976e4b9e9d26 (diff) | |
Doomed checking now uses the counterexample trace to minimize the number of theorem prover calls (See useCE in notdoomed.bpl).
Diffstat (limited to 'Source/VCGeneration/DoomErrorHandler.ssc')
| -rw-r--r-- | Source/VCGeneration/DoomErrorHandler.ssc | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/Source/VCGeneration/DoomErrorHandler.ssc b/Source/VCGeneration/DoomErrorHandler.ssc index 08bc2217..860f5334 100644 --- a/Source/VCGeneration/DoomErrorHandler.ssc +++ b/Source/VCGeneration/DoomErrorHandler.ssc @@ -41,6 +41,53 @@ namespace VC m_DoomedBlocks = doomedblocks;
m_TraceBlocks = traceblocks;
}
+
+ private List<Block!>! m_CurrentTrace = new List<Block!>();
+
+ public List<Block!>! TraceNodes
+ {
+ get
+ {
+ return m_CurrentTrace;
+ }
+ }
+
+ public override void OnModel(IList<string!>! labels, ErrorModel errModel) {
+ m_CurrentTrace.Clear();
+ //Console.Write("Used Blocks: ");
+ List<Block!> traceNodes = new List<Block!>();
+ List<AssertCmd!> assertNodes = new List<AssertCmd!>();
+ foreach (string! s in labels) {
+ Absy node = Label2Absy(s);
+ if (node is Block) {
+ Block b = (Block)node;
+ traceNodes.Add(b);
+ //Console.Write("{0}, ", b.Label);
+ } else {
+ AssertCmd a = (AssertCmd)node;
+ assertNodes.Add(a);
+ }
+ }
+ m_CurrentTrace.AddRange(traceNodes);
+ //Console.WriteLine();
+// assert assertNodes.Count > 0;
+// assert traceNodes.Count == assertNodes.Count;
+//
+// foreach (AssertCmd a in assertNodes) {
+// // find the corresponding Block (assertNodes.Count is likely to be 1, or small in any case, so just do a linear search here)
+// foreach (Block b in traceNodes) {
+// if (b.Cmds.Has(a)) {
+// BlockSeq trace = new BlockSeq();
+// trace.Add(b);
+// goto NEXT_ASSERT;
+// }
+// }
+// assert false; // there was no block that contains the assert
+// NEXT_ASSERT: {}
+// }
+
+ }
+
}
}
\ No newline at end of file |