about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2014-01-20Added Runtime/POSIX/lit.local.cfg file that prevents the POSIXDan Liew
tests from being executed if not enabled at configure time.
2014-01-20Fixed tests where llvm-gcc was called without the -emit-llvm flag.Dan Liew
DejaGNU testing used to have this flag in its substitution variable but for llvm-lit this has not been done. I could replicate what DejaGNU did but by forcing developers to be explicit when creating LLVM bitcode * Remove test suite inconsistentcies. Some tests explictly use -emit-llvm * Allows for tests to be written in the future that invoke the compiler as a native compiler
2014-01-20Add lit.local.cfg file for test/Concrete so no tests are executedDan Liew
in this directory. I don't know why these tests are here, they weren't executed before by DejaGNU.
2014-01-20* Do not ignore lit.local.cfg files needed for llvm-litDan Liew
* Ignore lit.site.cfg file.
2014-01-20Removed all of llvm-lit's dependence on DejaGNU. A few thingsDan Liew
are now broken and will be fixed shortly.
2014-01-20Fixed Feature/InAndOutOfBounds.c so it did not make use of ! whichDan Liew
seemed to causing problems for llvm-lit's parser.
2014-01-20Force python2 to be used when running llvm-lit. This needs to be fixedDan Liew
properly at configure time at some point.
2014-01-20Fix Feature/Envp.c test for llvm-lit by providing the PWD environmental variableDan Liew
in test environment.
2014-01-20Fixed Feature/LongDouble.cpp test for llvm-lit by removed use ofDan Liew
{ } quotes. I also add FileCheck lines but I've not added running FileCheck because only new versions of FileCheck support the CHECK-DAG: syntax.
2014-01-20Fixed many tests that make use of the file tool to checkDan Liew
a file created by KLEE exists. A big difference between DejaGNU and llvm-lit is that in DejaGNU the working directory is the test output directory (e.g. test/Feature/Output) but in llvm-lit the working directory is the test directory (e.g. test/Feature ) To fix this I have used the %T substitution variable for llvm-lit. I have also improved some tests by using LLVM's FileCheck tool and removing of hard coded constants for data type size in some places. This commit inevitably breaks running the tests under DejaGNU. Although it is possible to hack by introducing the %T substitution variable some tests would still be broken because the use of shell pipes in DejaGNU doesn't seem to work properly. I could work around this but it's really not worth the effort.
2014-01-20Allow llvm-lit from 2.9 to work by hacking %T substitution variable.Dan Liew
2014-01-20Put llvm tools directory at beginning of PATH list so that the LLVMDan Liew
version that KLEE and llvm-as use is the same.
2014-01-20Add LLVM tool directory to PATH when running tests with llvm-lit.Dan Liew
This is needed because the helper tool 'not' is used by some tests
2014-01-20Fixed Expr/Parser/Simplify.pc test for llvm-lit. Escaped quote issue.Dan Liew
2014-01-20Fixed Expr/Parser/MultiByteReads.pc test.Dan Liew
2014-01-20Fixed Expr/Parser/ConstantFolding.pc test for llvm-lit (this probablyDan Liew
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!
2014-01-20Removed use of deprecated Tcl parser for tests. This allowsDan Liew
llvm-lit from LLVM3.3 to actually run KLEE's testsuite. Things still seem to be broken though.
2014-01-17Merge pull request #94 from MartinNowack/fix_assert_library_linkingDan Liew
Fix assert library linking
2014-01-17Fix error message for failing linking of librariesMartin Nowack
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.
2014-01-17Make KLEE fail in case main function is missingMartin Nowack
Existence of main() function is checked with assertion. This check fails if KLEE is compiled in Release mode.
2014-01-12Merge pull request #68 from MartinNowack/feature_kleeInternalFunctionsDan Liew
Feature klee internal functions
2014-01-10Merge pull request #86 from msoos/masterDan Liew
get_sign.c missing include
2014-01-10Fixing missing include from get_sign.cMate Soos
2014-01-09Fixed race condition in parallel build where a symbolic linkDan Liew
(for klee-uclibc) would be created before the destination directory existed.
2014-01-09Fix build system so that ktest-tool and klee-stats can be installedDan Liew
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.
2013-12-22Merge pull request #78 from delcypher/fix_klee_installCristian Cadar
Fixes klee install. Adds support for passing libc.a files to --with-uclibc.
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-21Do not install KLEE's header files. They are not for publicDan Liew
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" )
2013-12-21Do not install KLEE's internal libraries.Dan Liew
2013-12-21Fixed mistake in commit c5510caa2a0ce6ad9a153fee094fe50855313450Dan Liew
( Fix compilation of unittests under Clang )
2013-12-20Merge pull request #81 from delcypher/fix_unittest_llvm33_clangCristian Cadar
Fix compilation of unittests under Clang.
2013-12-20Fix compilation of unittests under Clang.Dan Liew
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!
2013-12-19Added a few comments to Executor::getLastNonKleeInternalInstruction()Dan Liew
emphasising that the function cannot be returned from early.
2013-12-19When writing stack traces for bugs write the location in the assembly.llDan Liew
file as well.
2013-12-19If error location information is missing be explicit about it. ThisDan Liew
is more helpful because often the next message is "Now ignoring error at this location". Which is slightly confusing when no location is shown.
2013-12-19Only record debug info into InstructionInfoTable if debug informationDan Liew
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.
2013-12-19Remove old algorithm for acquiring debug info. Since LLVM 2.7,Dan Liew
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
2013-12-19Optimize inlineChecks functionMartin Nowack
* Just iterate over the instructions which use the function to be inlined * Handle each callsite (e.g. CallInst and InvokeInst)
2013-12-19Replicate debug information from checked instructions to checker call.Martin Nowack
2013-12-19Allow to specify KLEE-internal functionsMartin Nowack
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.
2013-12-19Simplify acquisition of debug informtion for instruction info with newer ↵Martin Nowack
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.
2013-12-19Merge pull request #76 from srg-imperial/masterDan Liew
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.)
2013-12-19Merge pull request #79 from delcypher/fix_llvm33_single_testDan Liew
Re-add support for running individual tests when built with LLVM3.3
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-19Merge pull request #80 from MartinNowack/fix_multiple_buildmodesDan Liew
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)
2013-12-19Allow different build modes for LLVM coexistMartin Nowack
2013-12-12Patch by Daniel Lupei, fixing a performance bug with theCristian Cadar
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.)
2013-12-11Merge pull request #31 from antiAgainst/chroot-replayCristian Cadar
Chroot replay feature
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-12-03 07:23:21 +0000