Skip to content

Don't wrap body in a closure unless we need to check postconditions

In current versions of contracts, annotating code using lifetime elision on mutable references will cause it to stop compiling. This is somewhat related to #11.

#[requires(i < s.len())] // ERROR
fn idx(s: &mut [u8], i: usize) -> &mut u8 {
    &mut s[i]
}

This issue is hard (though not impossible) to solve when the user specifies a postcondition with ensures or invariant, but we can sidestep it entirely when only preconditions are needed.

Edited by Dylan MacKenzie

Merge request reports

Loading