From 85ddad0ceebc705dfdb3d894bedc86ce6f433d2d Mon Sep 17 00:00:00 2001 From: Per <Per Lindgren> Date: Sun, 25 Nov 2018 16:28:39 +0100 Subject: [PATCH] README --- README.md | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 60873c8..fc0364a 100644 --- a/README.md +++ b/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 -- GitLab