Add a test for breakpoint
#1022
Conversation
tests/kani/Intrinsics/breakpoint.rs
Outdated
| #[kani::proof] | ||
| fn main() { | ||
| unsafe { std::intrinsics::breakpoint() }; | ||
| assert!(true); |
There was a problem hiding this comment.
Can you add something more meaningful and maybe move this to the expected test suite to ensure it is reachable?
If I'm not wrong, assert!(true) doesn't even get codegen. So this test would still succeed even if the breakpoint was translated to a return statement.
There was a problem hiding this comment.
assert!(true) does codegen, and in fact produces the only check:
RESULTS:
Check 1: main.assertion.1
- Status: SUCCESS
- Description: "assertion failed: true"
- Location: breakpoint.rs:11:5 in function main
I'm okay with moving this into expected, but I'm not sure how that ensures it is reachable if I remove the assertion.
There was a problem hiding this comment.
Oh, this works now because we override assert!(). Before that, this code would be pruned by the compiler. Good to know! :)
In this case, you can just check that this assertion is reachable.
There was a problem hiding this comment.
Converted to an expected test. Both approaches seem equivalent to me (if the assertion were not reachable, verification would fail), but if anything goes wrong I'm sure expected will complain before 😄
There was a problem hiding this comment.
Actually, verification succeeds if there are no failures (even if a check is unreachable).
There was a problem hiding this comment.
Right, thanks! Then I take that back, expected is the best option here.
* Add a test for `breakpoint` * Convert into an `expected` test * Update comment on test
* Add a test for `breakpoint` * Convert into an `expected` test * Update comment on test
* Add a test for `breakpoint` * Convert into an `expected` test * Update comment on test
* Add a test for `breakpoint` * Convert into an `expected` test * Update comment on test
Description of changes:
Adds a test for
breakpoint. It checks that is supported (breakpointgenerates aSKIPstatement)and that it does not affect the verification result by adding an
assert!(true)after it.If you have ideas on how to test "skip" intrinsics, please let me know.
Resolved issues:
Part of #727
Call-outs:
Testing:
How is this change tested? Adds one test.
Is this a refactor change? N/A
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.