addr_of on places derived from raw pointers should preserve permissions · patricklam/verify-rust-std@ed66a11

@@ -2285,9 +2285,13 @@ impl<F: FnPtr> fmt::Debug for F {

22852285

/// `addr_of!(expr)` is equivalent to `&raw const expr`. The macro is *soft-deprecated*;

22862286

/// use `&raw const` instead.

22872287

///

2288-

/// It is still an open question whether writing through an `addr_of!`-created pointer is permitted

2289-

/// or not. Until that is decided, the same rules as for shared references apply: it is UB to write

2290-

/// through a pointer created with this operation, except for bytes located inside an `UnsafeCell`.

2288+

/// It is still an open question under which conditions writing through an `addr_of!`-created

2289+

/// pointer is permitted. If the place `expr` evaluates to is based on a raw pointer, then the

2290+

/// result of `addr_of!` inherits all permissions from that raw pointer. However, if the place is

2291+

/// based on a reference, local variable, or `static`, then until all details are decided, the same

2292+

/// rules as for shared references apply: it is UB to write through a pointer created with this

2293+

/// operation, except for bytes located inside an `UnsafeCell`. Use `&raw mut` (or [`addr_of_mut`])

2294+

/// to create a raw pointer that definitely permits mutation.

22912295

///

22922296

/// Creating a reference with `&`/`&mut` is only allowed if the pointer is properly aligned

22932297

/// and points to initialized data. For cases where those requirements do not hold,