Adjust PropertyClass of assertions to identify UB #3860
Conversation
Anything listed as undefined behavior (UB) at https://doc.rust-lang.org/reference/behavior-considered-undefined.html must also be considered UB by Kani and should not pass under `should_fail`. In preparation of this PR, all occurrences of `PropertyClass` in the code base were audited and, where necessary, adjusted. Also, all uses of `kani::assert` were audited to confirm or adjust them. This resulted in first-time use of the `UnsupportedCheck` hook, which implied fixes to its implementation. Resolves: model-checking#3571
| @@ -1,16 +1,16 @@ | |||
| multiple_instrumentations_different_vars.assertion.3\ | |||
| multiple_instrumentations_different_vars.assertion.1\ | |||
There was a problem hiding this comment.
can you remove these numbers?
There was a problem hiding this comment.
Will the pattern still match given we use the backslash at the end of the line?
Given how those were designed, is the only way to fix this to filter for their specific messages? My understanding is that those insert MIR-level assert calls, making them indistinguishable from user-provided assertions. Am I getting this wrong? |
Can we insert calls to I think we can just swap this code to retrieve By looking at this code, it reminded me that we also have an internal function named |
Anything listed as undefined behavior (UB) at
https://doc.rust-lang.org/reference/behavior-considered-undefined.html must also be considered UB by Kani and should not pass under
should_fail. In preparation of this PR, all occurrences ofPropertyClassin the code base were audited and, where necessary, adjusted.Also, all uses of
kani::assertwere audited to confirm or adjust them. This resulted in first-time use of theUnsupportedCheckhook, which implied fixes to its implementation.Resolves: #3571
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.