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
When we generate calls with symbolic calldata, the trace output is not great. For example, in Unstoppable, we have this straightforward Attacker code:
contract SymbolicAttacker is Test, SymTest { function attack() public { address target = svm.createAddress("target"); bytes memory data = svm.createBytes(100, 'data'); target.call(data); } }
But when we run halmos --function check_unstoppable --solver-timeout-assertion 0 -vvv --statistics, we get this inscrutable part of the trace:
halmos --function check_unstoppable --solver-timeout-assertion 0 -vvv --statistics
CALL SymbolicAttacker::attack() STATICCALL svm::0x00000000(Concat(0x0000000000000000, halmos_target_address_d261631_01(), 0x0000002000000000000000000000000000000000000000000000000000000000000000067461726765740000000000000000000000000000000000000000000000000000)) ↩ Concat(0x000000000000000000000000, halmos_target_address_d261631_01()) STATICCALL hevm::assume(If(==(halmos_target_address_d261631_01(), 0x00000000000000000000000000000000aaaa0005), 0x0000000000000000000000000000000000000000000000000000000000000000, 0x0000000000000000000000000000000000000000000000000000000000000001)) ↩ 0x STATICCALL svm::createBytes(0x0000000000000000000000000000000000000000000000000000000000000064000000000000000000000000000000000000000000000000000000000000004000000000000000000000000000000000000000000000000000000000000000046461746100000000000000000000000000000000000000000000000000000000) ↩ Concat(0x00000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000064, halmos_data_bytes_db9a296_02()) CALL 0xaaaa0002::Extract(halmos_data_bytes_db9a296_02())(Extract(halmos_data_bytes_db9a296_02())) LOG3(topic0=Transfer, topic1=0x00000000000000000000000000000000000000000000000000000000aaaa0005, topic2=Concat(0x000000000000000000000000, Extract(halmos_data_bytes_db9a296_02())), data=Extract(halmos_data_bytes_db9a296_02())) ↩ RETURN 0x0000000000000000000000000000000000000000000000000000000000000001 ↩ STOP 0x
The text was updated successfully, but these errors were encountered:
No branches or pull requests
When we generate calls with symbolic calldata, the trace output is not great. For example, in Unstoppable, we have this straightforward Attacker code:
But when we run
halmos --function check_unstoppable --solver-timeout-assertion 0 -vvv --statistics
, we get this inscrutable part of the trace:The text was updated successfully, but these errors were encountered: