Function bitwise_or

src/tcb/misc.rs:114–116

(bv1: i32, bv2: i32)

// #[with_ghost_var(trace: &mut Trace)]
#[ensures(result >= bv1 && result >= bv2)]
pub fn bitwise_or(bv1: i32, bv2: i32) -> i32 {
    bv1 | bv2
}

#[trusted]
pub fn bitwise_or_u32(bv1: u32, bv2: u32) -> u32 {