diff --git a/mythril/analysis/modules/unchecked_suicide.py b/mythril/analysis/modules/unchecked_suicide.py index b1f7e5ae..2777b9e5 100644 --- a/mythril/analysis/modules/unchecked_suicide.py +++ b/mythril/analysis/modules/unchecked_suicide.py @@ -57,7 +57,7 @@ def execute(statespace): for s in statespace.sstors[index]: if s.tainted: - can_write = Trues + can_write = True issue.description += "\nThere is a check on storage index " + str(index) + ". This storage index can be written to by calling the function '" + s.node.function_name + "'." break diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 89b616a5..868253c8 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -3,6 +3,7 @@ from mythril.exceptions import UnsatError def get_model(constraints): s = Solver() + s.set("timeout", 2000) for constraint in constraints: s.add(constraint) @@ -12,5 +13,5 @@ def get_model(constraints): return s.model() else: - raise UnsatError + raise UnsatError diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 41382e11..0899bc57 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -69,19 +69,22 @@ class StateSpace: def sstor_analysis(self): - logging.debug("Analyzing storage operations...") + logging.info("Analyzing storage operations...") for index in self.sstors: for s in self.sstors[index]: # For now we simply 'taint' every storage location that is reachable without any constraint on msg.sender + taint = True + for constraint in s.node.constraints: - logging.debug("Constraint: " + str(constraint)) + # logging.debug("Constraint: " + str(constraint)) if ("caller" in str(constraint)): - s.tainted = False + taint = False break + if taint: try: solver.get_model(s.node.constraints) s.tainted = True