Filter sanity checks #1146
Filter sanity checks #1146
Conversation
…into filter-sanity-checks
scripts/cbmc_json_parser.py
Outdated
|
|
||
| def filter_properties(properties, message): | ||
| def filter_properties(properties, message=None, property_class=None): |
There was a problem hiding this comment.
Do we want a single property_class or a list?
There was a problem hiding this comment.
Maybe a wrapper function over this function which takes in a list of property_classes and messages? For this function itself, I think it's better to keep it simple, and call it over a list somewhere else.
scripts/cbmc_json_parser.py
Outdated
| @@ -329,6 +329,7 @@ def postprocess_results(properties, extra_ptr_check): | |||
| has_failed_unwinding_asserts = has_check_failure(properties, GlobalMessages.UNWINDING_ASSERT_DESC) | |||
| has_reachable_undefined_functions = modify_undefined_function_checks(properties) | |||
| properties, reach_checks = filter_reach_checks(properties) | |||
| properties = filter_sanity_checks(properties)[0] | |||
There was a problem hiding this comment.
Is there any chance this is empty?
There was a problem hiding this comment.
also, you should move this logic to be inside filter_sanity_checks
|
|
||
| /// This testcase is currently failing with the following error: | ||
| /// | ||
| /// [assertion.2] Reached assignment statement with unequal types Pointer { typ: |
There was a problem hiding this comment.
Good catch. As we discussed offline, sanity checks that fail should be visible and fail the verification. Thanks!
There was a problem hiding this comment.
let me address those cases and clean up some of the code as well
…into filter-sanity-checks
…into filter-sanity-checks
scripts/cbmc_json_parser.py
Outdated
|
|
||
| def filter_properties(properties, message): | ||
| def filter_properties(properties, message=None, property_class=None): |
There was a problem hiding this comment.
The changes to this function are no longer needed, right?
There was a problem hiding this comment.
Yes, redundant changes.
|
I've simplified this PR to just do the minimum and added a simple test to check for sanity_check. Will try to address comments on the spot to get it merged before tomorrow. |
Description of changes:
Properties which are sanity checks needed to be removed from the UI. They are now marked with the property_class "sanity_check" which makes it easy to filter such checks out as the pipeline to add, remove and edit checks based on their property_class has already been setup.
Resolved issues:
Resolves #1020
Call-outs:
Couldn't add tests for this UI change as it's a removal. In the future we should contain negative tests for similar changes.
Testing:
How is this change tested?
Is this a refactor change?
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.