From 46da1f05e9122830d6c107bed4fc16f21f7a54aa Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 8 May 2018 21:51:42 +0200 Subject: [PATCH] When checking if we can influence a value we should not consider the overflow constraint as this will lead to false positives with ++ operations --- mythril/analysis/modules/integer.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 51e28f22..c34d3c4e 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -111,11 +111,11 @@ def _verify_integer_overflow(statespace, node, expr, state, model, constraint, o if type(op0) is not int: op0_value = int(str(model.eval(op0, model_completion=True))) - model0 = _try_constraints(node.constraints, [constraint, op0 != op0_value]) + model0 = _try_constraints(node.constraints, [op0 != op0_value]) if type(op1) is not int: op1_value = int(str(model.eval(op1, model_completion=True))) - model1 = _try_constraints(node.constraints, [constraint, op1 != op1_value]) + model1 = _try_constraints(node.constraints, [op1 != op1_value]) if model0 is None and model1 is None: return False