assume.rs

// cargo klee --example registers --release

#![no_std]
#![no_main]

extern crate klee;
extern crate panic_abort;

#[no_mangle]
fn main() {
    let mut a: u32 = 0;
    let mut b: u32 = 0;

    klee::ksymbol!(&mut a, "a");
    klee::ksymbol!(&mut b, "b");

    let mut c = 0;
    if a > 10 {
        c+= 1;
    }
    // klee::kassume(b > 0);
    let v = a + b;

    unsafe {
        core::ptr::read_volatile(&a);
        core::ptr::read_volatile(&b);
        core::ptr::read_volatile(&v);
        core::ptr::read_volatile(&c);
    }
}