updated klee-examples

klee-examples/src/foo.rs

+//! 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)
 }

klee-examples/src/register.rs

 //! showcase volatile register
 //!
-//! $ cargo klee --bin register -r -g
+//! $ cargo klee --bin register -r -g -k
 //! ...
 //! Reading symbols from register.replay...done.
 //!