diff --git a/CHANGELOG.md b/CHANGELOG.md index 1a99ad6b904839938ab080b2c4afbd4c9a69ddfa..b84b8bff335a825e8c81d921df8766a2cb29af9f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,4 +2,6 @@ Most recent changes: +- 2020-12-08 Update `README.md` for Ubuntu (like) system with `z3` dependency. + - 2020-12-08 Update `README.md` and `examples/get_sign` to reflect the recent `klee 2.2` and `aur` package. \ No newline at end of file diff --git a/README.md b/README.md index 714b20927b30b2ddddfe9fa2aec846035170b226..eafe78bde1d5cbd51e2eb3aa00dfc4a20d87a01f 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# Klee tutorial +# KLEE tutorial Installing and testing klee. @@ -10,18 +10,25 @@ Under the hood, klee uses a `sat` solver for First Order Logic (FOL). Klee can i So first install `z3` on your system (then klee will use that instead of the default solver). +Later, you also need to have `gdb` installed, under arch by: + +### Arch linux: + Under arch with `yay` installed simply: ```shell > yay -S z3 ``` -Later, you also need to have `gdb` installed, under arch by: - ```shell > yay -S gdb ``` +### Ubuntu (like) systems + +> sudo apt install z3 libz3-4 libz3-cil libz3-dev libz3-java libz3-jni libz3-ocaml-de + + ## Install KLEE from source The instructions recommend LLVM 9, but the current master (2.2-pre) supports LLVM 11 (which is what you would have under arch as of 2020-12-07).