Select Git revision
model3.rs 1.14 KiB
// 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
impl RegC {
pub fn read(&self) -> u32 {
let v = self.0.read();
unsafe {
// klee::kassume(v - 0xFFFF_FFFC > 0);
// klee::kassume(v - OLD_STATE > 0);
// klee::kassert!(v > OLD_STATE);
klee::kassume(v > OLD_STATE);
OLD_STATE = v;
}
v
}
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");
//klee::kassume(init < 0xFFFF_FFFC);
//init = 0xFFFF_FFFD;
unsafe {
reg_c.write(init);
}
let t1 = reg_c.read();
let t2 = reg_c.read();
// let t3 = reg_c.read();
// let diff = 100 / (t2 - t1);
klee::kassert!(t2 > t1);
//klee::kassert!(t3 > t2);
//klee::kassert!(t3 > t1);
}