// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-verify-fail #![feature(core_intrinsics)] use std::intrinsics::*; #[kani::proof] fn main() { let mut a: Box<u8> = Box::new(0); unsafe { let x = volatile_load(&*a); assert!(x == *a); volatile_store(&mut *a, 1); assert!(*a == 1); unaligned_volatile_store(&mut *a, 2); assert!(*a == 2); volatile_set_memory(&mut *a, 3, 1); assert!(*a == 3); } }