Skip to content

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

@celinval

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.

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