Open
Description
hemv features an option that limits contracts doing reentrant calls: --promise-no-reent
. This helps to make this kind of exploration scalable:
function f(address x) {
uint y = C(x).g(..);
...
Since the x
cannot be the same contract, it avoid to repeat the same exploration over and over again at the cost of missing some paths where reentrancy is used.
In the case of looking for counter examples, instead of doing verification, we can go one step beyond restricting that the target of the calls to only allow contracts that are already deployed. This will make exploration even more scalable since fuzzers such as Echidna only deal with concrete contracts (allowing to have arbitrary deployments is usually too hard).