Use fully-qualified name for size_of

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]

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::<T>());
+                        let offset = kani::any_where(|b: &usize| *b < core::mem::size_of::<T>());
                         crate::ptr::NonNull::<T>::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::<T>());
+                        let offset = kani::any_where(|b: &usize| *b < core::mem::size_of::<T>());
                         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::<T>());
+                let offset = kani::any_where(|b: &usize| *b <= Self::BUF_LEN - core::mem::size_of::<T>());
                 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<T, const NUM_ELTS: usize>()
-        -> PointerGenerator<{ size_of::<T>() * NUM_ELTS }> {
-            PointerGenerator::<{ size_of::<T>() * NUM_ELTS }>::new()
+        -> PointerGenerator<{ core::mem::size_of::<T>() * NUM_ELTS }> {
+            PointerGenerator::<{ core::mem::size_of::<T>() * NUM_ELTS }>::new()
         }
     };
 }

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" }

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

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

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);
+}