expr_inferrer.py 文件源码

def infer_unary_operation(node, context, solver):
    """Infer the type for unary operations

    Examples: -5, not 1, ~2
    """
    unary_type = infer(node.operand, context, solver)
    if isinstance(node.op, ast.Not):  # (not expr) always gives bool type
        return solver.z3_types.bool

    if isinstance(node.op, ast.Invert):
        solver.add(axioms.unary_invert(unary_type, solver.z3_types),
                   fail_message="Invert operation in line {}".format(node.lineno))
        return solver.z3_types.int
    else:
        result_type = solver.new_z3_const("unary_result")
        solver.add(axioms.unary_other(unary_type, result_type, solver.z3_types),
                   fail_message="Unary operation in line {}".format(node.lineno))
        return result_type