-
Notifications
You must be signed in to change notification settings - Fork 62
New issue
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
test: more regression tests + external tests #121
Conversation
daejunpark
commented
Jul 17, 2023
•
edited
Loading
edited
- add more regression tests, including assertion violation cases
- add --json-output option to output test results in json
- add new pytest that runs all regression tests
- add external tests
@@ -1,30 +1,32 @@ | |||
// SPDX-License-Identifier: AGPL-3.0 | |||
pragma solidity >=0.8.0 <0.9.0; | |||
|
|||
// NOTE: required options: --loop 4 --symbolic-storage |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
out of scope for this but it would be really great if we could annotate it at the contract or method level
/// @custom:halmos loop=4
/// @custom:halmos symbolic-storage=true
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yes, it would be great! it's on the todo list.
src/halmos/__main__.py
Outdated
@@ -1089,7 +1114,7 @@ def parse_build_out(args: argparse.Namespace) -> Dict: | |||
return result | |||
|
|||
|
|||
def main() -> int: | |||
def main(argv=None, test_results_map=None) -> int: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
it seems a little odd to pass a "write argument" to main, but ok 🙃 could use a docstring explaining that it's basically for testing, to essentially avoid going through file IO right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
i wasn't happy with this either, but did so to avoid unnecessary asdict
conversion for test results in normal execution. i refactored the code to improve this, and now it explicitly returns the test results.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looking good! Excited to get more robust testing in place 💪