halmos
halmos copied to clipboard
Remove `metadata` checks for files with free functions / file-level functions
Describe the bug
If you currently use in some form contracts that use free functions (a.k.a file-level functions) via imports, halmos will issue the following warning:
Skipped FreeFunctionsFile.json due to parsing failure: KeyError: 'metadata'
Currently, this warning is printed in red colour. I would suggest orange should be enough ;). The underlying reason is that these files are compiled in the normal way (since in some contracts you will use them) but there is no metadata available in the standard JSON input file for these files.
To Reproduce
git clone https://github.com/pcaversaccio/snekmate and checkout the feat/halmos branch. Run pnpm install and forge install and invoke:
halmos --contract ERC20TestHalmos --function testHalmosAssertNoBackdoor --storage-layout generic --ffi -vvvv
Environment:
- OS:
Linux - Python version:
3.11.3 - Halmos and other dependency versions:
0.1.13.dev1+ga617814