mythril.concolic package¶
Submodules¶
mythril.concolic.concolic_execution module¶
-
mythril.concolic.concolic_execution.
concolic_execution
(concrete_data: mythril.concolic.concrete_data.ConcreteData, jump_addresses: List[T], solver_timeout=100000) → List[Dict[str, Dict[str, Any]]][source]¶ Executes codes and prints input required to cover the branch flips :param input_file: Input file :param jump_addresses: Jump addresses to flip :param solver_timeout: Solver timeout
-
mythril.concolic.concolic_execution.
flip_branches
(init_state: mythril.laser.ethereum.state.world_state.WorldState, concrete_data: mythril.concolic.concrete_data.ConcreteData, jump_addresses: List[str], trace: List[T]) → List[Dict[str, Dict[str, Any]]][source]¶ Flips branches and prints the input required for branch flip
Parameters: - concrete_data – Concrete data
- jump_addresses – Jump addresses to flip
- trace – trace to follow
mythril.concolic.concrete_data module¶
mythril.concolic.find_trace module¶
-
mythril.concolic.find_trace.
concrete_execution
(concrete_data: mythril.concolic.concrete_data.ConcreteData) → Tuple[mythril.laser.ethereum.state.world_state.WorldState, List[T]][source]¶ Executes code concretely to find the path to be followed by concolic executor :param concrete_data: Concrete data :return: path trace