diff --git a/Cargo.toml b/Cargo.toml index 6ab26345a09e..a83963ad986c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -72,6 +72,7 @@ exclude = [ "tests/script-based-pre/build-cache-bin/target/new_dep", "tests/script-based-pre/build-cache-dirty/target/new_dep", "tests/script-based-pre/verify_std_cmd/tmp_dir/target/kani_verify_std", + "tests/script-based-pre/kani_lib_dep", ] [workspace.lints.clippy] diff --git a/library/kani_core/src/arbitrary/pointer.rs b/library/kani_core/src/arbitrary/pointer.rs index 0e987b1260c6..2222e31b2f0b 100644 --- a/library/kani_core/src/arbitrary/pointer.rs +++ b/library/kani_core/src/arbitrary/pointer.rs @@ -265,7 +265,7 @@ macro_rules! ptr_generator { let ptr = match status { AllocationStatus::Dangling => { // Generate potentially unaligned pointer. - let offset = kani::any_where(|b: &usize| *b < size_of::()); + let offset = kani::any_where(|b: &usize| *b < core::mem::size_of::()); crate::ptr::NonNull::::dangling().as_ptr().wrapping_add(offset) } AllocationStatus::DeadObject => { @@ -279,7 +279,7 @@ macro_rules! ptr_generator { AllocationStatus::OutOfBounds => { // Generate potentially unaligned pointer. let buf_ptr = addr_of_mut!(self.buf) as *mut u8; - let offset = kani::any_where(|b: &usize| *b < size_of::()); + let offset = kani::any_where(|b: &usize| *b < core::mem::size_of::()); unsafe { buf_ptr.add(Self::BUF_LEN - offset) as *mut T } } }; @@ -331,7 +331,7 @@ macro_rules! ptr_generator { "Cannot generate in-bounds object of the requested type. Buffer is not big enough." ); let buf_ptr = addr_of_mut!(self.buf) as *mut u8; - let offset = kani::any_where(|b: &usize| *b <= Self::BUF_LEN - size_of::()); + let offset = kani::any_where(|b: &usize| *b <= Self::BUF_LEN - core::mem::size_of::()); let ptr = unsafe { buf_ptr.add(offset) as *mut T }; let is_initialized = kani::any(); if is_initialized { @@ -356,8 +356,8 @@ macro_rules! ptr_generator_fn { () => { /// Create a pointer generator that fits at least `N` elements of type `T`. pub fn pointer_generator() - -> PointerGenerator<{ size_of::() * NUM_ELTS }> { - PointerGenerator::<{ size_of::() * NUM_ELTS }>::new() + -> PointerGenerator<{ core::mem::size_of::() * NUM_ELTS }> { + PointerGenerator::<{ core::mem::size_of::() * NUM_ELTS }>::new() } }; } diff --git a/tests/script-based-pre/kani_lib_dep/Cargo.toml b/tests/script-based-pre/kani_lib_dep/Cargo.toml new file mode 100644 index 000000000000..89c2abb02687 --- /dev/null +++ b/tests/script-based-pre/kani_lib_dep/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "kani_lib_dep" +version = "0.1.0" +edition = "2021" + +[dependencies] +kani_core = { path = "../../../library/kani_core" } +kani = { path = "../../../library/kani" } diff --git a/tests/script-based-pre/kani_lib_dep/build.sh b/tests/script-based-pre/kani_lib_dep/build.sh new file mode 100755 index 000000000000..8bcf8e74c10e --- /dev/null +++ b/tests/script-based-pre/kani_lib_dep/build.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Test building a crate that has the Kani library as a dependency + +set -e + +rm -rf target + +set -e +cargo build + +rm -rf target diff --git a/tests/script-based-pre/kani_lib_dep/config.yml b/tests/script-based-pre/kani_lib_dep/config.yml new file mode 100644 index 000000000000..4e1b16c746e8 --- /dev/null +++ b/tests/script-based-pre/kani_lib_dep/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: build.sh +expected: expected +exit_code: 0 diff --git a/tests/script-based-pre/kani_lib_dep/expected b/tests/script-based-pre/kani_lib_dep/expected new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/tests/script-based-pre/kani_lib_dep/src/main.rs b/tests/script-based-pre/kani_lib_dep/src/main.rs new file mode 100644 index 000000000000..e5e3b8fc88c7 --- /dev/null +++ b/tests/script-based-pre/kani_lib_dep/src/main.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use kani::Arbitrary; + +struct Foo { + x: i32, + y: i32, + z: i32, +} + +impl Arbitrary for Foo { + fn any() -> Self { + Foo { x: 3, y: 4, z: 5 } + } +} + +fn main() { + let f: Foo = kani::any(); + assert_eq!(f.x, 3); + assert_eq!(f.y, 4); + assert_eq!(f.z, 5); +}