Upgrade Rust toolchain to 2025-06-16

docs/src/rust-feature-support/intrinsics.md

@@ -174,8 +174,8 @@ logf32 | Partial | Results are overapproximated |
 logf64 | Partial | Results are overapproximated |
 maxnumf32 | Yes | |
 maxnumf64 | Yes | |
-min_align_of | Yes | |
-min_align_of_val | Yes | |
+align_of | Yes | |
+align_of_val | Yes | |
 minnumf32 | Yes | |
 minnumf64 | Yes | |
 move_val_init | No | |

kani-compiler/src/intrinsics.rs

@@ -309,11 +309,11 @@ impl Intrinsic {
                 assert_sig_matches!(sig, RigidTy::Bool => RigidTy::Bool);
                 Self::Likely
             }
-            "min_align_of" => {
+            "align_of" => {
                 assert_sig_matches!(sig, => RigidTy::Uint(UintTy::Usize));
                 Self::MinAlignOf
             }
-            "min_align_of_val" => {
+            "align_of_val" => {
                 assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
                 Self::MinAlignOfVal
             }

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-06-13"
+channel = "nightly-2025-06-16"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs

@@ -1,11 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that we get the expected results for the `min_align_of_val` intrinsic
+// Check that we get the expected results for the `align_of_val` intrinsic
 // with common data types. Note that these tests assume an x86_64 architecture,
 // which is the only architecture supported by Kani at the moment.
 #![feature(core_intrinsics)]
-use std::intrinsics::min_align_of_val;
+use std::intrinsics::align_of_val;
 
 struct MyStruct {
     val: u32,
@@ -26,55 +26,55 @@ fn main() {
     #[cfg(target_arch = "x86_64")]
     unsafe {
         // Scalar types
-        assert!(min_align_of_val(&0i8) == 1);
-        assert!(min_align_of_val(&0i16) == 2);
-        assert!(min_align_of_val(&0i32) == 4);
-        assert!(min_align_of_val(&0i64) == 8);
-        assert!(min_align_of_val(&0i128) == 16);
-        assert!(min_align_of_val(&0isize) == 8);
-        assert!(min_align_of_val(&0u8) == 1);
-        assert!(min_align_of_val(&0u16) == 2);
-        assert!(min_align_of_val(&0u32) == 4);
-        assert!(min_align_of_val(&0u64) == 8);
-        assert!(min_align_of_val(&0u128) == 16);
-        assert!(min_align_of_val(&0usize) == 8);
-        assert!(min_align_of_val(&0f32) == 4);
-        assert!(min_align_of_val(&0f64) == 8);
-        assert!(min_align_of_val(&false) == 1);
-        assert!(min_align_of_val(&(0 as char)) == 4);
+        assert!(align_of_val(&0i8) == 1);
+        assert!(align_of_val(&0i16) == 2);
+        assert!(align_of_val(&0i32) == 4);
+        assert!(align_of_val(&0i64) == 8);
+        assert!(align_of_val(&0i128) == 16);
+        assert!(align_of_val(&0isize) == 8);
+        assert!(align_of_val(&0u8) == 1);
+        assert!(align_of_val(&0u16) == 2);
+        assert!(align_of_val(&0u32) == 4);
+        assert!(align_of_val(&0u64) == 8);
+        assert!(align_of_val(&0u128) == 16);
+        assert!(align_of_val(&0usize) == 8);
+        assert!(align_of_val(&0f32) == 4);
+        assert!(align_of_val(&0f64) == 8);
+        assert!(align_of_val(&false) == 1);
+        assert!(align_of_val(&(0 as char)) == 4);
         // Compound types (tuple and array)
-        assert!(min_align_of_val(&(0i32, 0i32)) == 4);
-        assert!(min_align_of_val(&[0i32; 5]) == 4);
+        assert!(align_of_val(&(0i32, 0i32)) == 4);
+        assert!(align_of_val(&[0i32; 5]) == 4);
         // Custom data types (struct and enum)
-        assert!(min_align_of_val(&MyStruct { val: 0u32 }) == 4);
-        assert!(min_align_of_val(&MyEnum::Variant) == 1);
-        assert!(min_align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4);
+        assert!(align_of_val(&MyStruct { val: 0u32 }) == 4);
+        assert!(align_of_val(&MyEnum::Variant) == 1);
+        assert!(align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4);
     }
     #[cfg(target_arch = "aarch64")]
     unsafe {
         // Scalar types
-        assert!(min_align_of_val(&0i8) == 1);
-        assert!(min_align_of_val(&0i16) == 2);
-        assert!(min_align_of_val(&0i32) == 4);
-        assert!(min_align_of_val(&0i64) == 8);
-        assert!(min_align_of_val(&0i128) == 16);
-        assert!(min_align_of_val(&0isize) == 8);
-        assert!(min_align_of_val(&0u8) == 1);
-        assert!(min_align_of_val(&0u16) == 2);
-        assert!(min_align_of_val(&0u32) == 4);
-        assert!(min_align_of_val(&0u64) == 8);
-        assert!(min_align_of_val(&0u128) == 16);
-        assert!(min_align_of_val(&0usize) == 8);
-        assert!(min_align_of_val(&0f32) == 4);
-        assert!(min_align_of_val(&0f64) == 8);
-        assert!(min_align_of_val(&false) == 1);
-        assert!(min_align_of_val(&(0 as char)) == 4);
+        assert!(align_of_val(&0i8) == 1);
+        assert!(align_of_val(&0i16) == 2);
+        assert!(align_of_val(&0i32) == 4);
+        assert!(align_of_val(&0i64) == 8);
+        assert!(align_of_val(&0i128) == 16);
+        assert!(align_of_val(&0isize) == 8);
+        assert!(align_of_val(&0u8) == 1);
+        assert!(align_of_val(&0u16) == 2);
+        assert!(align_of_val(&0u32) == 4);
+        assert!(align_of_val(&0u64) == 8);
+        assert!(align_of_val(&0u128) == 16);
+        assert!(align_of_val(&0usize) == 8);
+        assert!(align_of_val(&0f32) == 4);
+        assert!(align_of_val(&0f64) == 8);
+        assert!(align_of_val(&false) == 1);
+        assert!(align_of_val(&(0 as char)) == 4);
         // Compound types (tuple and array)
-        assert!(min_align_of_val(&(0i32, 0i32)) == 4);
-        assert!(min_align_of_val(&[0i32; 5]) == 4);
+        assert!(align_of_val(&(0i32, 0i32)) == 4);
+        assert!(align_of_val(&[0i32; 5]) == 4);
         // Custom data types (struct and enum)
-        assert!(min_align_of_val(&MyStruct { val: 0u32 }) == 4);
-        assert!(min_align_of_val(&MyEnum::Variant) == 1);
-        assert!(min_align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4);
+        assert!(align_of_val(&MyStruct { val: 0u32 }) == 4);
+        assert!(align_of_val(&MyEnum::Variant) == 1);
+        assert!(align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4);
     }
 }

tests/kani/Intrinsics/ConstEval/align_of.rs

@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we get the expected results for the `align_of` intrinsic
+// with common data types
+#![feature(core_intrinsics)]
+use std::intrinsics::align_of;
+
+struct MyStruct {}
+
+enum MyEnum {}
+
+#[kani::proof]
+fn main() {
+    // for the following types x86_64 and aarch64 agree on the alignment; see
+    // AlignOfVal/align_of_fat_ptr.rs for some example of where they don't agree
+    #[cfg(any(target_arch = "x86_64", target_arch = "aarch64"))]
+    {
+        // Scalar types
+        assert!(align_of::<i8>() == 1);
+        assert!(align_of::<i16>() == 2);
+        assert!(align_of::<i32>() == 4);
+        assert!(align_of::<i64>() == 8);
+        assert!(align_of::<i128>() == 16);
+        assert!(align_of::<isize>() == 8);
+        assert!(align_of::<u8>() == 1);
+        assert!(align_of::<u16>() == 2);
+        assert!(align_of::<u32>() == 4);
+        assert!(align_of::<u64>() == 8);
+        assert!(align_of::<u128>() == 16);
+        assert!(align_of::<usize>() == 8);
+        assert!(align_of::<f32>() == 4);
+        assert!(align_of::<f64>() == 8);
+        assert!(align_of::<bool>() == 1);
+        assert!(align_of::<char>() == 4);
+        // Compound types (tuple and array)
+        assert!(align_of::<(i32, i32)>() == 4);
+        assert!(align_of::<[i32; 5]>() == 4);
+        // Custom data types (struct and enum)
+        assert!(align_of::<MyStruct>() == 1);
+        assert!(align_of::<MyEnum>() == 1);
+    }
+}