0

我正在尝试在 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.
4

3 回答 3

2

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

于 2017-11-03T05:13:26.743 回答
0

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

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

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

于 2017-11-23T23:44:24.543 回答
0

在 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 测试用例以确保您的安装成功。

于 2018-04-18T19:05:25.350 回答