model.rs

// cargo klee --example registers --release

#![no_std]
#![no_main]

extern crate klee;
extern crate panic_abort;

extern crate volatile_register;
use volatile_register::RW;

struct Device<'a> {
  ptr: &'a RW<u32>,
}

// HW model.
// The register holds values 0..31
impl<'a> Device<'a> {
  pub fn read(&self) -> u32 {
    let v = self.ptr.read();
    klee::kassume(v < 32);
    v
  }
  pub unsafe fn write(
    &self,
    v: u32,
  ) {
    klee::kassert!(v < 32);
    let v = self.ptr.write(v);
  }
}

#[no_mangle]
fn main() {
  let reg = unsafe { core::mem::uninitialized() };
  let device = Device { ptr: &reg };

  let v = device.read();
  if v > 5 {
    unsafe {
      device.write(v - 1);
    }
    if device.read() == v - 1 {
      panic!();
    }
  }
}