Attribute Macro creusot_contracts::macros::ensures

#[ensures]

A post-condition of a function or trait item

The inside of a ensures may look like Rust code, but it is in fact pearlite.

Example

#[ensures(result@ == 1)]
fn foo() -> i32 { 1 }