blob: f31b597ec36199b8639590515ea723ad7f1b8ba9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
using Graphing;
using AI = Microsoft.AbstractInterpretationFramework;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
namespace VC
{
internal class DoomErrorHandler : ProverInterface.ErrorHandler {
protected Hashtable label2Absy;
protected VerifierCallback callback;
private List<Block> m_CurrentTrace = new List<Block>();
public Variable m_Reachvar;
public List<Block> m_DoomedBlocks, m_TraceBlocks;
[ContractInvariantMethod]
void ObjectInvariant()
{
Contract.Invariant(label2Absy!=null);
Contract.Invariant(callback != null);
Contract.Invariant(cce.NonNullElements(m_CurrentTrace));
Contract.Invariant(m_Reachvar != null);
Contract.Invariant(m_DoomedBlocks != null);
Contract.Invariant(m_TraceBlocks != null);
}
public DoomErrorHandler(Hashtable label2Absy, VerifierCallback callback) {
Contract.Requires(label2Absy != null);
Contract.Requires(callback != null);
this.label2Absy = label2Absy;
this.callback = callback;
}
public override Absy Label2Absy(string label) {
Contract.Requires(label != null);
Contract.Ensures(Contract.Result<Absy>() != null);
int id = int.Parse(label);
return cce.NonNull((Absy) label2Absy[id]);
}
public override void OnProverWarning(string msg) {
Contract.Requires(msg != null);
this.callback.OnWarning(msg);
}
public void OnDoom(Variable reachvar, List<Block>/*!>!*/ doomedblocks, List<Block>/*!>!*/ traceblocks) {
Contract.Requires(reachvar != null);
Contract.Requires(cce.NonNullElements(doomedblocks));
Contract.Requires(cce.NonNullElements(traceblocks));
m_Reachvar = reachvar;
m_DoomedBlocks = doomedblocks;
m_TraceBlocks = traceblocks;
}
public List<Block>/*!>!*/ TraceNodes
{
get
{
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
return m_CurrentTrace;
}
}
public override void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel) {
Contract.Requires(labels != null);
m_CurrentTrace.Clear();
//Console.Write("Used Blocks: ");
List<Block> traceNodes = new List<Block>();
List<AssertCmd> assertNodes = new List<AssertCmd>();
foreach (string s in labels) {
Contract.Assert(s != null);
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: {}
// }
}
}
}
|
