Open
Description
The experimental contract support MCP has been approved. The syntax proposed looks like the following:
#[rustc_contracts::requires(for safety: self.len() > 0)]
#[rustc_contracts::ensures(
for safety: |output| output == old(self.start),
for correctness: |_output| self.len() == old(self.len()) - 1)]
unsafe fn next_unchecked(&mut self) -> usize {
// function body
}
The main difference to today's implementations are the following:
- Contract forms (
for safety
vsfor correctness
). More forms may be added later. rustc_contracts
prefix instead ofcontracts
.
Note that # 2 may not be a problem, per the initial PR. No matter what, we will still need to address # 1.
Activity