可利安装错误

Question

我正在尝试在Ubuntu 16.04 LTS中安装klee （http://klee.github.io/build-llvm34/）。我有叮当声-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

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

Answer 2

如果有人仍在尝试在 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 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，我使用了以下命令。

1. 使用 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]
   

2. 居然通过奔跑make让克利.

3. 运行 Klee 测试用例以确保安装成功。