Add custom mir support for PtrMetadata · model-checking/verify-rust-std@a4025eb (original) (raw)

Original file line number Diff line number Diff line change
@@ -360,6 +360,10 @@ define!("mir_assume", fn Assume(operand: bool));
360 360 define!("mir_deinit", fn Deinit<T>(place: T));
361 361 define!("mir_checked", fn Checked<T>(binop: T) -> (T, bool));
362 362 define!("mir_len", fn Len<T>(place: T) -> usize);
363 +define!(
364 +"mir_ptr_metadata",
365 +fn PtrMetadata<P: ?Sized>(place: *const P) -> <P as ::core::ptr::Pointee>::Metadata
366 +);
363 367 define!("mir_copy_for_deref", fn CopyForDeref<T>(place: T) -> T);
364 368 define!("mir_retag", fn Retag<T>(place: T));
365 369 define!("mir_move", fn Move<T>(place: T) -> T);