generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 134
Closed
Labels
[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.
Description
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.
Metadata
Metadata
Assignees
Labels
[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.