about summary refs log tree commit diff homepage
path: root/Makefile.config.in
AgeCommit message (Collapse)Author
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-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-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-25Remove some dead makefile variables left over from the old testingDan Liew
system.
2015-04-25Remove dead STP logging code.Dan Liew
2015-04-09Try to fix using the compiler KLEE's configure script detected again!Dan Liew
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)
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.
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-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.
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-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-11Fixed compilation on LLVM 2.9. irreader should be linked only for LLVM >= 3.3Cristian Cadar
2013-10-03Extending ./configure with support to use metaSMT.Hristina Palikareva
2013-09-21Merge pull request #17 from MartinNowack/LLVM33Cristian Cadar
Make KLEE compile with LLVM 2.3.
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-27Port to LLVM 3.3Martin Nowack
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
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.
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: "fixed mistake in autoconf substitution variable name."Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160792 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-07-14Add option to use an external version of STPPeter Collingbourne
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
2009-05-21Initial KLEE checkin.Daniel Dunbar
- 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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 07:06:22 +0000