about summary refs log tree commit diff homepage
path: root/test
AgeCommit message (Collapse)Author
2014-02-14Fixed overshift of logical right shift by symbolic so that it overshiftsDan Liew
to zero. Test case is included.
2014-02-14Added C test case that checks that concrete and symbolic overshiftDan Liew
behaviour for left shift are identical.
2014-02-14Fixed overshifting an expression by a constant so that we overshift toDan Liew
zero. A test case was added for this. In addition the use to vc_bvExtract() was removed for shifting left by an expression because we don't want/need bitmasked behaviour anymore.
2014-02-14Added a test case for testing overshift behaviour of Shl and fixedDan Liew
a bug in the previous commit where 32-bit width was assumed.
2014-02-09Merge pull request #100 from delcypher/pass-param-llvm-litCristian Cadar
Allow passing arbitrary command line flags to klee and kleaver when running llvm-lit
2014-02-04Explicitly propagate CPLUS_INCLUDE_PATH and C_INCLUDE_PATH environmentDan Liew
variables in llvm-lit. This should hopefully fix the build bot. The propagation of environmental variables was also slightly refactored.
2014-01-29Fix Runtime/POSIX/Isatty.c test under LLVM3.3. The program makesDan Liew
a call fprintf(stderr,...). llvm-gcc transforms this to a call to fwrite() however clang does not so klee-uclibc's fprintf will be called instead and if klee-uclibc is compiled with KLEE_SYM_PRINTF then output will always go stdout if the FILE is stdout or stderr. The end result of this is that when we build with Clang under LLVM3.3 is that the fprintf(stderr,...) print outs go to standard output instead and so the test would fail because it expects the fprintf(stderr,...) to be on stderr. This test sort of fixes this by having the test check stdout for the fprintf(stderr,...) statements too.
2014-01-28Allow passing arbitrary command line flags to klee and kleaverDan Liew
when running llvm-lit. This is done by doing something like $ cd test/ $ llvm-lit --param klee_opts=--xxx --param kleaver_opts=--yyy . This would pass "--xxx" as an extra option to KLEE when running tests and would pass "--yyy" as an extra option to kleaver when running tests. This feature has been added to make it easy to pass different flags to KLEE or Kleaver without needing to modify tests or recompile KLEE with different defaults (yuck!).
2014-01-20Hide make check command unless using VERBOSE make variable.Dan Liew
e.g. $ make check VERBOSE=1 # Shows command and shows more detail $ make check # Does not show command and shows summary
2014-01-20Explicitly use only one thread when invoking llvm-lit in TestRunner.shDan Liew
We need to fix the test suite so we can run it in parallel.
2014-01-20Fixed test cases that fail if using an in-source buildDan Liew
2014-01-20Only run klee-uclibc tests if KLEE was configured with klee-uclibcDan Liew
support.
2014-01-20Partially fix python detection for running llvm-lit.Dan Liew
The problem is newer LLVM versions (e.g. 3.3) detect python at their configure time whereas older versions don't (i.e. 2.9). So I don't want to add python detection to KLEE's configure if LLVM already does the work for us. We need to move off llvm 2.9 anyway.
2014-01-20Remove the last remnants (I think) of DejaGNU. Goodbye!Dan Liew
Say hello to our new friend, llvm-lit :)
2014-01-20Give absolute paths to KLEE's tools in lit.cfg . This fixes a longDan Liew
standing FIXME:
2014-01-20Only run SELinux test if support for SELinux was detected at configureDan Liew
time.
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-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.
2013-11-14Add additional note that testcase might fail ifMartin Nowack
uclibc is compiled without symbolic printf support
2013-11-02Fix Futimesat compilation with newer gcc and clangMartin Nowack
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-17Fixed solver-related nondeterminism in test case ↵Hristina Palikareva
./test/Feature/ExprLogging.c -- using the counterexample cache affects the total number of queries issued to the solver.
2013-10-15Fixed nondeterministic behaviour in test case ./test/Solver/LargeIntegers.pc ↵Hristina Palikareva
-- only 16 bytes of array a were initialised in Query 2, but values of 17 bytes were later required for comparison.
2013-10-14Replaced --libc=klee with --libc=uclibc in two tests (as for ↵Cristian Cadar
https://github.com/ccadar/klee/issues/32) and fixed an #include in one of the tests.
2013-09-25Merge pull request #25 from paulmar/masterCristian Cadar
Added some of the common *at functions & others to the model. Obey --max-forks in switch statements.
2013-09-23Lower intrinsic instruction "llvm.trap" to a call of the abort() function.Lei Zhang
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-09-02Fixed bug where divide by zero bugs would only be detected once in a programDan Liew
even if there were many divide by zero bugs. The fix basically inlines all function calls to klee_div_zero_check() so that each call to klee_report_error() is a unique instruction for each instrumentation of a divide operation. It also seems that inlining the call "magically" fixed the debug information (file and line number) of the instruction so that the debug information on the inlined instructions matches that of the instrumented division instruction. Note that the command line option -emit-all-errors could be used to workaround the bug fixed in this commit.
2013-08-29Added some of the common *at functions to the modelPaul Marinescu
2013-08-28Fix test case to use llvm-link instead of llvm-ldMartin 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-15Implemented llvm.umul.with.overflowMartin Nowack
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-18Patch and test case by Jiri Slaby to handle "initializing globals whenCristian Cadar
a global has an undef fill of holes inside structures." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@177285 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta that refactors the logging code, by introducing a new ↵Cristian Cadar
logging class hierarchy. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171387 91177308-0d34-0410-b5e6-96231b3b80d8