Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove deprecated kani::check #3561

Closed
1 of 2 tasks
celinval opened this issue Oct 1, 2024 · 0 comments · Fixed by #3614
Closed
1 of 2 tasks

Remove deprecated kani::check #3561

celinval opened this issue Oct 1, 2024 · 0 comments · Fixed by #3614
Labels
[E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one.

Comments

@celinval
Copy link
Contributor

celinval commented Oct 1, 2024 •
edited
Loading

Proposed change: Deprecate the recently added kani::check function that generates non-fatal properties. I believe this was accidentally added as a new stable function as part of the uninitialized memory checks work.

Motivation: I don't think we have a clear use-case for this API today, and this will likely cause more confusion around which API to use, assertion vs cover vs check.

I'm OK keeping this internal to Kani for cases where we implement checks using demonic non-determinism to ensure some conditions are never violated.

  • Deprecate API (Kani 0.56)
  • Make it private (Kani 0.57)

Note: I have changed my mind since I created #695. I think cover is a much better fit for the cases I originally had in mind.
@celinval celinval added the [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. label Oct 1, 2024
@celinval celinval mentioned this issue Oct 1, 2024
Merged
@celinval celinval mentioned this issue Oct 18, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Oct 19, 2024
@celinval
[Breaking change] Make kani::check private (#3614)
00c648d 
In the previous release, we added a deprecation warning to `kani::check`
which was incorrectly exposed in our crate interface.

Make this private and remove the deprecation tag.

Resolves #3561

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[Breaking change] Make kani::check private celinval/kani-dev
1 participant
@celinval