diff --git a/README.md b/README.md index 881e2ce3c801d9bb3d13191a3f09d1b4d6fb2a7c..889ab9a512314f6eee1f6963553f3c65cebef410 100644 --- a/README.md +++ b/README.md @@ -44,7 +44,7 @@ Example usage: LLVM KLEE strives to cover all feasible paths. When generating tests for errors encountered (paths to `abort`), KLEE will generate *one* test for each unique position in the source code that lead up to the `abort`. Code that emits a Rust `panic!()`, will all reach the same `panic_handler` (which calls into `abort`), and KLEE will detect the `panic_handler` as the source of the error, and consequently generate *one* such test. (Perhaps there is a way to force KLEE to generate one test per unique path leading up to the `panic_handler`, but we have not yet found it. Tech note: The `panic` implementation can unfortunately not be inlined as far as we have seen.) -As a consequence, you have to eleminate sources of `panic!()` one by one, which may be time consuming. +As a consequence, you have to eliminate sources of `panic!()` one by one, which may be time consuming. We provide a set of macros `klee_abort`, `klee_assert` and `klee_assert_eq`, that gets fully inlined, allowing KLEE to generate specific tests for each failing assertion. Using these, all errors will be covered by unique test.