| Age | Commit message (Collapse) | Author |
|---|
|
configuration, TravisCI scripts and Dockerfile build appropriately.
There are a bunch of clean ups this enables but this commit doesn't
attempt them. We can do that in future commits.
|
|
Provide initial zlib-based compression support for
raw_outstreams. Replacing llvm::raw_fd_outstreams
with compressed_fd_outstreams automatically compresses
data in gzip format before writing to file.
Options added:
* --compress-log to compress all query log files (e.g. *.pc, *.smt2) on
the fly. Every query log file gets extended with .gz.
* --debug-compress-instructions to compress logfile for instruction
stream on the fly.
|
|
--with-metasmt-default-backend and improve the associated CXX flag
|
|
|
|
Beside improving performance of KLEE,
tcmalloc allows to track used memory correctly.
If available, tcmalloc is automatically used during compile time.
This can be forced to be:
- disabled using --without-tcmalloc
- enabled using --with-tcmalloc
In the second case, configure will fail if tcmalloc
is not found or usable.
Both versions of tcmalloc a minimal and normal version.
|
|
solver using the new ``--with-z3=`` option.
|
|
The default core solver is STP if KLEE is built with STP otherwise
it is MetaSMT.
Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for
consistency.
|
|
when they are given the --version command line option.
Unfortunately to make the build type and git revision available we
need to check this for every build which means KLEE's support library
will be rebuilt for every build which will slow down incremental builds.
This addresses issue #231
|
|
system.
|
|
|
|
My first attempt in b41cf33b6b726fd97e502c5c4818f5feeea0284b was wrong
because setting the CC and CXX Makefile variables in Makefile.config.in did not
work because LLVM's Makefile.config would override them.
Also detecting the C compiler is unnecessary because we already do this
(bitcode compiler detection)
|
|
ignore the C++ compiler detected and just use the compiler detected
during the LLVM configure.
|
|
configure/Makefile code that adds Boost as a depdendency because We
don't need to support old versions of STP that needed Boost.
|
|
I have stp in standard paths: /usr/include and /usr/lib64. Allow that
by correct STP_CFLAGS + STP_LDFLAGS instead of STP_ROOT. Those are
empty when --with-stp is not passed.
configure is regenerated by autoconf too.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
For LLVM >= 3.5 explicitly force this to be enabled otherwise we can't
compile against LLVM.
- Some minor tweaks to the configure logic by me (Daniel Dunbar), to ensure C++
compiler is tested before these checks run, and to properly restore CXXFLAGS.
|
|
the configure script to detect this by first trying to link without
boost and if that fails then trying to link libstp with boost.
This also updates the relevant Makefiles so that the klee and kleaver
executables link in STP's boost dependencies if necessary.
|
|
it can find klee-uclibc inside the same folder as the other
runtime libraries with the name "klee-uclibc.bca"
This is implemented as follows:
* When building, a sym-link is created to klee-uclibc's libc.a file
in the same directory that the rest of KLEE's runtime libraries
are built. This done so that if a developer changes klee-uclibc
on their system then the correct version of klee-uclibc is used
by KLEE.
* When installing, klee-uclibc's libc.a file is installed in the same
directory that the rest of KLEE's runtime libraries are installed.
In addition the configure script argument --with-uclibc can now
operate in two ways. It can either be passed the path to the root
of klee-uclibc or it can be passed a path to the libc.a file built
by klee-uclibc. This new behaviour has been added to allow users
to potential use pre-built versions of klee-uclibc.
|
|
It seems that the LLVM configure script no longer
looks for tclsh which was used to execute individual tests. E.g.
$ cd test
$ make TESTONE=Runtime/POSIX/DirConsistency.c check-one VERBOSE=1
This prevented the above from working. This commit fixes this by
having our configure script look for tclsh instead. The path_tclsh.m4
macro is taken from the projects/sample/autoconf/m4/ in LLVM3.3
|
|
configure time, not LLVM configure time! Configure will fail without
a working LLVM bitcode compiler. The precedence of detection is as
follows:
1. Compilers set by newly added --with-llvmcc= --with-llvmcxx= configure flags.
2. Clang in LLVM build directory.
3. llvm-gcc in PATH.
4. clang in PATH.
This has been tested with llvm2.9 (llvm-gcc in PATH) and llvm3.3 (clang
built in LLVM build directory).
This addresses a major pain point for new users of KLEE who forget to
put llvm-gcc in their PATH at LLVM configure time and then are later
forced to reconfigure and rebuild LLVM just so KLEE knows the right
PATH!
|
|
|
|
|
|
Make KLEE compile with LLVM 2.3.
|
|
The Default is Release+Asserts but if you are building KLEE with debug symbols (for example
"Release+Debug+Asserts" or "Debug+Asserts") then this breaks because KLEE will
look for the bitcode libraries in the wrong place because the
RUNTIME_CONFIGURATION macro is not defined to be what KLEE actually builds as.
This has been tweaked so that when we build the bitcode libraries the Makefile
variable "DEBUG_SYMBOLS" is correctly overridden.
|
|
Major changes are:
- Switching to llvm-link to build archive files
- Use GetMallocUsage instead of GetTotalMemoryUsage (be aware of bug in
LLVM 3.3 http://llvm.org/bugs/show_bug.cgi?id=16847)
- intrinsic library functions like memcpy/mov/set use weak linkage to be
replaced by e.g. uclibc functions
- rewrote linking with library
- enhanced MemoryLimit test case to check if mallocs were successful
|
|
Added support for dejagnu to still allow tests to be executed under
LLVM 3.2.
|
|
--with-stp option mandatory:
"1. At configure time the --with-stp= option is now mandatory.
2. The HAVE_EXT_STP macro has been removed.
3. The ENABLE_EXT_STP autoconf replacement variable has been removed and consequently the Makefile variable of the same name has been removed."
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161055 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160792 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
This patch changes the build system to use its own copy of
Makefile.rules (taken from a recent svn snapshot). Also added a
--with-llvm-build-mode flag and changed the default runtime library
configuration to Release+Asserts. Makefile.rules was modified to
support --with-llvm-build-mode and older versions of LLVM (tested 2.7
and 2.8).
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131584 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
This patch adds a new configure option, --with-stp, which configures
KLEE to use an external version of STP instead of the version in the
source tree. It includes documentation referring users to the STP
download location.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108347 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Lots more tweaks, documentation, and web page content is needed,
but this should compile & work on OS X & Linux.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
|
