Method visit_vertex

src/analysis/mir_visitor/body_visitor.rs:662–675

Visit a node in w.t.o

(&mut self, vertex: &WtoVertex)

{
    /// Visit a node in w.t.o
    fn visit_vertex(&mut self, vertex: &WtoVertex) {
        let bb = vertex.node();
        // If bb is the entry block (block ID is 0), initialize precondition as init state
        let pre = if vertex.is_entry() {
            self.init_state.clone()
        } else {
            // Otherwise, compute the disjunction of all the predecessors' post conditions
            self.get_state_from_predecessors(bb)
        };
        // self.set_pre(bb, pre.clone());

        // Now analyze this node
        self.analyze_basic_block(bb, pre);
    }

    /// Visit a circle in w.t.o, the analysis will only proceed if the circle reaches its fixed-point
    fn visit_circle(&mut self, circle: &WtoCircle) {