// cargo klee --example registers --release

#![no_std]
#![no_main]

extern crate klee;
extern crate panic_abort;

extern crate volatile_register;
use volatile_register::RW;

// model RegC
// values always increases
// but are non-deterministic
struct RegC(RW<u32>);

static mut OLD_STATE: u32 = 0; // reset value, cannot be symbolic (awaiting const eval)
impl RegC {
    pub fn read(&self) -> u32 {
        let v = self.0.read(); // to get a symbolic value
        klee::kassume(v > 0); // to ensure that the value is positive
        unsafe {
            if (OLD_STATE as u64 + v as u64) < 0x1_0000_0000 {
                OLD_STATE += v
            }
            OLD_STATE
        }
    }

    pub unsafe fn write(&self, v: u32) {
        OLD_STATE = v;
    }
}

#[no_mangle]
fn main() {
    let reg_c: RegC = unsafe { core::mem::uninitialized() };
    let mut init: u32 = unsafe { core::mem::uninitialized() };
    klee::ksymbol!(&mut init, "init");
    unsafe {
        reg_c.write(init); // to ensure that the initial value is symbolic
    }

    let t1 = reg_c.read();
    // let t2 = reg_c.read();
    let c = 100 / (t1 - init);
    //     klee::kassert!(t2 > t1);
}