halmos icon indicating copy to clipboard operation
halmos copied to clipboard

Remove `metadata` checks for files with free functions / file-level functions

Open pcaversaccio opened this issue 1 year ago • 0 comments

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

image

Environment:

  • OS: Linux
  • Python version: 3.11.3
  • Halmos and other dependency versions: 0.1.13.dev1+ga617814

pcaversaccio avatar Apr 28 '24 16:04 pcaversaccio