Pre-RFC: Safety Property System

libs
22

On reddit, Matthieum left some great comments, so we can still simplify #[discharges] for a shorter syntax and grouped SPs:

#[safety {
  ValidPtr, Align, Init: "`self.head_tail()` returns two slices to live elements";
  NotOwned: "because we incremented...";
  Alias(elem, head.iter());
}]
unsafe { ptr::read(elem) }

Very close to structured safety comments:

//  SAFETY
//  - ValidPtr, Aligned: by invariant.
//  - Init: `head` is a slice of initialized elements.
//  - NotOwned: because we incremented...
//  - Alias: ...
2 Likes