We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
createCalldata
Describe the bug
When using createCalldata, only the function arguments are shown
To Reproduce
git clone https://github.com/aviggiano/halmos-differential-erc20 git checkout 17c99b890779512b688dff5677afe48516c8ccf9 halmos
Environment:
Additional context
Logs:
Counterexample: p_amount_uint256_21 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0) p_amount_uint256_42 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0) p_from_address_19 = 0x0000000000000000008000000000000000000000 p_from_address_40 = 0x0000000000000000000000000000000000000000 p_n_staticcalls_uint256_00 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0) p_senders[0]_address_00 = 0xffffffff7fffbfcdbe7ffffffff7fffffdfeffff p_senders[1]_address_00 = 0x0000000000000000000000000000000000000000 p_senders_length_00 = 0x0000000000000000000000000000000000000000000000000000000000000002 p_to_address_20 = 0x0000000000000000008000000000000000000000 p_to_address_41 = 0x0000000000000000000000000000000000000000
Note: this is a minor issue, since console.log helps with debugging
console.log
The text was updated successfully, but these errors were encountered:
thanks for reporting. in the meantime while we're improving this, you can use the following trick:
function check_...(..., bytes4 selector, ...) { data = svm.createCalldata(...); vm.assume(selector == bytes4(data)); ... }
this way, you'll see the selector in counterexamples.
Sorry, something went wrong.
No branches or pull requests
Describe the bug
When using
createCalldata
, only the function arguments are shownTo Reproduce
Environment:
Additional context
Logs:
Note: this is a minor issue, since
console.log
helps with debuggingThe text was updated successfully, but these errors were encountered: