ethereum / hevm

symbolic EVM evaluator
https://hevm.dev
GNU Affero General Public License v3.0
235 stars 48 forks source link

Support to function deal (3 parameters) of StdCheats.sol #423

Open acmLL opened 12 months ago

acmLL commented 12 months ago

Configuration: MacBook Pro, Apple M1 Pro, Sonoma 14.0, 32GB RAM

hevm: version 0.52.0 Z3: Z3 version 4.12.2 - 64 bit

When I call the below function in a symbolic test (prove):

function deal(address token, address to, uint256 give, bool adjust) internal virtual

I got

[FAIL] prove_harvest()

Failure: prove_harvest()

No reachable assertion violations, but all branches reverted Prefix this testname with proveFail if this is expected

And I identified that the cause is in this statement:

// update balance stdstore.target(token).sig(0x70a08231).with_key(to).checked_write(give);

Thanks!

d-xo commented 12 months ago

hm yeah, fleshing out cheatcode support to the point where the full forge-std test suite passes is very desirable but is also a bit of a larger project. I think in this case we would need to support at least vm.record and vm.access