| Age | Commit message (Collapse) | Author |
|---|
|
breaks DejaGNU tests). The issue is that in Tcl the quote needs escaping
but for llvm-lit we don't need to do this.
We should move to using the LLVM FileCheck tool instead of grep!
|
|
llvm-lit from LLVM3.3 to actually run KLEE's testsuite.
Things still seem to be broken though.
|
|
Fix assert library linking
|
|
In case linking of external libraries failed, user would
only be informed if KLEE is compiled with assertions enabled.
This fix lets KLEE always fail.
|
|
Existence of main() function is checked with assertion.
This check fails if KLEE is compiled in Release mode.
|
|
Feature klee internal functions
|
|
get_sign.c missing include
|
|
|
|
(for klee-uclibc)
would be created before the destination directory existed.
|
|
under release build.
The problem is that under release build the install command is told
to strip symbols from the tools. It tries to do this for the python
scripts and fails.
This commit hacks this by requesting that symbols are not stripped
from the python scripts.
|
|
Fixes klee install. Adds support for passing libc.a files to --with-uclibc.
|
|
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.
|
|
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)
|
|
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.
|
|
consumption.
The header files are normally installed
by the install-local target in the top-level
makefile.
See Makefile.rules ( "Install support for the project's include files" )
|
|
|
|
( Fix compilation of unittests under Clang )
|
|
Fix compilation of unittests under Clang.
|
|
It seems the GTest header file in LLVM 3.3 (and possibly other versions)
makes use of typeid() but the build system passes -fno-rtti. These
are incompatible and if building with Clang then compilation will
fail. GCC doesn't seem to care!
|
|
emphasising that the function cannot be returned from early.
|
|
file as well.
|
|
is more helpful because often the next message is "Now ignoring error
at this location". Which is slightly confusing when no location
is shown.
|
|
is actually available.
In addition if doing a DEBUG build then the command line flag
-debug-only=klee_missing_debug
shows the instructions missing debug information
and
-debug-only=klee_obtained_debug
show the instructions with debug information.
|
|
debug information is attached directly to most instructions so
the simpler algorithm added in 5ecfd6e2fd5becc10be355b3a20d014e76e40518
can be used.
Since support for LLVM version < 2.9 has been removed the old algorithm
should be removed.
This has been tested with LLVM 2.9 and LLVM 3.3
|
|
* Just iterate over the instructions which use the function to be inlined
* Handle each callsite (e.g. CallInst and InvokeInst)
|
|
|
|
KLEE provides runtime library functions to do detection of bugs (e.g. overflow).
This runtime functions are not the location of the bugs but it is
the next non-runtime library function from the stack.
Use the caller inside that function to indicate where the bug is.
|
|
LLVM versions
With newer LLVM versions (starting with LLVM 2.7) debug information are directly associated
as meta data with each instruction.
Therefore, debug information can be acquired directly from each instruction.
|
|
Patch by Daniel Lupei, fixing a performance bug with the counterexample cache. (This is an old patch, reported at http://llvm.org/bugs/show_bug.cgi?id=11435, on KLEE's old bug tracking system.)
|
|
Re-add support for running individual tests when built with LLVM3.3
|
|
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
|
|
Allow different build modes for LLVM coexist (this issue can be avoided entirely if out of source builds are used and each build is its own directory)
|
|
|
|
counterexample cache. (This is an old patch, reported at
http://llvm.org/bugs/show_bug.cgi?id=11435, on KLEE's old bug tracking
system.)
|
|
Chroot replay feature
|
|
|
|
Deprecate LLVM 2.8 and lower and remove support for it
|
|
|
|
|
|
Patch Set II - Memleaks
|
|
|
|
|
|
Fixes memleak
|
|
|
|
Fix using assembler addresses for global variables
|
|
|
|
prior patch, this is part of the CU experiments and doesn't really
belong here.
|
|
Fix runtime posix
|
|
|
|
uclibc is compiled without symbolic printf support
|
