Syntax fixes

model-checking · Jul 9, 2024 · 2f1be0d · 2f1be0d
1 parent 3b8b99a
commit 2f1be0d
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
@@ -505,7 +505,7 @@ impl fmt::Display for LayoutError {
 mod verify {
     use crate::kani;
 
-    #[kani::proof_for_contact(from_size_align_unchecked)]
+    #[kani::proof_for_contract(from_size_align_unchecked)]
     pub fn check_from_size_align_unchecked() {
         let s = kani::any::<usize>();
         let shift_index = kani::any::<u8>();

diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs
@@ -4,6 +4,9 @@ use crate::num::NonZero;
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{cmp, fmt, hash, mem, num};
 
+#[cfg(kani)]
+use crate::kani;
+
 /// A type storing a `usize` which is a power of two, and thus
 /// represents a possible alignment in the Rust abstract machine.
 ///