Only add constraint to symbolic Ether balances

model-balances
Nathan 5 years ago
parent 3c2ef90056
commit 2aa0d39646
  1. 11
      mythril/analysis/solver.py
  2. 1
      mythril/laser/ethereum/transaction/transaction_models.py

@ -200,11 +200,12 @@ def _set_minimisation_constraints(
for account in world_state.accounts.values():
# Lazy way to prevent overflows and to ensure "reasonable" balances
# Each account starts with less than 100 ETH
constraints.append(
UGE(
symbol_factory.BitVecVal(100000000000000000000, 256),
world_state.starting_balances[account.address],
if account.address.symbolic:
constraints.append(
UGE(
symbol_factory.BitVecVal(100000000000000000000, 256),
world_state.starting_balances[account.address],
)
)
)
return constraints, tuple(minimize)

@ -189,7 +189,6 @@ class ContractCreationTransaction(BaseTransaction):
0, concrete_storage=True, creator=caller.value
)
callee_account.contract_name = contract_name
# TODO: set correct balance for new account
super().__init__(
world_state=world_state,
callee_account=callee_account,

Loading…
Cancel
Save