about summary refs log tree commit diff homepage
path: root/autoconf/configure.ac
AgeCommit message (Collapse)Author
2017-10-04Remove Autoconf/Makefile build system and adjust the TravisCIDan Liew
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.
2017-07-20Switching version to 1.4.0Cristian Cadar
2016-12-28Fix two issues with AC_LINK_IFELSE for metaSMT:Hoang M. Le
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.
2016-11-30Increasing version to 1.3.0Cristian Cadar
2016-09-29configure: add option to enable timestampingJiri Slaby
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>
2016-07-08Support gzip-based compression of raw_outstreamsMartin Nowack
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.
2016-06-10rename the configure option --with-metasmt-default-solver to ↵Hoang M. Le
--with-metasmt-default-backend and improve the associated CXX flag
2016-06-10add --with-metasmt-default-solver option to configureHoang M. Le
2016-06-10metaSMT does not require RTTIHoang M. Le
2016-03-31Moving to version 1.2.0Cristian Cadar
2016-03-05Fix SELinux signatures in runtimeLaszlo Szekeres
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.
2016-02-27Add support for tcmallocMartin Nowack
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.
2016-02-14Handle Z3 API change between 4.4.1 and the current master branchDan Liew
for the ``Z3_get_error_msg()`` function.
2016-02-10Teach the configure script to configure the build to use the Z3 SMTDan Liew
solver using the new ``--with-z3=`` option.
2016-01-14Output a message reporting if the MetaSMT backend is enabled whenDan Liew
running the Configure script.
2016-01-14Fix behaviour of --with-metasmt when passed a path that doesn't exist.Dan Liew
2016-01-14Make it possible to build KLEE without using STP and only MetaSMT.Dan Liew
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.
2015-11-13Moving to version 1.1.0Cristian Cadar
2015-08-10Changed version to 1.0.0 v1.0.0 1.0.xCristian Cadar
2015-04-25Give KLEE release version information in the output of klee and kleaverDan Liew
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
2015-04-08Fix very annoying issue where KLEE's configure would completlyDan Liew
ignore the C++ compiler detected and just use the compiler detected during the LLVM configure.
2015-04-03Upstream STP now depends on an external build of minisat. Attempt toDan Liew
fix travis build of upstream STP and also how KLEE links against STP.
2014-11-01Upstream libstp is no longer dependent on Boost so remove theDan Liew
configure/Makefile code that adds Boost as a depdendency because We don't need to support old versions of STP that needed Boost.
2014-11-01configure: allow stp being installed in /Jiri Slaby
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>
2014-09-14Provide --enable-cxx11 configure option to enable building with C++11.Dan Liew
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.
2014-09-13Add KLEE specific DEBUG macros.Daniel Dunbar
- 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.
2014-09-12[tests] Fix Concrete tests for out-of-tree builds.Daniel Dunbar
2014-09-12Add support for getting memory usage on Darwin.Daniel Dunbar
2014-09-12Do not require mallinfo(), which is Linux specific.Daniel Dunbar
2014-09-12Do not require <sys/capability.h>, which is Linux specific.Daniel Dunbar
2014-04-24Have configure check for presense of mallinfo for the newly addedDan Liew
klee::util::GetTotalMemoryUsage()
2014-01-25Upstream STP's libstp now depends on boost. This commit updatesDan Liew
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.
2014-01-20Remove the last remnants (I think) of DejaGNU. Goodbye!Dan Liew
Say hello to our new friend, llvm-lit :)
2013-12-21klee-uclibc detection is now a lot cleaner. KLEE now assumesDan Liew
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.
2013-12-19Re-add support for running individual tests when built with LLVM3.3Dan Liew
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
2013-12-19Allow different build modes for LLVM coexistMartin Nowack
2013-12-11Merge pull request #31 from antiAgainst/chroot-replayCristian Cadar
Chroot replay feature
2013-12-08Add chroot jail support in klee-replay.Lei Zhang
2013-11-08Fix the detection of the LLVM bitcode compiler. This is now done at KLEEDan Liew
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!
2013-10-11MetaSMT builder, solver and command-line options.Hristina Palikareva
2013-10-03Extending ./configure with support to use metaSMT.Hristina Palikareva
2013-08-28Modified the buildmode of bitcode libraries.Dan Liew
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.
2013-08-15Add support for dejagnu as removed from LLVM 3.2Martin Nowack
Added support for dejagnu to still allow tests to be executed under LLVM 3.2.
2013-08-13Updated configure.ac to use python3 compatible command.Dan Liew
2012-07-31Patch by Dan Liew that removes our internal copy of STP, and makes the ↵Cristian Cadar
--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
2012-07-26Patch by Dan Liew that adds support for building Doxygen out-of-source.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160795 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-20Deprecate LLVM_VERSION_MAJOR and LLVM_VERSION_MINOR in favour ofPeter Collingbourne
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
2011-05-18Use local Makefile.rulesPeter Collingbourne
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
2010-10-04Fix the Release+Asserts build-type-overwrite logic,Dylan Noblesmith
and document it. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115513 91177308-0d34-0410-b5e6-96231b3b80d8
2010-09-30Tweak configure to deal with another LLVM "Release -> Release+Asserts" rename onDaniel Dunbar
TOT. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115196 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 17:56:32 +0000