EXAMPLES.md

Example Usages

Integer Arithmetic with Overflow Checking

// Proven to never overflow
#[condition(pre="(x:i32 <= i32::MAX - 5:i32)", post="return:i32 == (x:i32 + 5:i32)")]
fn add_five(x:i32) -> i32 {
    assert!(x <= 2147483647-5);
    x+5
}

Boolean Conditional

// Proven to always return the NOT of the provided argument
#[condition(pre="true", post="(x:bool==true IMPLIES return:bool==false) && (x:bool==false IMPLIES return:bool==true)")]
fn boolean_not(x:bool) -> bool {
    if x == true {
        false
    } else {
        true
    }
}