Skip to content

Create a new #[proof_for_safety(fn)] #3579

Description

@celinval

Provide a new harnesss type which will only take into consideration the function safety contract, and that will only fail if UB is detected or, if the target function is safe, if any variable at the boundary of the target function violates their type safety.

Note that this is similar to #[should_panic], but it should not fail the verification if it does not panic.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    Z-ContractsIssue related to code contracts[C] Feature / EnhancementA new feature request or enhancement to an existing feature.

    Projects

    No projects

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions