From 997ea6d647e3187c7f30cf619d66ba9a379a404c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 12:31:53 +0000 Subject: [PATCH 1/3] Add safety dependency to alloc and std crates Just as previously done for core: this will enable future use of `safety::{ensures,requires}` in those crates. --- library/alloc/Cargo.toml | 1 + library/std/Cargo.toml | 1 + 2 files changed, 2 insertions(+) diff --git a/library/alloc/Cargo.toml b/library/alloc/Cargo.toml index 1bd4434d4f7e9..7911be6579f4e 100644 --- a/library/alloc/Cargo.toml +++ b/library/alloc/Cargo.toml @@ -11,6 +11,7 @@ edition = "2021" [dependencies] core = { path = "../core" } compiler_builtins = { version = "0.1.123", features = ['rustc-dep-of-std'] } +safety = { path = "../contracts/safety" } [dev-dependencies] rand = { version = "0.8.5", default-features = false, features = ["alloc"] } diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index e20fe9feff114..2d75324261318 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -26,6 +26,7 @@ hashbrown = { version = "0.14", default-features = false, features = [ std_detect = { path = "../stdarch/crates/std_detect", default-features = false, features = [ 'rustc-dep-of-std', ] } +safety = { path = "../contracts/safety" } # Dependencies of the `backtrace` crate rustc-demangle = { version = "0.1.24", features = ['rustc-dep-of-std'] } From ad2a2743017c0c15f65a45787e2a23690939e501 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 13:02:41 +0000 Subject: [PATCH 2/3] fixup! Add safety dependency to alloc and std crates --- library/alloc/src/lib.rs | 1 + library/std/src/lib.rs | 1 + 2 files changed, 2 insertions(+) diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index 7aaa4e73df72c..00eaeee3b84e0 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -130,6 +130,7 @@ #![feature(inplace_iteration)] #![feature(iter_advance_by)] #![feature(iter_next_chunk)] +#![feature(kani)] #![feature(layout_for_ptr)] #![feature(local_waker)] #![feature(maybe_uninit_slice)] diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs index 60969af3e8541..14195eba48522 100644 --- a/library/std/src/lib.rs +++ b/library/std/src/lib.rs @@ -269,6 +269,7 @@ #![cfg_attr(any(windows, target_os = "uefi"), feature(round_char_boundary))] #![cfg_attr(target_family = "wasm", feature(stdarch_wasm_atomic_wait))] #![cfg_attr(target_arch = "wasm64", feature(simd_wasm64))] +#![feature(kani)] // // Language features: // tidy-alphabetical-start From e1c783ed4d5bec97db0649093756ce4f7b090b02 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 13:38:46 +0000 Subject: [PATCH 3/3] fixup! Add safety dependency to alloc and std crates --- library/alloc/src/lib.rs | 2 +- library/std/src/lib.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index 00eaeee3b84e0..d28c5a29df2b9 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -91,6 +91,7 @@ // // Library features: // tidy-alphabetical-start +#![cfg_attr(kani, feature(kani))] #![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))] #![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))] #![feature(alloc_layout_extra)] @@ -130,7 +131,6 @@ #![feature(inplace_iteration)] #![feature(iter_advance_by)] #![feature(iter_next_chunk)] -#![feature(kani)] #![feature(layout_for_ptr)] #![feature(local_waker)] #![feature(maybe_uninit_slice)] diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs index 14195eba48522..3121ee8be8722 100644 --- a/library/std/src/lib.rs +++ b/library/std/src/lib.rs @@ -269,7 +269,7 @@ #![cfg_attr(any(windows, target_os = "uefi"), feature(round_char_boundary))] #![cfg_attr(target_family = "wasm", feature(stdarch_wasm_atomic_wait))] #![cfg_attr(target_arch = "wasm64", feature(simd_wasm64))] -#![feature(kani)] +#![cfg_attr(kani, feature(kani))] // // Language features: // tidy-alphabetical-start