foo.rs

//! Showcase how individual fields can be made symbolic
//! $ cargo klee --bin foo -r -k -g -v
//! ...
//! Reading symbols from register.replay...done.
//!
//! (gdb) set env KTEST_FILE=klee-last/test000001.ktest
//! (gdb) run # for the generated test the program will run to end
//! 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 # for the generated test the program will panic du to a division by zero, line 60
//! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/debug/deps/foo.replay 
//! 
//! Program received signal SIGILL, Illegal instruction.
//! rust_begin_unwind (_info=0x7fffffffd9b8) 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=0x7fffffffd9b8) 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
//! 51          let _ = f2(f1(u.a));
//! 
//! //! (gdb) print u
//! $1 = foo::A {a: 255, b: 7}

#![no_std]
#![no_main]

#[macro_use]
extern crate klee;
extern crate panic_abort;

struct A {
    a: u8,
    b: u32,
}

#[no_mangle]
fn main() {
    let mut a = 0;
    ksymbol!(&mut a, "a");
    let mut u = A { a: a, b: 0 };
    u.b = 7;
    let _ = f2(f1(u.a));
}

// add 1 wrapping instead of panic
fn f1(u: u8) -> u8 {
    u.wrapping_add(1)
}

fn f2(u: u8) -> u8 {
    100 / u
}