Enable concrete playback for satisfiable cover properties #2134
Conversation
| if self.args.concrete_playback.is_some() | ||
| && !self.args.quiet | ||
| && results.iter().all(|r| !r.result.generated_concrete_test) | ||
| { | ||
| println!( | ||
| "INFO: The concrete playback feature never generated unit tests because there were no failing harnesses." |
There was a problem hiding this comment.
Do you think we even need this? I was also wondering if we print that when a unit tests wasn't generated because it already existed.
There was a problem hiding this comment.
I do think it is better than not printing anything, which could leave the user wondering whether the --concrete-playback option had any effect.
There was a problem hiding this comment.
I was also wondering if we print that when a unit tests wasn't generated because it already existed.
We do that here.
I misunderstood the question initially. We currently don't print it if the test already existed. Not sure if we should.
| #[kani::proof] | ||
| pub fn harness() { | ||
| let x: i32 = kani::any(); | ||
| kani::cover!(x != 0 && x / 2 == 0); |
There was a problem hiding this comment.
Can you make this check to have only one satisfying value, so we avoid having to change the test whenever CBMC decides to produce a different value.
There was a problem hiding this comment.
Good point. Done.
Description of changes:
Include satisfiable cover properties as part of what concrete playback can generate tests for.
Resolved issues:
Resolves #2133
Related RFC:
Optional #ISSUE-NUMBER.
Call-outs:
Testing:
How is this change tested? Added a new test
Is this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.