diff --git a/klee-examples/src/foo.rs b/klee-examples/src/foo.rs index a86342d1a0c22d2c61e14915e621a19ee2c9b588..ecff76d42d430e39c87c2602ce67f34e9745f5d1 100644 --- a/klee-examples/src/foo.rs +++ b/klee-examples/src/foo.rs @@ -1,3 +1,35 @@ +//! Showcase how individual fields can be made symbolic +//! $ cargo klee --bin foo --release -r -k -g -v +//! ... +//! 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/debug/deps/foo.replay +//! [Inferior 1 (process 25074) exited with code 01] +//! +//! (gdb) set env KTEST_FILE=klee-last/test000002.ktest +//! (gdb) run +//! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/debug/deps/foo.replay +//! +//! Program received signal SIGILL, Illegal instruction. +//! rust_begin_unwind (_info=0x7fffffffd6a8) +//! at /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31 +//! 31 unsafe { intrinsics::abort() } +//! (gdb) backtrace +//! #0 rust_begin_unwind (_info=0x7fffffffd6a8) +//! at /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31 +//! #1 0x000055555555530c in core::panicking::panic_fmt () +//! at src/libcore/panicking.rs:85 +//! #2 0x000055555555538b in core::panicking::panic () at src/libcore/panicking.rs:49 +//! #3 0x0000555555555281 in foo::f2 (u=0) at src/foo.rs:60 +//! #4 0x0000555555555234 in main () at src/foo.rs:51 +//! (gdb) frame 4 +//! #4 0x0000555555555234 in main () at src/foo.rs:51 +//! 46 let _ = f2(f1(u.a)); +//! (gdb) print u +//! $1 = foo::A {a: 255, b: 7} + #![no_std] #![no_main] @@ -5,8 +37,6 @@ extern crate klee; extern crate panic_abort; -use core::ptr; - struct A { a: u8, b: u32, @@ -17,13 +47,11 @@ fn main() { let mut a = 0; ksymbol!(&mut a, "a"); let mut u = A { a: a, b: 0 }; - - unsafe { - ptr::read_volatile(&f2(f1(u.a))); - } + u.b = 7; + let _ = f2(f1(u.a)); } -// add 1 wrapping +// add 1 wrapping instead of panic fn f1(u: u8) -> u8 { u.wrapping_add(1) } diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs index 3df905db95b2afa490d7009cefcd1adf30e3917e..8024b4efb2051a372e4afcc15bf0db0c789d7098 100644 --- a/klee-examples/src/register.rs +++ b/klee-examples/src/register.rs @@ -1,6 +1,6 @@ //! showcase volatile register //! -//! $ cargo klee --bin register -r -g +//! $ cargo klee --bin register -r -g -k //! ... //! Reading symbols from register.replay...done. //!