From e1c5fb7797bda2d28d4e72ea30af4ad70fd87471 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Mon, 1 Jul 2024 14:02:23 -0700 Subject: [PATCH] Enable `uninit-checks` in `std-checks` --- tests/std-checks/core/Cargo.toml | 2 +- tests/std-checks/core/src/slice.rs | 20 +++++++++++++++++--- 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/tests/std-checks/core/Cargo.toml b/tests/std-checks/core/Cargo.toml index f6e1645c3a39..a1496a0c81a7 100644 --- a/tests/std-checks/core/Cargo.toml +++ b/tests/std-checks/core/Cargo.toml @@ -7,7 +7,7 @@ edition = "2021" description = "This crate contains contracts and harnesses for core library" [package.metadata.kani] -unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true } +unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true, uninit-checks = true } [package.metadata.kani.flags] output-format = "terse" diff --git a/tests/std-checks/core/src/slice.rs b/tests/std-checks/core/src/slice.rs index 044f4bd38586..fe627f21a5ae 100644 --- a/tests/std-checks/core/src/slice.rs +++ b/tests/std-checks/core/src/slice.rs @@ -1,25 +1,30 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +extern crate kani; + /// Create wrapper functions to standard library functions that contains their contract. pub mod contracts { use kani::{mem::*, requires}; #[requires(can_dereference(std::ptr::slice_from_raw_parts(data, len)))] - #[requires(is_initialized(data, len))] pub unsafe fn from_raw_parts<'a, T>(data: *const T, len: usize) -> &'a [T] { std::slice::from_raw_parts(data, len) } + + #[requires(can_dereference(std::ptr::slice_from_raw_parts(data, len)))] + pub unsafe fn from_raw_parts_mut<'a, T>(data: *mut T, len: usize) -> &'a mut [T] { + std::slice::from_raw_parts_mut(data, len) + } } #[cfg(kani)] mod verify { use super::*; - const MAX_LEN: usize = 2; + const MAX_LEN: usize = isize::MAX as usize; #[kani::proof_for_contract(contracts::from_raw_parts)] - #[kani::unwind(25)] pub fn check_from_raw_parts_primitive() { let len: usize = kani::any(); kani::assume(len < MAX_LEN); @@ -27,4 +32,13 @@ mod verify { let arr = vec![0u8; len]; let _slice = unsafe { contracts::from_raw_parts(arr.as_ptr(), len) }; } + + #[kani::proof_for_contract(contracts::from_raw_parts_mut)] + pub fn check_from_raw_parts_mut_primitive() { + let len: usize = kani::any(); + kani::assume(len < MAX_LEN); + + let mut arr = vec![0u8; len]; + let _slice = unsafe { contracts::from_raw_parts_mut(arr.as_mut_ptr(), len) }; + } }