llvm-gcc --emit-llvm -c tr.c -o tr.bc

klee --max-time 2 --sym-args 1 10 10--sym-files 2 2000 --max-fail 1 tr.bc

示例程序1 : void expand(char *arg, unsigned char *buffer) { 82 : int i, ac; 93 : while (*arg) { 10*4 : if (*arg == ’\’) { 11*5 : arg++;6 : i = ac = 0;7 : if (*arg >= ’0’ && *arg <= ’7’) {8 : do {9 : ac = (ac << 3) + *arg++ − ’0’;10: i++;11: } while (i<4 && *arg>=’0’ && *arg<=’7’);12: *buffer++ = ac;13: } else if (*arg != ’’)14: *buffer++ = *arg++;15: } else if (*arg == ’[’) { 12*16: arg++; 1317: i = *arg++; 1418: if (*arg++ != ’-’) { 15!19: *buffer++ = ’[’;20: arg −= 2;21: continue;22: }23: ac = *arg++;24: while (i <= ac) *buffer++ = i++;25: arg++; /* Skip ’]’ */26: } else27: *buffer++ = *arg++;28: }29: }30: . . .31: int main(int argc, char* argv[ ]) { 132: int index = 1; 233: if (argc > 1 && argv[index][0] == ’-’) { 3*34: . . . 435: } 536: . . . 637: expand(argv[index++], index); 738: . . .39: }

klee --max-time 2 --sym-args 1 10 10--sym-files 2 2000 --max-fail 1 tr.bc

[ "" ""

%dst = add i32 %src0, %src1

x+0改成x,x*2^n改成x<<n2*x-x改成x

x<10

x=5

x+1=10

{i<10，i-10}(没有解) {i<10，j=8}(有解，例如当分配i=5,j=8)

{i < 10, i = 10, j = 12}（依然是无解的）

i→5，j→8分别是i<10或j=8的解

约束集{i<10，j=8，i！=3}的解还是i→5，j→8。

sudo apt-get install build-essential curl libcap-dev git cmake libncurses5-dev python-minimal python-pip unzip libtcmalloc-minimal4 libgoogle-perftools-dev libsqlite3-dev doxygen

sudo apt-get install python3 python3-pip gcc-multilib g++-multilib

bigeast@ubuntu:~$ locate pip3/usr/local/lib/python3.6/dist-packages/bin/pip3/usr/local/lib/python3.6/dist-packages/bin/pip3.6/usr/share/man/man1/pip3.1.gz

sudo ln -s /usr/local/lib/python3.6/dist-packages/bin/pip3.6 /usr/local/bin/pip3

pip3 install lit tabulate wllvm

sudo apt-get install clang-9 llvm-9 llvm-9-dev llvm-9-tools

git clone https://github.com/Z3Prover/z3.gitcd z3/python scripts/mk_make.pysudo make install

bigeast@ubuntu:~$ git clone https://github.com/klee/klee-uclibc.gitbigeast@ubuntu:~$ cd klee-uclibcbigeast@ubuntu:~/klee-uclibc$ ./configure --make-llvm-libINFO:Disabling assertionsINFO:Configuring for Debug buildINFO:Configuring for LLVM bitcode archiveINFO:Using llvm-config at...NoneERROR:llvm-config cannot be found

./configure --make-llvm-lib --with-llvm-config /usr/bin/llvm-config-9

curl -OL https://github.com/google/googletest/archive/release-1.7.0.zipunzip release-1.7.0.zip

sudo add-apt-repository ppa:ubuntu-toolchain-r/testsudo apt-get updatesudo apt-get install gcc-9 g++-9

bigeast@ubuntu:~/klee-2.1$ sudo LLVM_VERSION=9 SANITIZER_BUILD= BASE=/usr/include/c++/9 REQUIRES_RTTI=1 DISABLE_ASSERTIONS=1 ENABLE_DEBUG=0 ENABLE_OPTIMIZED=1 ./scripts/build/build.sh libcxx

Detected OS: linuxOS=linuxDetected distribution: ubuntuDISTRIBUTION=ubuntuDetected version: 18.04DISTRIBUTION_VER=18.04Component sanitizer not found.Component sanitizer not found.Already installed llvm/usr/bin/llvm-config-9Already installed clangCMake Error at /usr/share/cmake-3.10/Modules/CMakeDetermineCCompiler.cmake:48 (message):  Could not find compiler set in environment variable CC:   wllvm.Call Stack (most recent call first):  CMakeLists.txt:49 (project)  CMake Error: CMAKE_C_COMPILER not set, after EnableLanguageCMake Error: CMAKE_CXX_COMPILER not set, after EnableLanguageCMake Error: CMAKE_ASM_COMPILER not set, after EnableLanguage-- Configuring incomplete, errors occurred!See also "/usr/include/c++/9/libc++-build-9/CMakeFiles/CMakeOutput.log".make: *** No rule to make target 'cxx'.  Stop.

bigeast@ubuntu:~/klee-2.1$ sudo -H python3 -m pip install wllvm

mkdir buildcd buildcmake -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DENABLE_KLEE_LIBCXX=ON -DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-90/ -DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-90/include/c++/v1/ -DENABLE_KLEE_EH_CXX=ON -DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/llvm-90/libcxxabi/ -DKLEE_UCLIBC_PATH=/home/bigeast/klee-uclibc/ -DENABLE_UNIT_TESTS=ON -DENABLE_SYSTEM_TESTS=ON -DGTEST_SRC_DIR=/home/bigeast/googletest-release-1.7.0/  -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9 -DLLVMCC=/usr/bin/clang-9 -DLLVMCXX=/usr/bin/clang++-9 -DCMAKE_C_COMPILER=clang  -DCMAKE_CXX_COMPILER=clang++  ..

bigeast@ubuntu:~/klee-2.1/build$ cmake -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DENABLE_KLEE_LIBCXX=ON -DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-90/ -DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-90/include/c++/v1/ -DENABLE_KLEE_EH_CXX=ON -DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/llvm-90/libcxxabi/ -DKLEE_UCLIBC_PATH=/home/bigeast/klee-uclibc/ -DENABLE_UNIT_TESTS=ON -DENABLE_SYSTEM_TESTS=ON -DGTEST_SRC_DIR=/home/bigeast/googletest-release-1.7.0/  -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9 -DLLVMCC=/usr/bin/clang-9 -DLLVMCXX=/usr/bin/clang++-9 -DCMAKE_C_COMPILER=clang  -DCMAKE_CXX_COMPILER=clang++  ..-- The CXX compiler identification is unknown-- The C compiler identification is unknownCMake Error at CMakeLists.txt:43 (project):  The CMAKE_CXX_COMPILER:     clang++   is not a full path and was not found in the PATH.   Tell CMake where to find the compiler by setting either the environment  variable "CXX" or the CMake cache entry CMAKE_CXX_COMPILER to the full path  to the compiler, or to the compiler name if it is in the PATH.  CMake Error at cmake/cxx_flags_override.cmake:24 (message):  Overrides not set for compilerCall Stack (most recent call first):  /usr/share/cmake-3.10/Modules/CMakeCXXInformation.cmake:89 (include)  CMakeLists.txt:43 (project)  CMake Error at CMakeLists.txt:43 (project):  The CMAKE_C_COMPILER:     clang   is not a full path and was not found in the PATH.   Tell CMake where to find the compiler by setting either the environment  variable "CC" or the CMake cache entry CMAKE_C_COMPILER to the full path to  the compiler, or to the compiler name if it is in the PATH.  -- Configuring incomplete, errors occurred!See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeOutput.log".See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeError.log".

bigeast@ubuntu:~/klee-2.1/build$ cmake -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DENABLE_KLEE_LIBCXX=ON -DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-90/ -DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-90/include/c++/v1/ -DENABLE_KLEE_EH_CXX=ON -DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/llvm-90/libcxxabi/ -DKLEE_UCLIBC_PATH=/home/bigeast/klee-uclibc/ -DENABLE_UNIT_TESTS=ON -DENABLE_SYSTEM_TESTS=ON -DGTEST_SRC_DIR=/home/bigeast/googletest-release-1.7.0/  -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9 -DLLVMCC=/usr/bin/clang-9 -DLLVMCXX=/usr/bin/clang++-9 -DCMAKE_C_COMPILER=clang-9  -DCMAKE_CXX_COMPILER=clang++-9  ..-- The CXX compiler identification is Clang 9.0.0-- The C compiler identification is Clang 9.0.0-- Check for working CXX compiler: /usr/bin/clang++-9-- Check for working CXX compiler: /usr/bin/clang++-9 -- 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/clang-9-- Check for working C compiler: /usr/bin/clang-9 -- works-- Detecting C compiler ABI info-- Detecting C compiler ABI info - done-- Detecting C compile features-- Detecting C compile features - done-- KLEE version 2.1-- 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-9-- LLVM_PACKAGE_VERSION: "9.0.0"-- LLVM_VERSION_MAJOR: "9"-- LLVM_VERSION_MINOR: "0"-- LLVM_VERSION_PATCH: "0"-- LLVM_DEFINITIONS: "-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS"-- LLVM_ENABLE_ASSERTIONS: "ON"-- LLVM_ENABLE_EH: "OFF"-- LLVM_ENABLE_RTTI: "ON"-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-9/include"-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-9/lib"-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-9/bin"-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "OFF"-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"-- LLVM_BUILD_MAIN_SRC_DIR: "/usr/lib/llvm-9/build/"-- Looking for bitcode compilers-- Found /usr/bin/clang-9-- Found /usr/bin/clang++-9-- Testing bitcode compiler /usr/bin/clang-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang-9" is compatible-- Testing bitcode compiler /usr/bin/clang++-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang++-9" is compatible-- LLVMCC: /usr/bin/clang-9-- LLVMCXX: /usr/bin/clang++-9-- Performing Test HAS__Wall_CXX-- Performing Test HAS__Wall_CXX - Success-- C++ compiler supports -Wall-- Performing Test HAS__Wextra_CXX-- Performing Test HAS__Wextra_CXX - Success-- C++ compiler supports -Wextra-- Performing Test HAS__Wno_unused_parameter_CXX-- Performing Test HAS__Wno_unused_parameter_CXX - Success-- C++ compiler supports -Wno-unused-parameter-- Performing Test HAS__Wall_C-- Performing Test HAS__Wall_C - Success-- C compiler supports -Wall-- Performing Test HAS__Wextra_C-- Performing Test HAS__Wextra_C - Success-- C compiler supports -Wextra-- Performing Test HAS__Wno_unused_parameter_C-- Performing Test HAS__Wno_unused_parameter_C - Success-- C compiler supports -Wno-unused-parameter-- Not treating compiler warnings as errors-- Could NOT find STP (missing: STP_DIR)-- STP solver support disabled-- Found Z3 libraries: "/usr/lib/libz3.so"-- Found Z3 include path: "/usr/include"-- Found Z3: /usr/include -- Z3 solver support enabled-- Found Z3-- Checking prototype Z3_get_error_msg for HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT - True-- Z3_get_error_msg requires context-- metaSMT solver support disabled-- Performing Test HAS__fno_exceptions-- Performing Test HAS__fno_exceptions - Success-- C++ compiler supports -fno-exceptions-- Found ZLIB: /usr/lib/x86_64-linux-gnu/libz.so (found version "1.2.11")-- Zlib support enabled-- TCMalloc support enabled-- Looking for C++ include gperftools/malloc_extension.h-- Looking for C++ include gperftools/malloc_extension.h - not foundCMake Error at CMakeLists.txt:419 (message):  Can't find "gperftools/malloc_extension.h"  -- Configuring incomplete, errors occurred!See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeOutput.log".See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeError.log".

sudo apt-get install libtcmalloc-minimal4 libgoogle-perftools-dev

bigeast@ubuntu:~/klee-2.1/build$ cmake > -DENABLE_POSIX_RUNTIME=ON > -DENABLE_KLEE_UCLIBC=ON > -DENABLE_KLEE_LIBCXX=ON > -DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-90/ > -DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-90/include/c++/v1/ > -DENABLE_KLEE_EH_CXX=ON > -DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/llvm-90/libcxxabi/ > -DKLEE_UCLIBC_PATH=/home/bigeast/klee-uclibc/ > -DENABLE_UNIT_TESTS=ON > -DENABLE_SYSTEM_TESTS=ON > -DGTEST_SRC_DIR=/home/bigeast/googletest-release-1.7.0/  > -DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-9 > -DLLVMCC=/usr/bin/clang-9 > -DLLVMCXX=/usr/bin/clang++-9 > -DCMAKE_C_COMPILER=clang-9  > -DCMAKE_CXX_COMPILER=clang++-9  > ..-- KLEE version 2.1-- CMake generator: Unix Makefiles-- Build type: RelWithDebInfo-- KLEE assertions enabled-- LLVM_CONFIG_BINARY: /usr/bin/llvm-config-9-- LLVM_PACKAGE_VERSION: "9.0.0"-- LLVM_VERSION_MAJOR: "9"-- LLVM_VERSION_MINOR: "0"-- LLVM_VERSION_PATCH: "0"-- LLVM_DEFINITIONS: "-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS"-- LLVM_ENABLE_ASSERTIONS: "ON"-- LLVM_ENABLE_EH: "OFF"-- LLVM_ENABLE_RTTI: "ON"-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-9/include"-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-9/lib"-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-9/bin"-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "OFF"-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"-- LLVM_BUILD_MAIN_SRC_DIR: "/usr/lib/llvm-9/build/"-- Looking for bitcode compilers-- Found /usr/bin/clang-9-- Found /usr/bin/clang++-9-- Testing bitcode compiler /usr/bin/clang-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang-9" is compatible-- Testing bitcode compiler /usr/bin/clang++-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang++-9" is compatible-- LLVMCC: /usr/bin/clang-9-- LLVMCXX: /usr/bin/clang++-9-- C++ compiler supports -Wall-- C++ compiler supports -Wextra-- C++ compiler supports -Wno-unused-parameter-- C compiler supports -Wall-- C compiler supports -Wextra-- C compiler supports -Wno-unused-parameter-- Not treating compiler warnings as errors-- Could NOT find STP (missing: STP_DIR)-- STP solver support disabled-- Found Z3 libraries: "/usr/lib/libz3.so"-- Found Z3 include path: "/usr/include"-- Z3 solver support enabled-- Found Z3-- Z3_get_error_msg requires context-- metaSMT solver support disabled-- C++ compiler supports -fno-exceptions-- Zlib support enabled-- TCMalloc support disabled-- Could NOT find SQLITE3 (missing: SQLITE3_LIBRARY SQLITE3_INCLUDE_DIR)CMake Error at CMakeLists.txt:434 (message):  SQLite3 not found, please install  -- Configuring incomplete, errors occurred!See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeOutput.log".See also "/home/bigeast/klee-2.1/build/CMakeFiles/CMakeError.log".

sudo apt-get install sqlite3 libsqlite3-dev

-- KLEE version 2.1-- CMake generator: Unix Makefiles-- Build type: RelWithDebInfo-- KLEE assertions enabled-- LLVM_CONFIG_BINARY: /usr/bin/llvm-config-9-- LLVM_PACKAGE_VERSION: "9.0.0"-- LLVM_VERSION_MAJOR: "9"-- LLVM_VERSION_MINOR: "0"-- LLVM_VERSION_PATCH: "0"-- LLVM_DEFINITIONS: "-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS"-- LLVM_ENABLE_ASSERTIONS: "ON"-- LLVM_ENABLE_EH: "OFF"-- LLVM_ENABLE_RTTI: "ON"-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-9/include"-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-9/lib"-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-9/bin"-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "OFF"-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"-- LLVM_BUILD_MAIN_SRC_DIR: "/usr/lib/llvm-9/build/"-- Looking for bitcode compilers-- Found /usr/bin/clang-9-- Found /usr/bin/clang++-9-- Testing bitcode compiler /usr/bin/clang-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang-9" is compatible-- Testing bitcode compiler /usr/bin/clang++-9-- Compile success-- Checking compatibility with LLVM 9.0.0-- "/usr/bin/clang++-9" is compatible-- LLVMCC: /usr/bin/clang-9-- LLVMCXX: /usr/bin/clang++-9-- C++ compiler supports -Wall-- C++ compiler supports -Wextra-- C++ compiler supports -Wno-unused-parameter-- C compiler supports -Wall-- C compiler supports -Wextra-- C compiler supports -Wno-unused-parameter-- Not treating compiler warnings as errors-- Could NOT find STP (missing: STP_DIR)-- STP solver support disabled-- Found Z3 libraries: "/usr/lib/libz3.so"-- Found Z3 include path: "/usr/include"-- Z3 solver support enabled-- Found Z3-- Z3_get_error_msg requires context-- metaSMT solver support disabled-- C++ compiler supports -fno-exceptions-- Zlib support enabled-- TCMalloc support disabled-- SELinux support disabled-- Workaround for LLVM PR39177 (affecting LLVM 3.9 - 7.0.0) disabled-- KLEE_RUNTIME_BUILD_TYPE: Debug+Asserts-- POSIX runtime enabled-- klee-uclibc support enabled-- Found klee-uclibc library: "/home/bigeast/klee-uclibc/lib/libc.a"-- klee-libcxx support enabled-- Use libc++ include path: "/usr/include/c++/9/libc++-install-9/include/c++/v1/"-- Found libc++ library: "/usr/include/c++/9/libc++-install-9/lib/libc++.bca"-- CMAKE_CXX_FLAGS:  -Wall -Wextra -Wno-unused-parameter-- KLEE_COMPONENT_EXTRA_INCLUDE_DIRS: '/usr/lib/llvm-9/include;/usr/include;/usr/include'-- KLEE_COMPONENT_CXX_DEFINES: '-D_GNU_SOURCE;-D__STDC_CONSTANT_MACROS;-D__STDC_FORMAT_MACROS;-D__STDC_LIMIT_MACROS;-DKLEE_UCLIBC_BCA_NAME="klee-uclibc.bca";-DKLEE_LIBCXX_BC_NAME="libc++.bca"'-- KLEE_COMPONENT_CXX_FLAGS: '-fno-exceptions'-- KLEE_COMPONENT_EXTRA_LIBRARIES: '/usr/lib/x86_64-linux-gnu/libz.so'-- KLEE_SOLVER_LIBRARIES: '/usr/lib/libz3.so'-- Testing is enabled-- Using lit: /home/bigeast/.local/bin/lit-- Unit tests enabled-- Google Test: Building from source.-- GTEST_SRC_DIR: /home/bigeast/googletest-release-1.7.0/-- Found PythonInterp: /usr/bin/python (found version "2.7.17")-- Looking for pthread.h-- Looking for pthread.h - found-- Looking for pthread_create-- Looking for pthread_create - not found-- Looking for pthread_create in pthreads-- Looking for pthread_create in pthreads - not found-- Looking for pthread_create in pthread-- Looking for pthread_create in pthread - found-- Found Threads: TRUE -- GTEST_INCLUDE_DIR: /home/bigeast/googletest-release-1.7.0/include-- System tests enabledCMake Deprecation Warning at test/CMakeLists.txt:133 (cmake_policy):  The OLD behavior for policy CMP0026 will be removed from a future version  of CMake.   The cmake-policies(7) manual explains that the OLD behaviors of all  policies are deprecated and that a policy should be set to OLD only under  specific short-term circumstances.  Projects should be ported to the NEW  behavior and not rely on setting a policy to OLD.  -- Could NOT find Doxygen (missing: DOXYGEN_EXECUTABLE)CMake Warning at docs/CMakeLists.txt:46 (message):  Doxygen not found.  Can't build Doxygen documentation  -- Configuring done-- Generating doneCMake Warning:  Manually-specified variables were not used by the project:     KLEE_LIBCXXABI_SRC_DIR  -- Build files have been written to: /home/bigeast/klee-2.1/build

makesudo make install

clang-9 -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c

/* * First KLEE tutorial: testing a small function */ #include "klee/klee.h" int get_sign(int x) {  if (x == 0)     return 0;   if (x < 0)     return -1;  else     return 1;} int main() {  int a;  klee_make_symbolic(&a, sizeof(a), "a");  return get_sign(a);}

bigeast@ubuntu:~/klee-2.1/examples/get_sign$ klee get_sign.bcKLEE: output directory is "/home/bigeast/klee-2.1/examples/get_sign/klee-out-0"KLEE: Using Z3 solver backend KLEE: done: total instructions = 33KLEE: done: completed paths = 3KLEE: done: generated tests = 3

bigeast@ubuntu:~/klee-2.1/examples/get_sign$ ls klee-lastassembly.ll  messages.txt  run.stats         test000002.ktest  warnings.txtinfo         run.istats    test000001.ktest  test000003.ktest

bigeast@ubuntu:~/klee-2.1/examples/get_sign$ ktest-tool klee-last/test000001.ktestktest file : 'klee-last/test000001.ktest'args       : ['get_sign.bc']num objects: 1object 0: name: 'a'object 0: size: 4object 0: data: b'x00x00x00x00'object 0: hex : 0x00000000object 0: int : 0object 0: uint: 0object 0: text: ....bigeast@ubuntu:~/klee-2.1/examples/get_sign$ ktest-tool klee-last/test000002.ktestktest file : 'klee-last/test000002.ktest'args       : ['get_sign.bc']num objects: 1object 0: name: 'a'object 0: size: 4object 0: data: b'xffx00x00x00'object 0: hex : 0xff000000object 0: int : 255object 0: uint: 255object 0: text: ....bigeast@ubuntu:~/klee-2.1/examples/get_sign$ ktest-tool klee-last/test000003.ktestktest file : 'klee-last/test000003.ktest'args       : ['get_sign.bc']num objects: 1object 0: name: 'a'object 0: size: 4object 0: data: b'x00x00x00x80'object 0: hex : 0x00000080object 0: int : -2147483648object 0: uint: 2147483648object 0: text: ....