diff --git a/manticore/__main__.py b/manticore/__main__.py index d882ebe..b85cfeb 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -65,6 +65,9 @@ def parse_arguments(): parser.add_argument('--txlimit', type=positive, help='Maximum number of symbolic transactions to run (positive integer) (Ethereum only)') + parser.add_argument('--txnocoverage', action='store_true', + help='Do not use coverage as stopping criteria (Ethereum only)') + parser.add_argument('--txaccount', type=str, default="attacker", help='Account used as caller in the symbolic transactions, either "attacker" or "owner" (Ethereum only)') @@ -96,7 +99,7 @@ def ethereum_cli(args): logger.info("Beginning analysis") - m.multi_tx_analysis(args.argv[0], args.contract, args.txlimit, args.txaccount) + m.multi_tx_analysis(args.argv[0], args.contract, args.txlimit, not args.txnocoverage, args.txaccount) def main(): diff --git a/manticore/ethereum.py b/manticore/ethereum.py index c6a0ee2..01ecd2a 100644 --- a/manticore/ethereum.py +++ b/manticore/ethereum.py @@ -981,7 +981,7 @@ class ManticoreEVM(Manticore): return status - def multi_tx_analysis(self, solidity_filename, contract_name=None, tx_limit=None, tx_account="attacker"): + def multi_tx_analysis(self, solidity_filename, contract_name=None, tx_limit=None, tx_use_coverage=True, tx_account="attacker"): with open(solidity_filename) as f: source_code = f.read() @@ -1007,7 +1007,7 @@ class ManticoreEVM(Manticore): prev_coverage = 0 current_coverage = 0 - while current_coverage < 100: + while current_coverage < 100 or not tx_use_coverage: try: run_symbolic_tx() except NoAliveStates: @@ -1018,12 +1018,13 @@ class ManticoreEVM(Manticore): if tx_limit == 0: break - prev_coverage = current_coverage - current_coverage = self.global_coverage(contract_account) - found_new_coverage = prev_coverage < current_coverage + if tx_use_coverage: + prev_coverage = current_coverage + current_coverage = self.global_coverage(contract_account) + found_new_coverage = prev_coverage < current_coverage - if not found_new_coverage: - break + if not found_new_coverage: + break self.finalize()