UI fix : Fix missing function check descriptions #1126
Conversation
| // SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
|
||
| // kani-flags: --enable-unstable --cbmc-args --unwind 4 --object-bits 9 | ||
|
|
There was a problem hiding this comment.
Can you add a comment explaining what this test is testing?
| // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
| // SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
|
||
| #[kani::proof] |
There was a problem hiding this comment.
Same here, comment what is this test testing
| """ | ||
| prop_class = prop["property"].rsplit(".", 3) | ||
| # Do nothing if prop_class is diff than cbmc's convention | ||
| class_id = prop_class[-2] if len(prop_class) > 1 else None |
There was a problem hiding this comment.
Should we warn/log this error?
There was a problem hiding this comment.
Maybe in some developer log but to the user, this error should make no difference at all. This convention/tag schema is mostly for our consumption at the end of it.
| 1. Searches for any check which has unknown file location or missing defition and replaces description | ||
| 2. If any of these checks has a failure status, then we turn all the sucesses into undetermined. | ||
| """ | ||
| has_unknown_location_checks = False |
There was a problem hiding this comment.
I would call this has_reachable_undefined_functions.
| """ | ||
| has_unknown_location_checks = False | ||
| for property in properties: | ||
| if GlobalMessages.ASSERTION_FALSE in property["description"] and extract_property_class( |
There was a problem hiding this comment.
Can we add a comment that this logic is intended to capture assertions that CBMC generates for functions with missing definitions?
One way to check whether this logic matches other checks is to run the regressions without the --generate-function-body-options assert-false-assume-false that we pass to goto-instrument (which would disable the undefined function checks) and see if any other checks are captured by this logic.
There was a problem hiding this comment.
After running the suggested experiment, no unexpected tests were found to change their result so we can safely assume that this logic doesn't capture false positives.
typo fixed Co-authored-by: Zyad Hassan <[email protected]>
Description of changes:
Fixes output for cases where there are checks with unreachable functions with missing definitions.
Before -
After -
UNDETERMINEDif any such check has aFAILUREstatus.Resolved issues:
Addresses -
&strfrom&[u8]#241Call-outs:
Only a temporary fix , in the future, we'll need to resolve the mangled names.
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.