blob: ce14ff73f9b4b33741a19d977e270276ef96c4ad (
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
|
using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
namespace VC
{
internal class DoomErrorHandler : ProverInterface.ErrorHandler
{
protected Dictionary<int, Absy> label2Absy;
protected VerifierCallback callback;
private List<Block> m_CurrentTrace = new List<Block>();
[ContractInvariantMethod]
void ObjectInvariant()
{
Contract.Invariant(label2Absy != null);
Contract.Invariant(callback != null);
Contract.Invariant(cce.NonNullElements(m_CurrentTrace));
}
public DoomErrorHandler(Dictionary<int, Absy> 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 List<Block>/*!>!*/ TraceNodes
{
get
{
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
return m_CurrentTrace;
}
}
public override void OnModel(IList<string>/*!>!*/ labels, Model model, ProverInterface.Outcome proverOutcome)
{
// TODO: it would be better to check which reachability variables are actually set to one!
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);
}
}
m_CurrentTrace.AddRange(traceNodes);
}
}
}
|
