Gustavo Grieco
Gustavo Grieco
Fix for #2427
This PR contains: * A lazy evaluation mode for `jumpi` constraints enabled by default (so we can see the effects in the tests). This mode cannot be used if the...
When manticore is used during audits, it's very common to take a piece of code and abstract the state variables as parameters, to allow our tool to explore any possible...
In most of the cases, SMT solvers take the majority of the time when we run manticore. We have a `auto` selection for it and upcoming portfolio of them, but...
The timeout option is very important to make sure the solver don't take forever. It's unclear if they work as expected.
Most of the EVM tests access the list of states/transactions without considering that some of them could be unsound. For instance: https://github.com/trailofbits/manticore/blob/47326e688915132a32a56f7b892f8d8ca6ffb4b4/tests/ethereum/test_general.py#L672-L699 They should be changed to use only sound...
It seems that once a state goes from busy to killed, the worker handling that state will not take another one. This cases are not so rare to happen, for...
Explore the possibility of creating a database of hashes of SMT formula that are false. These do not require to save any model, so they can be easily replayed during...
Most of the smtlib2 tests have the use of the z3 solver hardcoded: https://github.com/trailofbits/manticore/blob/fd83be7a9929d3645a3df995e2f925d3fb3b4b7f/tests/other/test_smtlibv2.py#L995-L1020 Instead, they should use `self.solver` since that variable is properly initialized to have the correct instance:...
There is no clear documentation or examples of how to symbolically execute a bytecode-only Ethereum contract. In this case, the ABI will be provided by the user, but there is...