|
1 |
| -KLEE Symbolic Virtual Machine |
| 1 | +KLEEF Symbolic Virtual Machine |
2 | 2 | =============================
|
3 | 3 |
|
4 |
| -[](https://github.com/klee/klee/actions?query=workflow%3ACI) |
5 |
| -[](https://cirrus-ci.com/github/klee/klee) |
6 |
| -[](https://codecov.io/gh/klee/klee) |
| 4 | +[](https://github.com/UnitTestBot/klee/actions?query=workflow%3ACI) |
| 5 | +[](https://codecov.io/gh/UnitTestBot/klee) |
7 | 6 |
|
8 |
| -`KLEE` is a symbolic virtual machine built on top of the LLVM compiler |
9 |
| -infrastructure. Currently, there are two primary components: |
10 | 7 |
|
11 |
| - 1. The core symbolic virtual machine engine; this is responsible for |
12 |
| - executing LLVM bitcode modules with support for symbolic |
13 |
| - values. This is comprised of the code in lib/. |
14 |
| - |
15 |
| - 2. A POSIX/Linux emulation layer oriented towards supporting uClibc, |
16 |
| - with additional support for making parts of the operating system |
17 |
| - environment symbolic. |
18 |
| - |
19 |
| -Additionally, there is a simple library for replaying computed inputs |
20 |
| -on native code (for closed programs). There is also a more complicated |
21 |
| -infrastructure for replaying the inputs generated for the POSIX/Linux |
22 |
| -emulation layer, which handles running native programs in an |
23 |
| -environment that matches a computed test input, including setting up |
24 |
| -files, pipes, environment variables, and passing command line |
25 |
| -arguments. |
26 |
| - |
27 |
| -For further information, see the [webpage](http://klee.github.io/). |
| 8 | +`KLEEF`` is a complete overhaul of the KLEE symbolic execution engine for LLVM, fine-tuned for a robust analysis of industrial C/C++ code. |
| 9 | +For further information, see the [webpage](https://toolchain-labs.com/projects/kleef.html). |
0 commit comments