runner.py 文件源码

def _actual_result(self, result, line):
        actual = None
        distance = inf
        if line == -inf:    # precondition
            actual = result.get_node_result(self.cfg.in_node)[0]
            return actual
        elif line == inf:   # postcondition
            actual = result.get_node_result(self.cfg.out_node)[0]
            return actual
        elif line < 0:
            for edge in self.cfg.edges.values():
                if isinstance(edge, Conditional):
                    current = edge.condition.pp.line + line
                    if current < distance:
                        states = result.get_node_result(edge.source)
                        actual = states[0]
                        distance = current
        for node in self.cfg.nodes.values():
            states = result.get_node_result(node)
            for i, stmt in enumerate(node.stmts):
                current = stmt.pp.line - line
                if abs(current) < distance:
                    actual = states[i+1] if current < 0 else states[i]
                    distance = abs(current)
        return actual