Re: [klee-dev] Error while using C++ STL, libcxx

2020-06-06 Thread Cristian Cadar

On 26/05/2020 13:32, Namrata Jain wrote:
I also want to know about klee version-2.1-pre, is it the same as 
version 2.0? This is because I have made some changes in my klee source 
(2.1-pre) for a project and now I will be using version-2.1.
2.1-pre is the version string reported by the mainline between releases 
2.0 and 2.1.


Cristian

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


Re: [klee-dev] Error while using C++ STL, libcxx

2020-05-27 Thread Namrata Jain

Thankyou Felix.

--
Namrata Jain

On 26.05.2020 22:02, Felix Rath wrote:

Hey,


As suggested, I ran "make check" from klee-build-directory and found
that 47 unexpected tests were failing.


That definitely sounds like something might have been broken there.


What this error is about? I also found this as an open issue on klee
github page.


I sadly cannot help with this, as I don't use KLEE's build scripts,
and am not really familiar with how they work at all. So I don't know
what the correct options, usage, etc. for building KLEE with libcxx
support are.

As you mentioned that libcxx support was not required for the example 
I
stated, I built klee (version 2.1) without enabling libcxx and was 
able

to see the output "12" with no errors.


Nice :) Then I would assume that LLVM 9 or 10 should definitely help
with running with `--libcxx`.


Are these due to not linking libcxx?



KLEE: WARNING: undefined reference to function: _ZSt9terminatev
KLEE: WARNING: undefined reference to function: __cxa_begin_catch
KLEE: WARNING: undefined reference to function: __gxx_personality_v0


I think these are from not linking libcxxabi, which can be part of
libcxx depending on how you build it.


KLEE: WARNING: undefined reference to function: __syscall_rt_sigaction
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: fstat
KLEE: WARNING: undefined reference to function: ioctl
KLEE: WARNING: undefined reference to function: llvm.dbg.label
KLEE: WARNING: undefined reference to function: open
KLEE: WARNING: undefined reference to function: write
KLEE: WARNING: undefined reference to function: kill (UNSAFE)!


