Requested feature: Enable users to verify and stub compiler intrinsics with Kani contract
Use case: Intrinsics are functions implemented in the compiler. Today there are three possible intrinsics definitions:
- Functions declared as an
extern "rust-intrinsics" without any body.
- Functions annotated with
#[rustc_intrinsic] and annotated with #[rustc_intrinsic_must_be_overridden]. These functions have a dummy body that is ignored by the compiler. For StableMIR, 1 and 2 are handled the same way, i.e., they are intrinsics without a body.
- Functions annotated with
#[rustc_intrinsic] and not annotated with #[rustc_intrinsic_must_be_overridden]. These functions are marked as intrinsics, but they provide a fallback body.
Kani contract support for those are very limited. Users cannot annotate intrinsics from category 1 with Kani contract due to #3325. Users can add contracts to the other categories, but their contracts are ignored.
Requested feature: Enable users to verify and stub compiler intrinsics with Kani contract
Use case: Intrinsics are functions implemented in the compiler. Today there are three possible intrinsics definitions:
extern "rust-intrinsics"without any body.#[rustc_intrinsic]and annotated with#[rustc_intrinsic_must_be_overridden]. These functions have a dummy body that is ignored by the compiler. For StableMIR, 1 and 2 are handled the same way, i.e., they are intrinsics without a body.#[rustc_intrinsic]and not annotated with#[rustc_intrinsic_must_be_overridden]. These functions are marked as intrinsics, but they provide a fallback body.Kani contract support for those are very limited. Users cannot annotate intrinsics from category 1 with Kani contract due to #3325. Users can add contracts to the other categories, but their contracts are ignored.