about summary refs log tree commit diff homepage
path: root/test/Feature
AgeCommit message (Collapse)Author
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.
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-09-23Lower intrinsic instruction "llvm.trap" to a call of the abort() function.Lei Zhang
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-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-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
2012-11-28Only emitting a warning, instead of failing on large mallocs.Cristian Cadar
Addresses the issue raised by Bowen Zhou at http://keeda.stanford.edu/pipermail/klee-dev/2012-November/000972.html. Fixed test case that depended on the old behavior. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168797 91177308-0d34-0410-b5e6-96231b3b80d8
2012-11-28Fixed fragile test case that depended too much on the code generatedCristian Cadar
by the compiler (this was failing with clang/llvm 3.1). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168795 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: "Added primitive test that checks kleaver's newCristian Cadar
-print-smt option. Improved Feature/ExprLogging.c test: - Now (primitive) checks the result of -write-smt2s - Now (primitive) checks the result of -write-pcs - Now (primitive) checks the result of -write-cvcs" git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166569 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew which improves the logging options: "RemovedCristian Cadar
-use-query-pc-log and -use-stp-query-pc-log and replaced with better command line option -use-query-log=option. Multiple comma seperated options can be specified after -use-query-log=. In addition queries can now be logged in SMT-LIBv2 format as well as KQuery format. The names of logging files has changed and also KLEE now informs users which files are being written to. Because of the changes the test/Feature/ExprLogging.c test broke so it was necessary to fix it." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166565 91177308-0d34-0410-b5e6-96231b3b80d8
2012-09-12Restructured the command-line options for setting the searchCristian Cadar
heuristics in KLEE. The new options are documented at http://klee.llvm.org/klee-options.html. Cleaned a bit the code in UserSearcher.cpp, and fixed some test cases to use the new options. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163711 91177308-0d34-0410-b5e6-96231b3b80d8
2012-09-11Fixed test case to be independent of compiler optimizations and search ↵Cristian Cadar
heuristics. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163631 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-20Fixed bug FPToSI bug reported by Peng Li. Added a simple test case. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160547 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-10Lowering support for the llvm.uadd.with.overflow intrinsic.Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154367 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-08Fixed --max-stp-time, which wasn't working unless --use-forked-stp wasCristian Cadar
also used. Thanks to Paul Marinescu for reporting and debugging this. The patch also disables the STP timeout by default. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154300 91177308-0d34-0410-b5e6-96231b3b80d8
2011-08-01Make the Executor capable of handling bitcasts of aliases, by rewriting thePeter Collingbourne
direct function call logic. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136605 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-29Sign extend, rather than zero extend, narrow gep indicesPeter Collingbourne
For example, clang creates these for ++ and -- operations on pointers on 64-bit platforms. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136474 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Add ConstantStruct support to Executor::evalConstantPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131586 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Support for arbitrary sized types in ConstantExpr::fromMemoryPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131583 91177308-0d34-0410-b5e6-96231b3b80d8
2010-10-22Use %llvmgxx to compile a .cpp filePeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@117118 91177308-0d34-0410-b5e6-96231b3b80d8
2010-08-05Small fix to test case. Without -f, the test fails when 'make test'Cristian Cadar
is run a second time without running 'make clean' in-between. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110321 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-08Add support for InsertValue and ExtractValue instructionsPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107912 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-28Applied Stefan Bucur's patch fromCristian Cadar
http://llvm.org/bugs/show_bug.cgi?id=6690. The patch adds specialized versions of klee_get_value for different types, fixing the previous klee_get_value function that sometimes truncated 64bit parameters to 32bit. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107006 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05Add long double support, patch by David Ramos.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100421 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05Fix -emit-llvm spelling (although, these aren't actually needed).Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100397 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01Implement va_arg handling for x86_64.Daniel Dunbar
- Based on a patch by Vladimir Kuznetsov! - x86_64 has a complicated calling convention for va_args; instead of dealing with this, this patch uses a clever workaround by initializing the va_list structure so that the callee believes all arguments were passed in the stack save area. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77819 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-27Start move to using APFloat (support long double).Daniel Dunbar
- Incomplete, still have to move some conversion operations. - Also, there isn't support yet for copying long double values to native memory. - Still, should be a monotonic improvement and we are no longer faking long double support. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74363 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Didn't mean to check this in.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74144 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Flesh out support for arbitrary bit widths in some key places (STP & constantDaniel Dunbar
creation). - Not used yet. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74142 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Support the extended query command syntax.Daniel Dunbar
- There are two optional lists following the constraints and the query expression. The first is a list of expressions to give values for and the second is a list of arrays to provide values for. - Update ExprPPrinter to accept extra arguments to print these arguments. - Add Parser support. - Add more ArrayDecl support. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72938 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Add test case.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72920 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-23Changed bout to ktest. Kept "BOUT\n" as the header of test files, for ↵Cristian Cadar
backward compatibility. Also changed KLEE_RUNTEST to KTEST_FILE. Updated tutorial-1. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72312 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-22Add "name" argument to klee_make_symbolic, and kill off klee_make_symbolic_name.Daniel Dunbar
- For compatibility we still accept 2 argument form of klee_make_symbolic, but this will go away eventually. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72265 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Initial KLEE checkin.Daniel Dunbar
- Lots more tweaks, documentation, and web page content is needed, but this should compile & work on OS X & Linux. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8