Attribute Macro contracts::post

#[post]

Post-conditions are checked after the function body is run.

The result of the function call is accessible in conditions using the ret identifier.

Example

#[post(ret > x)]
fn incr(x: usize) -> usize {
    x + 1
}