|
|
@ -3,6 +3,7 @@ from mythril.analysis.ops import * |
|
|
|
from mythril.analysis.report import Issue |
|
|
|
from mythril.analysis.report import Issue |
|
|
|
from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT |
|
|
|
from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT |
|
|
|
from mythril.exceptions import UnsatError |
|
|
|
from mythril.exceptions import UnsatError |
|
|
|
|
|
|
|
from mythril.laser.ethereum.transaction import ContractCreationTransaction |
|
|
|
import logging |
|
|
|
import logging |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@ -54,15 +55,25 @@ def _analyze_state(state, node): |
|
|
|
description += "The remaining Ether is sent to: " + str(to) + "\n" |
|
|
|
description += "The remaining Ether is sent to: " + str(to) + "\n" |
|
|
|
|
|
|
|
|
|
|
|
not_creator_constraints = [] |
|
|
|
not_creator_constraints = [] |
|
|
|
if len(state.world_state.transaction_sequence) > 1: |
|
|
|
if len(state.world_state.transaction_sequence) >= 1: |
|
|
|
creator = state.world_state.transaction_sequence[0].caller |
|
|
|
creator = None |
|
|
|
for transaction in state.world_state.transaction_sequence[1:]: |
|
|
|
if isinstance( |
|
|
|
not_creator_constraints.append( |
|
|
|
state.world_state.transaction_sequence[0], ContractCreationTransaction |
|
|
|
Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator)) |
|
|
|
): |
|
|
|
) |
|
|
|
creator = state.world_state.transaction_sequence[0].caller |
|
|
|
not_creator_constraints.append( |
|
|
|
if creator is not None: |
|
|
|
Not(Extract(159, 0, transaction.caller) == 0) |
|
|
|
for transaction in state.world_state.transaction_sequence[1:]: |
|
|
|
) |
|
|
|
not_creator_constraints.append( |
|
|
|
|
|
|
|
Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator)) |
|
|
|
|
|
|
|
) |
|
|
|
|
|
|
|
not_creator_constraints.append( |
|
|
|
|
|
|
|
Not(Extract(159, 0, transaction.caller) == 0) |
|
|
|
|
|
|
|
) |
|
|
|
|
|
|
|
else: |
|
|
|
|
|
|
|
for transaction in state.world_state.transaction_sequence: |
|
|
|
|
|
|
|
not_creator_constraints.append( |
|
|
|
|
|
|
|
Not(Extract(159, 0, transaction.caller) == 0) |
|
|
|
|
|
|
|
) |
|
|
|
|
|
|
|
|
|
|
|
try: |
|
|
|
try: |
|
|
|
model = solver.get_model(node.constraints + not_creator_constraints) |
|
|
|
model = solver.get_model(node.constraints + not_creator_constraints) |
|
|
|