Carolyn Zech
Carolyn Zech
> I suppose you know about the very related option `--fail-uncoverable` which essentially converts all `cover!` macros into something like this. > Yes, I did see that. This implementation is...
Closing for now; this feature requires further design discussion.
Note that this fails the standard library job because a number of the `unchecked_mul` harnesses are restricted to ranges such that the precondition empties the search space. For example, `verify::unchecked_mul_usize_edge`...
Moving to draft for now -- we need to decide whether we want verification failure for these properties to be the default behavior, or a characteristic of the harness. This...
Closing this PR, since we don't have an answer for the UX questions and we have other features that are higher priority right now.
#4250 adds partial support for this, but we still don't support trait functions with generic parameters. The current limitation is that `resolve_in_trait_impl`: ```rust let trait_fn_fn_def = stable_fn_def(tcx, trait_fn_id).unwrap(); let desired_generic_args...
@rahulku This isn't going to merge automatically because it fails our required copyright status check. I believe we'll have to temporarily disable this check (or at least make it optional)...
I checked off the assess items assuming that we are deprecating `assess` per #4111
Verification succeeds in Kani v0.56. `git bisect` revealed that #3305 fixed the issue. @celinval I can go ahead and close, but I see you have an open PR for fixme...
@celinval should we close this as "won't do? given #3561?