about summary refs log tree commit diff homepage
path: root/test
AgeCommit message (Collapse)Author
2014-04-14Fix test case to support new llvm-litMartin Nowack
2014-04-14Update to new lit configuration to support changes in LLVM3.4Martin Nowack
2014-04-02Modify the SMT-LIB printer to declare arrays in a deterministic ↵Peter Collingbourne
(alphabetical) order.
2014-02-24Improved DumpStatesOnHalt.c to make sure there is always more than one ↵Cristian Cadar
instruction in main().
2014-02-24Fixed AliasFunction.c and AliasFunctionExit.c to work also when ↵Cristian Cadar
optimizations are enabled.
2014-02-14Added C test case that checks that concrete and symbolic overshiftDan Liew
behaviour for arithmetic right shift are identical.
2014-02-14Fixed overshift of arithmetic right shift by constant so that itDan Liew
overshifts to zero. Test case is included.
2014-02-14Fixed overshift of arithmetic 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 logical right shift are identical.
2014-02-14Fixed overshift of logical right shift by constant so that itDan Liew
overshifts to zero. Test case is included.
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-28 10:37:17 +0000