register.rs

//! showcase volatile register
//!
//! $ cargo klee --bin register -r -g
//! ...
//! Reading symbols from register.replay...done.
//!
//! (gdb) set env KTEST_FILE=klee-last/test000001.ktest
//! (gdb) run
//! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/release/deps/main2.replay
//! [Inferior 1 (process 25074) exited with code 01]
//!
//! (gdb) set env KTEST_FILE=klee-last/test000003.ktest
//! (gdb) run
//! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/release/deps/main2.replay
//! rust_begin_unwind (_info=0x7fffffffd678)
//!    at /home/pln/.cargo/git/checkouts/cargo-klee-8f30fda3bd23bb30/68dc73d/src/lang_items.rs:66
//!            unsafe { intrinsics::abort() }
//! (gdb) backtrace
//! #0  rust_begin_unwind (_info=0x7fffffffd678)
//!    at /home/pln/.cargo/git/checkouts/cargo-klee-8f30fda3bd23bb30/68dc73d/src/lang_items.rs:6
//! #1  0x000055555555531c in core::panicking::panic_fmt () at src/libcore/panicking.rs:95
//! #2  0x000055555555539b in core::panicking::panic () at src/libcore/panicking.rs:59
//! #3  0x00005555555552a6 in main () at src/main2.rs:54
//! (gdb) q
//! A debugging session is active.
//!
//!        Inferior 1 [process 25893] will be killed.
//! $ ktest-tool --write-int target/debug/deps/klee-last/test000003.ktest
//! ktest file : 'target/debug/deps/klee-last/test000003.ktest'
//! args       : ['/home/pln/rust/cargo-klee/klee-examples/target/debug/deps/main2-2a0fc03ce12ab528.ll']
//! num objects: 2
//! object    0: name: b'register'
//! object    0: size: 4
//! object    0: data: 0
//! object    1: name: b'register'
//! object    1: size: 4
//! object    1: data: 0

#![no_std]
#![no_main]

extern crate klee;
extern crate panic_abort;

extern crate volatile_register;
use volatile_register::RO;

#[no_mangle]
fn main() {
    let rw: RO<u32> = unsafe { core::mem::uninitialized() };

    if rw.read() == 0 {
        if rw.read() == 0 {
            klee::abort();
        }
    }
}