README

README.md

@@ -18,6 +18,10 @@ the master branch of KLEE (https://github.com/klee/klee) as of Sun Nov 25 14:57:
 
 Currently only native KLEE is supported, we need to build a new docker with recent KLEE first in order to re-enable docker usage.
 
+A Rust `no_std` application under linux will use the target triple `x86_64-unknown-linux-gnu` while KLEE uses the target triple `x86_64-pc-linux-gnu`, which renders a KLEE warning. To the best of our understanding both refers to the same (ABI) and thus the warning can be safely ignored.
+
+If the code under analysis is targeting another architecture (e.g., with other byte order or pointer size) the KLEE run-time system should be compiled for the target architecture to ensure complience in between analysis and production code behavior. An ergonomic way of re-targeting KLEE has yet not been investigated. (This is not a Rust `klee` issue per-se, but rather a possible feature for further KLEE development.)
+
 ## usage
 
 ``` console
@@ -105,4 +109,13 @@ fn f1(u: u8) -> u8 {
 fn f2(u: u8) -> u8 {
     100 / u // <- Rust div 0 panic! 
 }
-```
+```
\ No newline at end of file
+
+The application is compiled for `#[no_std]` (thus isolating the application to dependencies of the environment). `extern crate klee` gives us access to the `klee` bindings. `ksymbol` marks the variable `u` as symbolic (unknown). `read_volatile(&T)` ensures that `T` is computed (and thus prevents the corresesponding code from being optimized out by the compiler).
+
+## Examples
+
+Further examples is found in the `klee-examples` directory.
+
+- `foo`, shows the above example.
+- `foo2`, shows further use of `ksymbol!(&mut T, &str)` for making declared variables symbolic.
\ No newline at end of file