From fa061753c7dfc63dd1a9578d3863cb04b8538077 Mon Sep 17 00:00:00 2001 From: Per <Per Lindgren> Date: Sun, 25 Nov 2018 15:46:39 +0100 Subject: [PATCH] README --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 70f02d2..9f791cc 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ KLEE is a symbolic execution engine, based on the LLVM compiler infrastructure. KLEE generetes test cases aiming to cover (all) reachable paths of the input program. The KLEE run-time infers further checks for common program errors, e.g., out of bounds indexing and division by zero. Rust as being designed for safety, catches such errors and panics in precence of such faults. For analysis, a Rust `panic` implies an `abort`, which is detected as an error by KLEE, thus our `klee` tool spots potential panicing behavior of the application at hand. -In effect, the programmer may safely guide the Rust compiler to use unchecked operations (and thus improve the efficiency of the generated code), without jeopordizing memory safety and robustnes for programs. This holds in general for programs passing KLEE without panics, and in particular for operations checked by the KLEE run-time. In the latter case, unchecked operations can be fearlessly adopted, as it is sufficent to re-run KLEE if the source program is changed. To in the general case of adopting unchecked operations safety can be +In effect, the programmer may safely guide the Rust compiler to use unchecked operations (and thus improve the efficiency of the generated code), without jeopordizing memory safety and robustnes for programs. This holds in general for programs passing KLEE without panics, and in particular for operations checked by the KLEE run-time. In the latter case, unchecked operations can be fearlessly adopted, as it is sufficent to re-run KLEE if the source program is changed. In the general case of adopting unchecked operations safety can be ensured by adding assertions to the source. If those assertions are condititonally compiled (e.g. under a `klee` feature) the assertions (and their implied overhead) will be omitted in a production build. ## Requirements -- GitLab