| Age | Commit message (Collapse) | Author |
|---|
|
|
|
1. It expects only 2 arguments, so if linking succeeds, nothing will happen (thanks to []),
otherwise the message "checking for new_bitvector() in -lmetaSMT" will appear.
The latter is that what we currently observe, which means linking actually failed.
2. The reason for linking failure is the use of "-lmetaSMT" in LDFLAGS.
AC_LINK_IFELSE does approximately the following: ${CXX} ... -lmetaSMT ${EXECUTABLE_NAME} ${LIBS},
which causes "libmetaSMT cannot be found" (at least on Ubuntu Xenial, where ${LIBS} = -lz).
After consulting https://www.gnu.org/software/autoconf/manual/autoconf-2.66/html_node/Running-the-Linker.html,
adding "-lmetaSMT" to ${LIBS} seems to be the correct solution.
|
|
|
|
It is pain for build systems to see __DATE__ or __TIME__ in sources as
the build is not reproducible. So disable the timestamping by default
and add an option to enable it if somebody is really after it.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
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
|
|
|
|
|
|
|
|
The SELinux function signatures have changed between version 2.2 and
2.3. In particular, the type of the "security context" parameter was
changed from char * to const char *, with the following patch:
SELinuxProject/selinux@9eb9c9327563014ad6a807814e7975424642d5b9.
Recent Linux distributions (e.g. Ubuntu 15.10) ship with the updated
version of libselinux. This change makes the SELinux runtime compatible
with the newer versions of the library by replacing security_context_t
with its original char * definition and defining it as const only if the
installed library does so. Whether the system uses const char * types is
detected with the configure script.
Fixes klee/klee#303.
|
|
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.
|
|
for the ``Z3_get_error_msg()`` function.
|
|
solver using the new ``--with-z3=`` option.
|
|
running the Configure script.
|
|
|
|
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
|
|
ignore the C++ compiler detected and just use the compiler detected
during the LLVM configure.
|
|
fix travis build of upstream STP and also how KLEE links against STP.
|
|
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>
|
|
on Linux systems (2.60 is quite old) which will make updating the
configure script easier for most users.
|
|
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.
|
|
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling
the checks in that mode).
- Eventually it would be nice to just move off of LLVM's DEBUG infrastructure
entirely and just have our own copy, but this works for now.
- Fixes #150.
|
|
|
|
|
|
|
|
|
|
newer versions of autoconf""
The entire point of this version check in this script is so that configure is
only generated with one exact version of autotools, so that it doesn't get
spurious diffs from people generating it with different versions. This is the
approach used by LLVM, and I'd like to stick to it. Most people don't regenerate
these files, so it falls on the people who do to install the appropriate
versions of the tools.
If we want to change this policy, we should just drop the version checks completely.
|
|
klee::util::GetTotalMemoryUsage()
|
|
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.
|
|
Say hello to our new friend, llvm-lit :)
|
|
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
|
|
|
|
Chroot replay feature
|
|
|
|
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!
|
|
|
|
|
|
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.
|
|
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@160795 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
versions of autoconf"
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160793 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
version codes. This makes the preprocessor-based version tests more
concise and less error prone.
Also, fix the version tests in lib/Expr/Parser.cpp (immutable zext
and trunc were introduced in LLVM 2.9); now 2.9 passes "make test".
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135583 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
|
