Skip to content

Remove deprecated kani::check #3561

@celinval

Description

@celinval

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

No one assigned

    Labels

    [E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions