1use crate::prelude::*; 2use core::cell::*; 3 4extern_spec! { 5 impl<T> UnsafeCell<T> { 6 #[check(ghost)] 7 fn new(value: T) -> UnsafeCell<T>; 8 } 9 10 impl<T: ?Sized> UnsafeCell<T> { 11 #[check(ghost)] 12 fn get(&self) -> *mut T; 13 } 14}