pull/375/head^2
Joran Honig 6 years ago
parent ab4c49e78c
commit e0e92630b9
  1. 1
      mythril/analysis/modules/integer.py
  2. 2
      mythril/analysis/solver.py
  3. 2
      mythril/laser/ethereum/svm.py

@ -30,7 +30,6 @@ def execute(statespace):
node = statespace.nodes[k] node = statespace.nodes[k]
for state in node.states: for state in node.states:
# pass
issues += _check_integer_underflow(statespace, state, node) issues += _check_integer_underflow(statespace, state, node)
issues += _check_integer_overflow(statespace, state, node) issues += _check_integer_overflow(statespace, state, node)

@ -12,7 +12,7 @@ def get_model(constraints):
if result == sat: if result == sat:
return s.model() return s.model()
elif result == unknown: elif result == unknown:
logging.error("Timeout encountered while solving expression using z3") logging.info("Timeout encountered while solving expression using z3")
raise UnsatError raise UnsatError

@ -70,7 +70,7 @@ class LaserEVM:
try: try:
new_states, op_code = self.execute_state(global_state) new_states, op_code = self.execute_state(global_state)
except NotImplementedError: except NotImplementedError:
logging.error("Encountered unimplemented instruction: {}".format(op_code)) logging.info("Encountered unimplemented instruction: {}".format(op_code))
continue continue
if len(new_states) == 0: if len(new_states) == 0:

Loading…
Cancel
Save