Skip to content
Snippets Groups Projects
Select Git revision
  • 11b7935d666af75fd3325da137279ac9a7a5141c
  • master default protected
  • home_exam
  • wip
4 results

parse.rs

Blame
  • Forked from Per Lindgren / D7050E
    Source project has a limited visibility.
    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);
    }