stmt_inferrer.py 文件源码

def _infer_try(node, context, solver):
    """Infer the types for a try/except/else block"""
    result_type = solver.new_z3_const("try")

    body_type = _infer_body(node.body, context, node.lineno, solver)
    else_type = _infer_body(node.orelse, context, node.lineno, solver)
    final_type = _infer_body(node.finalbody, context, node.lineno, solver)

    solver.add(axioms.try_except(body_type, else_type, final_type, result_type, solver.z3_types),
               fail_message="Try/Except block in line {}".format(node.lineno))
    solver.optimize.add_soft(result_type == body_type)
    solver.optimize.add_soft(result_type == else_type)
    solver.optimize.add_soft(result_type == final_type)

    # TODO: Infer exception handlers as classes

    for handler in node.handlers:
        handler_context = context
        if handler.name:
            handler_context = Context(node.body, solver, parent_context=context)
            handler_context.set_type(handler.name,
                                     solver.annotation_resolver.resolve(handler.type, solver))
        handler_body_type = _infer_body(handler.body, handler_context, handler.lineno, solver)
        solver.add(solver.z3_types.subtype(handler_body_type, result_type),
                   fail_message="Exception handler in line {}".format(handler.lineno))

    return result_type