From 26a9871d333ebec3e9e295bd79b859d9efd41f4b Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 1 May 2018 19:33:31 +0200 Subject: [PATCH 1/2] Ignore requires checking --- mythril/analysis/modules/integer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 3163e0a1..e33687aa 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -274,7 +274,7 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth if len(element) < 1: continue if _check_requires(element[0], node, statespace, constraint): - continue + pass results += element # Recursively search children From f7b2bcead9695efb7d80caa1afb3418c47fe24d0 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 1 May 2018 19:45:06 +0200 Subject: [PATCH 2/2] Ignore reachability for now --- mythril/analysis/modules/integer.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index e33687aa..51e28f22 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -82,7 +82,7 @@ def _check_integer_overflow(statespace, state, node): logging.debug("[INTEGER_OVERFLOW] no model found") return issues - if not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1) : + if not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1): return issues # Build issue @@ -273,8 +273,8 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth element = _check_usage(current_state, expression) if len(element) < 1: continue - if _check_requires(element[0], node, statespace, constraint): - pass + # if _check_requires(element[0], node, statespace, constraint): + # pass results += element # Recursively search children @@ -283,7 +283,7 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid - and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None + # and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None ] for child in children: