From 1f84fb1fc08c1e614d659967d107fd1645d40f79 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 10 Mar 2020 16:24:09 +0100 Subject: [PATCH] Use UGT comparison --- .../plugins/implementations/mutation_pruner.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index 3213dd76..73963d3a 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -5,6 +5,7 @@ from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( ) from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.svm import LaserEVM +from mythril.laser.smt import UGT, symbol_factory from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) @@ -59,9 +60,17 @@ class MutationPruner(LaserPlugin): ): return + if isinstance(global_state.environment.callvalue, int): + callvalue = symbol_factory.BitVecVal( + global_state.environment.callvalue, 256 + ) + else: + callvalue = global_state.environment.callvalue + try: + constraints = global_state.world_state.constraints + [ - global_state.environment.callvalue > 0 + UGT(callvalue, symbol_factory.BitVecVal(0, 256)) ] solver.get_model(constraints)