Klee安装错误

Question

我试图在Ubuntu16.04LTS中安装klee (http://klee.github.io/build-llvm34/)。我吃的是嘎吱声-3.9。在klee_build_dir中执行下面的命令后，我有带有ktest和ktest-tool的bin目录，但没有klee。请帮帮忙

cmake -DENABLE_SOLVER_Z3=ON -DENABLE_SOLVER_STP=OFF -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DENABLE_UNIT_TESTS=OFF -DENABLE_SYSTEM_TESTS=OFF -DKLEE_UCLIBC_PATH=/home/balaji/Downloads/klee-uclibc /home/balaji/Downloads/klee-- The CXX compiler identification is GNU 5.4.0
-- The C compiler identification is GNU 5.4.0
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- KLEE version 1.4.0.0
-- CMake generator: Unix Makefiles
-- CMAKE_BUILD_TYPE is not set. Setting default
-- The available build types are: Debug;Release;RelWithDebInfo;MinSizeRel
-- Build type: RelWithDebInfo
-- KLEE assertions enabled
-- LLVM_CONFIG_BINARY: /usr/bin/llvm-config
-- LLVM_PACKAGE_VERSION: "3.8.0"
-- LLVM_VERSION_MAJOR: "3"
-- LLVM_VERSION_MINOR: "8"
-- LLVM_VERSION_PATCH: "0"
-- LLVM_DEFINITIONS: "-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS"
-- LLVM_ENABLE_ASSERTIONS: "OFF"
-- LLVM_ENABLE_EH: "OFF"
-- LLVM_ENABLE_RTTI: "ON"
-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-3.8/include"
-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-3.8/lib"
-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-3.8/bin"
-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "ON"
-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"
CMake Warning at CMakeLists.txt:237 (message):
  LLVM was built without assertions but KLEE will be built with them.

  This might lead to unexpected behaviour.

Answer 1

如果有人仍然试图在Ubuntu 14上安装KLEE，您可以在下面的链接中使用我的虚拟机：

Github链接：https://github.com/balajibalasubramaniam/dig

该虚拟机最重要的特点是它预先安装了SAGE (免费开源数学软件系统)、Z3 ( Microsoft的定理证明器)、KLEE(建立在LLVM编译器基础之上的符号虚拟机)、Java、JPF(验证可执行Java字节码程序的系统)和Junit。最重要的是，它包括DIG或SymInfer --一种使用从C和Java程序的符号执行工具中提取的符号状态生成数值不变量的最新工具(请访问https://bitbucket.org/nguyenthanhvuh/symtraces/wiki/Home了解更多信息)。

Answer 2

欢迎您使用我的GitHub库，它使用6个简单脚本在Ubuntu14.04.5LTS上安装KLEE。我喜欢Ubuntu14.04而不是Ubuntu16.04的原因是他们附带的默认GCC版本。请注意，第6个脚本使用需要更改的绝对路径(从/home/oren/GIT/到/home/YourUserName/Some/Dirname). )。我还包含了一个调用KLEE并使用一些简单的input.c文件检查安装的第7个脚本。祝好运!

Answer 3

在(http://klee.github.io/build-llvm34/)中，他们指出您需要使用llvm-3.4。这意味着您需要安装llvm-3.4，然后使用clang-3.4/clang++-3.4作为编译器。

要安装llvm-3.4，可以运行：

sudo apt-get update
sudo apt-get install clang-3.4 llvm-3.4 llvm-3.4-dev llvm-3.4-tools

为了编译klee，我使用了以下命令。

1. 使用cmake进行配置。您需要知道您的llvm-3.4二进制文件在哪里。 cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON\ _ -DENABLE_KLEE_UCLIBC=ON _-DENABLE_KLEE_UCLIBC=ON_-DENABLE_KLEE_UCLIBC=ON=/usr/bin/llvm-config-3.4-DLLVMCC=/usr/bin/clang-3.4\ -DLLVMCC=/usr/bin/clang-3.4 -DLLVMCXX=/usr/bin/clang++-3.4
2. 实际上，通过运行make来制造Klee。
3. 运行Klee测试用例以确保安装成功。