def _infer_arithmetic(left_type, right_type, op, lineno, solver):
"""Infer the type of an arithmetic operation, and add the corresponding axioms"""
result_type = solver.new_z3_const("arithmetic_result")
magic_method = ""
if isinstance(op, ast.Sub):
magic_method = "__sub__"
elif isinstance(op, ast.FloorDiv):
magic_method = "__floordiv__"
elif isinstance(op, ast.Mod):
magic_method = "__mod__"
elif isinstance(op, ast.LShift):
magic_method = "__lshift__"
elif isinstance(op, ast.RShift):
magic_method = "__rshift__"
solver.add(axioms.arithmetic(left_type, right_type, result_type, magic_method,
isinstance(op, ast.Mod), solver.z3_types),
fail_message="Arithmetic operation in line {}".format(lineno))
return result_type
评论列表
文章目录