Some of these actually are provided by --posix-runtime (like `open`,
`ioctl` and maybe more), so that might help here. Others might not be
modeled for KLEE (yet), but they don't seem to be from libcxx, as
libcxx usually contains C++-mangled names (but they might appear in
the program because you #include'd  and ).


I also want to know about klee version-2.1-pre, is it the same as
version 2.0? This is because I have made some changes in my klee 
source

(2.1-pre) for a project and now I will be using version-2.1.


Can't really help with this, not really familiar with KLEE's release 
process.


Best,
Felix


From: Namrata Jain 
Sent: Tuesday, May 26, 2020 2:32 PM
To: Felix Rath
Cc: klee-dev@imperial.ac.uk
Subject: Re: [klee-dev] Error while using C++ STL, libcxx

Hello Felix,

Thankyou for the reply.
As suggested, I ran "make check" from klee-build-directory and found
that 47 unexpected tests were failing.
So, I installed llvm-10, but while installing libcxx from
klee-source-directory using the command:
LLVM_VERSION=10 SANITIZER_BUILD= BASE=
./scripts/build/build.sh libcxx

it generated output:

Detected OS: linux
OS=linux
Detected distribution: ubuntu
DISTRIBUTION=ubuntu
Detected version: 18.04
DISTRIBUTION_VER=18.04
Component sanitizer not found.
Component sanitizer not found.
ENABLE_OPTIMIZED Required but unset

What this error is about? I also found this as an open issue on klee
github page.

As you mentioned that libcxx support was not required for the example I
stated, I built klee (version 2.1) without enabling libcxx and was able
to see the output "12" with no errors.

(using the command: klee --libc=uclibc /experiment.bc)

Warnings that were generated:

KLEE: WARNING: undefined reference to function: _ZSt9terminatev
KLEE: WARNING: undefined reference to function: __cxa_begin_catch
KLEE: WARNING: undefined reference to function: __gxx_personality_v0
KLEE: WARNING: undefined reference to function: __syscall_rt_sigaction
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: fstat
KLEE: WARNING: undefined reference to function: ioctl
KLEE: WARNING: undefined reference to function: llvm.dbg.label
KLEE: WARNING: undefined reference to function: open
KLEE: WARNING: undefined reference to function: write
KLEE: WARNING: undefined reference to function: kill (UNSAFE)!
KLEE: WARNING ONCE: calling external: ioctl(0, 21505, 94590150907232) 
at

libc/termios/tcgetattr.c:43 12
KLEE: WARNING ONCE: calling __user_main with extra arguments.

Are these due to not linking libcxx?

I also want to know about klee version-2.1-pre, is it the same as
version 2.0? This is because I have made some changes in my klee source
(2.1-pre) for a project and now I will be using version-2.1.

Thankyou.

--
Namrata Jain


On 25.05.2020 17:21, Felix Rath wrote:

Hello Namrata,

I worked a lot on the current C++ support in KLEE (the recent C++
support PRs to KLEE were by me), so I hope I can help. I think the
main problem is that llvm 6.0 is quite old, and your example should
pretty much work as-is if you switch to a recent llvm version (the
most recent being 10, which should work). I tried your example locally
with llvm (and libc++) 10 and it produced the 

Re: [klee-dev] Error while using C++ STL, libcxx

2020-05-26 Thread Namrata Jain
ms to a working binary this way might be
a problem, or might still mix up llvm and g++ versions of the standard
library (as I'm not sure what this uses for linking, or whether it
reports an error). This might especially be the case when you build
larger real-word projects using wllvm++.

Here are the flags I generally use to build C++ programs for running 
with KLEE:


LIBCXX_LIB_DIR="//lib"
LIBCXXABI_LIB_DIR="//lib"
MY_CXX_FLAGS="-nostdinc++ -stdlib=libc++ -lc++ -lc++abi \
-I//libcxx/include \
-I//libcxxabi/include \
-Wl,-L$LIBCXX_LIB_DIR -Wl,-L$LIBCXXABI_LIB_DIR \
-Wl,-rpath=$LIBCXX_LIB_DIR -Wl,-rpath=$LIBCXXABI_LIB_DIR"

And then build a file main.cpp using:

clang++ $MY_CXX_FLAGS -emit-llvm -c main.cpp

Or, when building a project that uses cmake (plus setup for 
clang++/wllvm++):


cmake -DCMAKE_CXX_FLAGS="$MY_CXX_FLAGS" 

Depending on how you build libcxx and libcxxabi (I build them without
checking out the rest of llvm's source, which I think leads to a
slightly different setup), you might need only some of these. E.g., if
your build process outputs a `libc++.bca` that already contains a
linked version of `libc++abi`, the linker directives (those beginning
with -Wl) for libcxxabi should not be needed (but those for libcxx are
still required).

Additionally, I usually use a version of KLEE that supports C++
exceptions (exactly this PR: https://github.com/klee/klee/pull/966),
which is why the libcxxabi/libc++abi setup is required, but you might
be able to avoid specifying those if you use one of the released KLEE
versions or KLEE's current master.

Some more explanations: `-nostdinc++` makes the compiler not set
default paths for including standard library headers, which you also
used in your example. `-stdlib=libc++` makes clang++ use llvm's libc++
implementation instead of g++'s. I sometimes get warnings that this
flag is ignored by the compiler, which I think is due to the fact that
the next flags, `-lc++` and `-lc++abi`, already cause linking against
libc++ and libc++abi. The two `-I` directives then set up
include-paths for standard library includes done by the program
(pretty much what your example also did).

I then tell the linker, using the `-Wl,-L` flags, to also check the
given paths for required libraries, which leads to my versions of
libc++ and libc++abi being used. The `-Wl,-rpath=` flags make sure
that these same directories are also in the runtime path of the
program, which can be required if the program (additionally) loads
some parts of the standard library at runtime. I think this happens
when the standard library (or some part of it) is linked dynamically
(and not statically).

Maybe these flags can help as a starting point for determining the
flags you need in your use-case/setup. I think especially the
libcxxabi/libc++abi parts might no be required for you (yet), or might
need adjusting so you don't link libc++abi twice (once as part of
libc++ and once as libc++abi).

For running KLEE, `--libcxx` should always be accompanied by
`--libc=uclibc` (which you also did), as libcxx relies on a libc for
certain parts of its functionality (such as printing).

Sorry for this lengthy trace, if unnecessary or if this is a trivial 
issue.


I found the steps and output you gave really helpful to see what
exactly is going on.

To sum up, try running KLEE's tests, and try building with a more
recent version of llvm (I'd suggest 10) and see if that fixes the
issue. Also, when building larger programs, you might need to adjust
your compiler/linker flags to make sure things work correctly.

I'd be happy to hear if this fixed the issue, and in general how your
experience with KLEE's C++ support goes, and the kinds of
issues/questions that come up.

Best,
Felix


From: klee-dev-boun...@imperial.ac.uk
 on behalf of Namrata Jain

Sent: Sunday, May 24, 2020 5:47 PM
To: klee-dev@imperial.ac.uk
Subject: [klee-dev] Error while using C++ STL, libcxx

Hello all,

I always run into 'Terminator found in the middle of basic block' when 
I

try running C++ program with STL. I could not figure out if this error
is due to some error in program, how I run KLEE, libcxx or due to some
mistake while building KLEE.


An example program:

#include 
#include 

int main()
{
 std::vector x;
 x.push_back(1);
 x.push_back(2);
 std::cout << x[0] << x[1];
 return 0;
}

To generate bitcode:

 clang++ -emit-llvm -c experiment.cpp -o experiment.bc

(I also tried: clang++-6.0 -emit-llvm -c -std=c++11 -I
"/home/namrata/libc++-install-60/include/c++/v1/" -nostdinc++
experiment.cpp)

command I used to run klee:
  klee -libc=uclibc -libcxx -posix-runtime
/home/namrata/Desktop/project/verifTool/experiment.bc

Output:

KLEE: NOTE: Using POSIX model:
/home/namrata/build/Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: NOTE: Using libcxx :
/home/namrata/build/Debug+Asserts/lib/libc++.bca
KLEE: NOTE: Using klee

Re: [klee-dev] Error while using C++ STL, libcxx

2020-05-26 Thread Felix Rath
Hey,

> As suggested, I ran "make check" from klee-build-directory and found
> that 47 unexpected tests were failing.

That definitely sounds like something might have been broken there.

> What this error is about? I also found this as an open issue on klee
> github page.

I sadly cannot help with this, as I don't use KLEE's build scripts, and am not 
really familiar with how they work at all. So I don't know what the correct 
options, usage, etc. for building KLEE with libcxx support are.

> As you mentioned that libcxx support was not required for the example I
> stated, I built klee (version 2.1) without enabling libcxx and was able
> to see the output "12" with no errors.

Nice :) Then I would assume that LLVM 9 or 10 should definitely help with 
running with `--libcxx`.

> Are these due to not linking libcxx?

> KLEE: WARNING: undefined reference to function: _ZSt9terminatev
> KLEE: WARNING: undefined reference to function: __cxa_begin_catch
> KLEE: WARNING: undefined reference to function: __gxx_personality_v0

I think these are from not linking libcxxabi, which can be part of libcxx 
depending on how you build it.

> KLEE: WARNING: undefined reference to function: __syscall_rt_sigaction
> KLEE: WARNING: undefined reference to function: fcntl
> KLEE: WARNING: undefined reference to function: fstat
> KLEE: WARNING: undefined reference to function: ioctl
> KLEE: WARNING: undefined reference to function: llvm.dbg.label
> KLEE: WARNING: undefined reference to function: open
> KLEE: WARNING: undefined reference to function: write
> KLEE: WARNING: undefined reference to function: kill (UNSAFE)!

Some of these actually are provided by --posix-runtime (like `open`, `ioctl` 
and maybe more), so that might help here. Others might not be modeled for KLEE 
(yet), but they don't seem to be from libcxx, as libcxx usually contains 
C++-mangled names (but they might appear in the program because you #include'd 
 and ).

> I also want to know about klee version-2.1-pre, is it the same as
> version 2.0? This is because I have made some changes in my klee source
> (2.1-pre) for a project and now I will be using version-2.1.

Can't really help with this, not really familiar with KLEE's release process.

Best,
Felix


From: Namrata Jain 
Sent: Tuesday, May 26, 2020 2:32 PM
To: Felix Rath
Cc: klee-dev@imperial.ac.uk
Subject: Re: [klee-dev] Error while using C++ STL, libcxx

Hello Felix,

Thankyou for the reply.
As suggested, I ran "make check" from klee-build-directory and found
that 47 unexpected tests were failing.
So, I installed llvm-10, but while installing libcxx from
klee-source-directory using the command:
LLVM_VERSION=10 SANITIZER_BUILD= BASE=
./scripts/build/build.sh libcxx

it generated output:

Detected OS: linux
OS=linux
Detected distribution: ubuntu
DISTRIBUTION=ubuntu
Detected version: 18.04
DISTRIBUTION_VER=18.04
Component sanitizer not found.
Component sanitizer not found.
ENABLE_OPTIMIZED Required but unset

What this error is about? I also found this as an open issue on klee
github page.

As you mentioned that libcxx support was not required for the example I
stated, I built klee (version 2.1) without enabling libcxx and was able
to see the output "12" with no errors.

(using the command: klee --libc=uclibc /experiment.bc)

Warnings that were generated:

KLEE: WARNING: undefined reference to function: _ZSt9terminatev
KLEE: WARNING: undefined reference to function: __cxa_begin_catch
KLEE: WARNING: undefined reference to function: __gxx_personality_v0
KLEE: WARNING: undefined reference to function: __syscall_rt_sigaction
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: fstat
KLEE: WARNING: undefined reference to function: ioctl
KLEE: WARNING: undefined reference to function: llvm.dbg.label
KLEE: WARNING: undefined reference to function: open
KLEE: WARNING: undefined reference to function: write
KLEE: WARNING: undefined reference to function: kill (UNSAFE)!
KLEE: WARNING ONCE: calling external: ioctl(0, 21505, 94590150907232) at
libc/termios/tcgetattr.c:43 12
KLEE: WARNING ONCE: calling __user_main with extra arguments.

Are these due to not linking libcxx?

I also want to know about klee version-2.1-pre, is it the same as
version 2.0? This is because I have made some changes in my klee source
(2.1-pre) for a project and now I will be using version-2.1.

Thankyou.

--
Namrata Jain


On 25.05.2020 17:21, Felix Rath wrote:
> Hello Namrata,
>
> I worked a lot on the current C++ support in KLEE (the recent C++
> support PRs to KLEE were by me), so I hope I can help. I think the
> main problem is that llvm 6.0 is quite old, and your example should
> pretty much work as-is if you switch to a recent llvm version (the
> most recent being 10, which should work). I tried your example loc

Re: [klee-dev] Error while using C++ STL, libcxx

2020-05-25 Thread Felix Rath
 and libc++abi. The two `-I` directives 
then set up include-paths for standard library includes done by the program 
(pretty much what your example also did).

I then tell the linker, using the `-Wl,-L` flags, to also check the given paths 
for required libraries, which leads to my versions of libc++ and libc++abi 
being used. The `-Wl,-rpath=` flags make sure that these same directories are 
also in the runtime path of the program, which can be required if the program 
(additionally) loads some parts of the standard library at runtime. I think 
this happens when the standard library (or some part of it) is linked 
dynamically (and not statically).

Maybe these flags can help as a starting point for determining the flags you 
need in your use-case/setup. I think especially the libcxxabi/libc++abi parts 
might no be required for you (yet), or might need adjusting so you don't link 
libc++abi twice (once as part of libc++ and once as libc++abi).

For running KLEE, `--libcxx` should always be accompanied by `--libc=uclibc` 
(which you also did), as libcxx relies on a libc for certain parts of its 
functionality (such as printing).

> Sorry for this lengthy trace, if unnecessary or if this is a trivial issue.

I found the steps and output you gave really helpful to see what exactly is 
going on.

To sum up, try running KLEE's tests, and try building with a more recent 
version of llvm (I'd suggest 10) and see if that fixes the issue. Also, when 
building larger programs, you might need to adjust your compiler/linker flags 
to make sure things work correctly.

I'd be happy to hear if this fixed the issue, and in general how your 
experience with KLEE's C++ support goes, and the kinds of issues/questions that 
come up.

Best,
Felix


From: klee-dev-boun...@imperial.ac.uk  on 
behalf of Namrata Jain 
Sent: Sunday, May 24, 2020 5:47 PM
To: klee-dev@imperial.ac.uk
Subject: [klee-dev] Error while using C++ STL, libcxx

Hello all,

I always run into 'Terminator found in the middle of basic block' when I
try running C++ program with STL. I could not figure out if this error
is due to some error in program, how I run KLEE, libcxx or due to some
mistake while building KLEE.


An example program:

#include 
#include 

int main()
{
 std::vector x;
 x.push_back(1);
 x.push_back(2);
 std::cout << x[0] << x[1];
 return 0;
}

To generate bitcode:

 clang++ -emit-llvm -c experiment.cpp -o experiment.bc

(I also tried: clang++-6.0 -emit-llvm -c -std=c++11 -I
"/home/namrata/libc++-install-60/include/c++/v1/" -nostdinc++
experiment.cpp)

command I used to run klee:
  klee -libc=uclibc -libcxx -posix-runtime
/home/namrata/Desktop/project/verifTool/experiment.bc

Output:

KLEE: NOTE: Using POSIX model:
/home/namrata/build/Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: NOTE: Using libcxx :
/home/namrata/build/Debug+Asserts/lib/libc++.bca
KLEE: NOTE: Using klee-uclibc :
/home/namrata/build/Debug+Asserts/lib/klee-uclibc.bca
KLEE: output directory is
"/home/namrata/Desktop/project/verifTool/klee-out-19"
KLEE: Using STP solver backend
WARNING: this target does not support the llvm.stacksave intrinsic.
Terminator found in the middle of a basic block!
label %1
LLVM ERROR: Broken function found, compilation aborted!


KLEE source directory: /home/namrata/klee
KLEE build directory: /home/namrata/build

I followed the instructions on while building:
https://klee.github.io/build-llvm60/

KLEE Build command:

cmake   -DENABLE_SOLVER_STP=ON   -DENABLE_POSIX_RUNTIME=ON
-DENABLE_KLEE_UCLIBC=ON   -DKLEE_UCLIBC_PATH=/home/namrata/klee-uclibc/
  -DLLVM_CONFIG_BINARY=/usr/lib/llvm-6.0/bin/llvm-config
-DENABLE_KLEE_LIBCXX=ON-DENABLE_UNIT_TESTS=OFF
-DLLVMCC=/usr/lib/llvm-6.0/bin/clang
-DLLVMCXX=/usr/lib/llvm-6.0/bin/clang++
-DKLEE_LIBCXX_DIR=/home/namrata/libc++-install-60/
-DKLEE_LIBCXX_INCLUDE_DIR=/home/namrata/libc++-install-60/include/c++/v1/
/home/namrata/klee

Output:

-- The CXX compiler identification is GNU 7.5.0
-- The C compiler identification is GNU 7.5.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 2.1-pre
-- 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/lib/llvm-6.0/bin/llvm-config
-- LLVM_PACKAGE_VERSION: "6.0.0"
-- LLVM_VERSION_MAJOR: "6"
-- 

[klee-dev] Error while using C++ STL, libcxx

2020-05-24 Thread Namrata Jain

Hello all,

I always run into 'Terminator found in the middle of basic block' when I 
try running C++ program with STL. I could not figure out if this error 
is due to some error in program, how I run KLEE, libcxx or due to some 
mistake while building KLEE.



An example program:

#include 
#include 

int main()
{
std::vector x;
x.push_back(1);
x.push_back(2);
std::cout << x[0] << x[1];
return 0;
}

To generate bitcode:

clang++ -emit-llvm -c experiment.cpp -o experiment.bc

(I also tried: clang++-6.0 -emit-llvm -c -std=c++11 -I 
"/home/namrata/libc++-install-60/include/c++/v1/" -nostdinc++ 
experiment.cpp)


command I used to run klee:
 klee -libc=uclibc -libcxx -posix-runtime 
/home/namrata/Desktop/project/verifTool/experiment.bc


Output:

KLEE: NOTE: Using POSIX model: 
/home/namrata/build/Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: NOTE: Using libcxx : 
/home/namrata/build/Debug+Asserts/lib/libc++.bca
KLEE: NOTE: Using klee-uclibc : 
/home/namrata/build/Debug+Asserts/lib/klee-uclibc.bca
KLEE: output directory is 
"/home/namrata/Desktop/project/verifTool/klee-out-19"

KLEE: Using STP solver backend
WARNING: this target does not support the llvm.stacksave intrinsic.
Terminator found in the middle of a basic block!
label %1
LLVM ERROR: Broken function found, compilation aborted!


KLEE source directory: /home/namrata/klee
KLEE build directory: /home/namrata/build

I followed the instructions on while building: 
https://klee.github.io/build-llvm60/


KLEE Build command:

cmake   -DENABLE_SOLVER_STP=ON   -DENABLE_POSIX_RUNTIME=ON   
-DENABLE_KLEE_UCLIBC=ON   -DKLEE_UCLIBC_PATH=/home/namrata/klee-uclibc/  
 -DLLVM_CONFIG_BINARY=/usr/lib/llvm-6.0/bin/llvm-config   
-DENABLE_KLEE_LIBCXX=ON-DENABLE_UNIT_TESTS=OFF
-DLLVMCC=/usr/lib/llvm-6.0/bin/clang   
-DLLVMCXX=/usr/lib/llvm-6.0/bin/clang++   
-DKLEE_LIBCXX_DIR=/home/namrata/libc++-install-60/
-DKLEE_LIBCXX_INCLUDE_DIR=/home/namrata/libc++-install-60/include/c++/v1/ 
/home/namrata/klee


Output:

-- The CXX compiler identification is GNU 7.5.0
-- The C compiler identification is GNU 7.5.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 2.1-pre
-- 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/lib/llvm-6.0/bin/llvm-config
-- LLVM_PACKAGE_VERSION: "6.0.0"
-- LLVM_VERSION_MAJOR: "6"
-- 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: "OFF"
-- LLVM_ENABLE_EH: "OFF"
-- LLVM_ENABLE_RTTI: "ON"
-- LLVM_INCLUDE_DIRS: "/usr/lib/llvm-6.0/include"
-- LLVM_LIBRARY_DIRS: "/usr/lib/llvm-6.0/lib"
-- LLVM_TOOLS_BINARY_DIR: "/usr/lib/llvm-6.0/bin"
-- LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN: "ON"
-- TARGET_TRIPLE: "x86_64-pc-linux-gnu"
CMake Warning at CMakeLists.txt:248 (message):
  LLVM was built without assertions but KLEE will be built with them.

  This might lead to unexpected behaviour.


-- Looking for bitcode compilers
-- Found /usr/lib/llvm-6.0/bin/clang
-- Found /usr/lib/llvm-6.0/bin/clang++
-- Testing bitcode compiler /usr/lib/llvm-6.0/bin/clang
-- Compile success
-- Checking compatibility with LLVM 6.0.0
-- "/usr/lib/llvm-6.0/bin/clang" is compatible
-- Testing bitcode compiler /usr/lib/llvm-6.0/bin/clang++
-- Compile success
-- Checking compatibility with LLVM 6.0.0
-- "/usr/lib/llvm-6.0/bin/clang++" is compatible
-- LLVMCC: /usr/lib/llvm-6.0/bin/clang
-- LLVMCXX: /usr/lib/llvm-6.0/bin/clang++
-- 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
-- STP solver support enabled
-- Found STP version 2.1.2
-- Using STP static