def _infer_bitwise(left_type, right_type, op, lineno, solver):
"""Infer the type of a bitwise operation, and add the corresponding axioms"""
result_type = solver.new_z3_const("bitwise_result")
magic_method = ""
if isinstance(op, ast.BitOr):
magic_method = "__or__"
elif isinstance(op, ast.BitXor):
magic_method = "__xor__"
elif isinstance(op, ast.BitAnd):
magic_method = "__and__"
solver.add(axioms.bitwise(left_type, right_type, result_type, magic_method, solver.z3_types),
fail_message="Bitwise operation in line {}".format(lineno))
return result_type
评论列表
文章目录