-
Notifications
You must be signed in to change notification settings - Fork 981
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
[WIP] Adds initial support for kspec coverage tool #360
Conversation
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 think it is probably worth to add tests with inherited contracts, I am not sure the coverage works as expected in these cases.
We should also add unit tests to ensure it works on all the verified Solidity contracts from https://github.com/runtimeverification/verified-smart-contracts |
function_arguments = [refactor_type(arg.strip().split(' ')[0]) for arg in function_arguments] | ||
function_full_name = function_full_name[:start] + ','.join(function_arguments) + ')' | ||
covered_functions.add((contract_name, function_full_name)) | ||
i += 1 |
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 would refactor this code, it's weak and too order dependent/specific. I can imagine it causing bugs. It was just kept this way because it worked without issue for the specific codebase it was designed for.
Refactor complete. Uses |
I am closing this in profit of #364 |
This PR adds support for a new kspec coverage tool.
Usage:
slither-kspec-coverage contract.sol kspec.md
The tool currently checks which functions in the specified
contract.sol
have corresponding Klab specifications in the providedkspec.md
. It outputs a table illustrating which contract functions havekspec funcs
,kspec reached funcs
ornot covered funcs
.kspec funcs
indicates contract functions that have corresponding Klab specifications.kspec reached funcs
indicates contract functions that do not have corresponding Klab specifications themselves but are called by functions that do have Klab specifications.not covered funcs
highlights contract functions that do not have corresponding Klab specifications. The last two categories of functions need attention because they do not have Klab coverage.For example:
slither-kspec-coverage ./kspec_coverage/test/token/token.sol ./kspec_coverage/test/token/spec.md
produces: