Function vstd::std_specs::num::ex_i32_checked_div

source ·

pub exec fn ex_i32_checked_div(lhs: i32, rhs: i32) -> result : Option<i32>

Expand description

ensures

rhs == 0 ==> result.is_None(),

({
    let x = lhs as int;
    let d = rhs as int;
    let output = if x == 0 {
        0
    } else if x > 0 && d > 0 {
        x / d
    } else if x < 0 && d < 0 {
        ((x * -1) / (d * -1))
    } else if x < 0 {
        ((x * -1) / d) * -1
    } else {
        (x / (d * -1)) * -1
    };
    if output < i32::MIN || output > i32::MAX {
        result.is_None()
    } else {
        result == Some(output as i32)
    }
}),