summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/DoomErrorHandler.cs
blob: b082124062918e5882c0d4bcf671a8316eebd360 (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
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>();

        [ContractInvariantMethod]
        void ObjectInvariant()
        {
            Contract.Invariant(label2Absy != null);
            Contract.Invariant(callback != null);
            Contract.Invariant(cce.NonNullElements(m_CurrentTrace));
        }


        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 List<Block>/*!>!*/ TraceNodes
        {
            get
            {
                Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

                return m_CurrentTrace;
            }
        }

        public override void OnModel(IList<string>/*!>!*/ labels, Model model)
        {
            // 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);
        }

    }

}