Klee安装错误

Question

我正在尝试在 Ubuntu 16.04 LTS 中安装 klee (http://klee.github.io/build-llvm34/)。我有 clang-3.9。在 klee_build_dir 中执行以下命令后，我有带有 klee-stats 和 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

欢迎您使用 my GitHub repository，它使用 6 个简单的脚本在 UBUNTU 14.04.5 LTS[= 上安装 KLEE 17=]。我更喜欢 UBUNTU 14.04 而不是 UBUNTU 16.04 的原因是它们附带的默认 GCC 版本。请注意，第 6 个脚本使用了您需要更改的绝对路径（从 /home/oren/GIT/ 到 /home/YourUserName/Some/Dirname）。我还包含了第 7 个脚本，它调用 KLEE 并使用一些简单的 input.c 文件检查安装。祝你好运！

Answer 2

如果有人还在尝试在 Ubuntu 14 上安装 KLEE，您可以在以下 link:

使用我的虚拟机

Github link: https://github.com/balajibalasubramaniam/dig

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

Answer 3

在KLEE安装指南(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，我使用了以下命令。

使用 cmake 进行配置。你需要知道你的 llvm-3.4 二进制文件在哪里。

cmake -DENABLE_SOLVER_STP=ON   -DENABLE_POSIX_RUNTIME=ON\
      -DENABLE_KLEE_UCLIBC=ON   -DKLEE_UCLIBC_PATH=[klee-uclibc-repository] \ 
      -DGTEST_SRC_DIR=/[google-release-repository] \ 
      -DENABLE_SYSTEM_TESTS=ON   -DENABLE_UNIT_TESTS=ON \ 
      -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-3.4 -DLLVMCC=/usr/bin/clang-3.4 \ 
      -DLLVMCXX=/usr/bin/clang++-3.4 [your-klee-repository]

实际上运行 make.
运行 Klee 测试用例以确保您的安装成功。

Klee安装错误

Klee installation error

klee