From 271eda6111036d2cb61c695c24c5c77baeb136ee Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 1 May 2019 14:17:47 +0200 Subject: [PATCH 1/2] Disable effect check feature --- mythril/analysis/modules/integer.py | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 0c6582a0..6b859b0a 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -31,6 +31,7 @@ import logging log = logging.getLogger(__name__) +DISABLE_EFFECT_CHECK = True class OverUnderflowAnnotation: """ Symbol Annotation used if a BitVector can overflow""" @@ -287,9 +288,15 @@ class IntegerOverflowUnderflowModule(DetectionModule): continue try: + # This check can be disabled if the contraints are to difficult for z3 to solve + # within any reasonable time. + if DISABLE_EFFECT_CHECK: + constraints = ostate.mstate.constraints + [annotation.constraint] + else: + constraints = state.mstate.constraints + [annotation.constraint] transaction_sequence = solver.get_transaction_sequence( - state, state.mstate.constraints + [annotation.constraint] + state, constraints ) except UnsatError: continue From ec0794a54b89a7cd59c045776b08f17d3ab22372 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 1 May 2019 14:20:17 +0200 Subject: [PATCH 2/2] add return character --- mythril/analysis/modules/integer.py | 1 + 1 file changed, 1 insertion(+) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 6b859b0a..43f57c96 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -33,6 +33,7 @@ log = logging.getLogger(__name__) DISABLE_EFFECT_CHECK = True + class OverUnderflowAnnotation: """ Symbol Annotation used if a BitVector can overflow"""