// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // Check that we get the expected results for the `size_of` intrinsic // with common data types #![feature(core_intrinsics)] use std::intrinsics::size_of; struct MyStruct {} enum MyEnum {} #[kani::proof] fn main() { // Scalar types assert!(size_of::<i8>() == 1); assert!(size_of::<i16>() == 2); assert!(size_of::<i32>() == 4); assert!(size_of::<i64>() == 8); assert!(size_of::<i128>() == 16); assert!(size_of::<isize>() == 8); assert!(size_of::<u8>() == 1); assert!(size_of::<u16>() == 2); assert!(size_of::<u32>() == 4); assert!(size_of::<u64>() == 8); assert!(size_of::<u128>() == 16); assert!(size_of::<usize>() == 8); assert!(size_of::<f32>() == 4); assert!(size_of::<f64>() == 8); assert!(size_of::<bool>() == 1); assert!(size_of::<char>() == 4); // Compound types (tuple and array) assert!(size_of::<(i32, i32)>() == 8); assert!(size_of::<[i32; 5]>() == 20); // Custom data types (struct and enum) assert!(size_of::<MyStruct>() == 0); assert!(size_of::<MyEnum>() == 0); }