about summary refs log tree commit diff homepage
path: root/tools
AgeCommit message (Collapse)Author
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-21The location of KLEE's runtime libraries (apart from klee-uclibc)Dan Liew
are now detected at runtime. This allows the correct location to be used when klee is invoked from the build directory or from its install location (i.e. make install)
2013-12-21Revert "Patch from Ben Gras which "makes Klee look for the libraries in the"Dan Liew
This reverts commit 1715ee37118cdf8785a1dd70d812b6a88ad623e7. Conflicts: Makefile.common Future commits are going to add a more way elegant to handle the search for libraries in build/install directory.
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-12-06Remove stoppoint referencesMartin Nowack
2013-12-06Deprecate LLVM 2.8 and lowerMartin Nowack
2013-12-05Close file descriptors used for warnings and messagesMartin Nowack
2013-11-05Exit if using --libc=uclibc and KLEE was not configured with uclibcDan Liew
or if the configured path does not exist. Previously if KLEE was configured and compiled without uclibc linking would still succeed because KLEE_UCLIBC was blank so LLVM was effectively asked to link with "/lib/libc.a" i.e. the system's native C library!
2013-11-05Refactored part of KleeHandler construction so thatDan Liew
- A fixed size buffer is no longer used for output Directory path (would of failed for large paths). - KLEE warns about the presence of klee-out-* files that aren't directories. - We don't get stuck in an infinite loop if there aren't available directories.
2013-11-05sort and remove some includesFrank Busse
2013-11-05Fix arbitrary path limits and improved error handling (exitFrank Busse
even if not built with asserts).
2013-10-29Merge pull request #26 from delcypher/fix_divide_by_zeroPaul
Fixed bug where divide by zero bugs would only be detected once in a program
2013-10-21Removed unnecessary/redundant linking of library boost_thread-mt to klee and ↵Hristina Palikareva
kleaver.
2013-10-11MetaSMT builder, solver and command-line options.Hristina Palikareva
2013-10-11Fixed compilation on LLVM 2.9. irreader should be linked only for LLVM >= 3.3Cristian Cadar
2013-09-24Add missing header file and linker parameterDominic Chen
2013-09-21Merge pull request #17 from MartinNowack/LLVM33Cristian Cadar
Make KLEE compile with LLVM 2.3.
2013-09-02Implemented runtime check for overshift (controllable with --check-overshiftDan Liew
command line argument). Overshift is where a Shl, AShr or LShr has a shift width greater than the bit width of the first operand. This is undefined behaviour in LLVM so we report this as an error.
2013-08-29Revert "Use new PathV2 interface for LLVM 2.9 and higher"Martin Nowack
This reverts commit 5c059018c02a7c7db252a3cb636a39c89c430a06.
2013-08-29Fix compiling issues with llvm 2.9Martin Nowack
Interface for ParseCommandLineOptions changed with LLVM 3.2 preserving constness for pointer to arguments.
2013-08-29Use new PathV2 interface for LLVM 2.9 and higherMartin Nowack
Enable PathV2 interface starting from LLVM 2.9 and do some minor include cleanup.
2013-08-28Fix constness warnings issued by gcc 4.7Martin Nowack
2013-08-28Silence warning of deprecated PathV1 usageMartin Nowack
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-15Merge pull request #16 from MartinNowack/DebugSymbolsCristian Cadar
Patch Set VII - Handle additional debug intrinsics of LLVM
2013-08-15Merge pull request #10 from MartinNowack/TyposCristian Cadar
Fixed typos.
2013-08-14Handle additional debug intrinsics of LLVMMartin Nowack
2013-08-14Fix typoMartin Nowack
2013-08-13Modified ktest-tool so that it is compatible with python3.Dan Liew
2013-08-06TimingSolver and constructSolverChain() no longer coupled with pointers to ↵Hristina Palikareva
STPSolver objects. Timeout is now set by the solver at the top of the solver chain rather than by STPSolver.
2013-08-06Methods getConstraintLog() and setTimeout() made virtual and moved from ↵Hristina Palikareva
STPSolver to base Solver and SolverImpl classes, and consequently redefined in derived classes to call the corresponding methods down the solver chain. Method setTimeout() renamed to setCoreSolverTimeout().
2013-08-06Renaming solver-related command-line options in order to decouple them from ↵Hristina Palikareva
STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively. Option of running the SMT solver in a separate process (i.e. forked) set to true by default. Options of running SMT solver forked and with optimized divides made available to Kleaver as well.
2013-03-11Patch by Dan Liew which unifies the solver construction between KLEECristian Cadar
and Kleaver and fixes --use-query-log in Kleaver. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176811 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-06Patch by Tomek Kuchta which adds the --max-stp-time option to Kleaver.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176571 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-29Patch by Tomasz Kuchta that fixes the fragile way in which KLEE and Kleaver ↵Cristian Cadar
options were shared. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173819 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-22Patch by Hristina Palikareva which enables Kleaver to configure theCristian Cadar
solver chain. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173180 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Refactoring patch by Tomasz Kuchta that moves options shared by KLEE and ↵Cristian Cadar
Kleaver to a separate file. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171395 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta adding more detailed information on query failures.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171391 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta adding a new option (min-query-time-to-log) that ↵Cristian Cadar
enables KLEE to log only the queries exceeding a certain duration, or only those that time out. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171385 91177308-0d34-0410-b5e6-96231b3b80d8
2012-11-27Patch by Seungbeom Kim: "Interrupting KLEE's execution while aCristian Cadar
watchdog is in effect kills the watchdog immediately, giving the user a shell prompt prematurely while the child process is still running. This patch keeps the watchdog running until the child is finished. I see no need to be able to kill the watchdog forcefully, as long as the child process can be killed forcefully with two interrupts." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168696 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Jonathan Neuschäfer: "update symbol list forCristian Cadar
klee_get_value*. It might be better to just get (most of) the exported symbols right from the SpecialFunctionHandler class." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166585 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Code refactorings by Jonathan Neuschäfer: "move increment into for-loopCristian Cadar
head (Just a cosmetic change to make things a bit more readable)" and "move duplicate code to a function and also remove an old comment that seems to be obsolete by now. (Another cosmetic change)" git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166581 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: "Added support for generating .smt2 files whenCristian Cadar
writing out test cases (option --write-smt2s) in KLEE." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166568 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: "Added -print-smtlib option to kleaver tool thatCristian Cadar
allows .pc files to be printed as SMT-LIBv2 queries." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166563 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-09Patch by Tomasz Kuchta that adds several useful options (--print-abs-times, ↵Cristian Cadar
--print-rel-times, --precision) to klee-stats. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@165499 91177308-0d34-0410-b5e6-96231b3b80d8
2012-09-11Changed the default to --max-memory and documented randomize-fork.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163632 91177308-0d34-0410-b5e6-96231b3b80d8
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-06-21Patch by Paul Marinescu improving klee-stats: "klee-stats now reports avg ↵Cristian Cadar
and max memory consumption and states. A bug in the compare-by=<key> functionality has been fixed and the --compare-at=[<value>|last] option has been added. Specifying a value reports all statistics at the point where <key> had value <value>; specifying 'last' reports at the largest <key> value common to all executions" git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@158948 91177308-0d34-0410-b5e6-96231b3b80d8
2012-06-20Fixed a minor issue related to an error path in --posix-runtime mode.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@158835 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-12-25 16:14:06 +0000