about summary refs log tree commit diff homepage
path: root/test/Feature
AgeCommit message (Collapse)Author
2018-11-23Implemented memalign with alignmentLukas Wölfer
2018-11-05Check for stack overflow in a tested programMartin Nowack
Check if a state reaches the maximum number of stack frames allowed. To be performant, the number of stack frames are checked. In comparison, native execution checks the size of the stack. Still, this is good enough to find possible stack overflows. The limit can be changed with `-max-stack-frames`. The current default is 8192 frames.
2018-11-02Added test for the case where external calls are encountered but disallowedCristian Cadar
2018-11-02Replaced --no-externals and --allow-external-sym-calls with ↵Cristian Cadar
--external-calls, updated tests accordingly, and improved documentation on external calls
2018-11-02The test DeterministicSwitch.c does not need to allow external symbolic callsCristian Cadar
2018-10-29add %OOopt to recently added tests and ConcreteJulian Büning
2018-10-26llvm5: test, add -disable-O0-optnone to -O0Jiri Slaby
Otherwise optimizations done in klee won't have any effect. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-24Add testcase for shift checkMartin Nowack
Validate non-optimised and optimised variant of added checks.
2018-10-24Add test case for div checkerMartin Nowack
Check that only important div instructions are annotated. Check the optimized case as well: the call to the validating function might not be part of the code anymore but already inlined - make sure the instruction still has the metadata attached.
2018-10-24Added lowering passRafael Zaehl
2018-10-17tests: disable CompressedExprLogging on zlib-less systemsFrank Busse
2018-09-06Use FileCheck and LINE instead of grep if possibleMartin Nowack
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers.
2018-09-06Avoid Vararg non-deterministic allocationMartin Nowack
Vararg test can fail if KLEE is able to resolve the intended out-of-bound memory address to a memory object. To avoid this, allocate memory explicitly deterministic with sufficient space between the allocations. Enables support for Mac OSX again
2018-08-01test: remove geq-llvm-3.4Julian Büning
2018-07-28remove last comma from -debug-print-escaping-functionsJulian Büning
2018-07-28test/Feature/EscapingFunctionsAlias.c: clarify alias(ee) castingJulian Büning
2018-07-28add declarations to escapingFunctionsJulian Büning
2018-07-23ModuleUtil: improve and test valueIsOnlyCalledJulian Büning
* handle BlockAddress (which is not a valid function pointer) * there is no instruction with opcode 0 * add test for functionality
2018-07-12llvm38: test, change some testsJiri Slaby
alias in LLVM 3.8 has a new format, it adds an AliaseeTy parameter. So handle this in the tests. [v2] add comments about what was changed and why Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-07-11Removed support for klee_make_symbolic with 2 arguments. This has been ↵Cristian Cadar
deprecated for many years now and causes problems during replay. Changed and simplified affected test case.
2018-07-10test: remove undefined behaviourJiri Slaby
Shifting negative values is implementation-defined. Shifting by equal number of the bits as is the size of the type is undefined. So fix both of these. This fixes #911. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-06-29Make ConstantExpr hashing function faster and modify affected testTimotej Kapus
2018-05-24test: add versions of some tests for LLVM 3.7Richard Trembecký
Clone some tests to have their 3.7 version. 'call's, 'load's and 'getelementptr's match the new specification in them. @andreamattavelli: Fixed test cases: BitCastAlias test cases included modification to alias specifications that require LLVM 3.8 [v2] added comments what was changed and why [v3] the new tests are without suffix, the old ones have ".leq36". Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-05-18tests: use names in klee_make_symbolicFrank Busse
2018-05-17Improve error messages for ReadStringAtAddressTimotej Kapus
2018-05-06Moved regression test to proper location. Fixes #705Cristian Cadar
2018-05-01add blockaddress and indirectbr instructionsFrank Busse
2018-03-23fix test/Feature/BFSSearcherAndDFSSearcherInterleaved.c to use explicit ↵Julian Büning
enumeration of possible strings instead of CHECK-SAME (does not work as intended with LLVM >= 3.7)
2018-02-18Add testcase for constant array handlingMartin Nowack
2017-11-24klee_make_symbolic: add test cases for APIFrank Busse
2017-10-15Fixed assert in BFSSearcher that does not hold as part of interleaved searcherJulian Büning
2017-10-06Removed the word 'unsigned' from integer overflow error messagesAndrew Santosa
2017-08-09Merge pull request #742 from ccadar/foldCristian Cadar
Added checks for div/mod by zero and overshifts in constant expressio…
2017-08-07Added checks for div/mod by zero and overshifts in constant expressions. ↵Cristian Cadar
Such div/mod by zero expressions would previously crash KLEE. Added two test cases, one for div/mod by zero, the other for overshift. This fixes the bug reported in #268.
2017-08-04Removed merging searchersLukas Wölfer
2017-07-29Added an optional KInstruction* argument to evalConstant and ↵Cristian Cadar
evalConstantExpr which allows us to print the location associated with the constant in any error messages. Added a test case for the unsupported features for taking the address of a label, which exercises the patch.
2017-07-25Cleanup tests for last LLVM 2.9 referencesAndrea Mattavelli
2017-07-23Updated test cases to reflect removal of LLVM 2.9Martin Nowack
2017-06-08Merge pull request #667 from andreamattavelli/fix_macos_varargCristian Cadar
Removing flaky test Vararg.c from Darwin build until we find a proper…
2017-06-07Prevent test failure when realloc fails in test/Feature/Realloc.cAndrew Santosa
2017-06-05Removing flaky test Vararg.c from Darwin build until we find a proper fixAndrea Mattavelli
2017-06-05Fix test failure on systems with libstdc++ corresponding to gcc7.Dan Liew
This fixes #664. As reported by @jirislaby the `test/Feature/LongDouble.cpp` test fails to compile with Clang 3.4 due to new changes the libstdc++ headers. This ends up giving errors like ``` In file included from /home/abuild/rpmbuild/BUILD/klee-1.3.0+20170409/test/Feature/LongDouble.cpp:12: In file included from /usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/cstdlib:77: /usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/bits/std_abs.h:101:3: error: unknown type name '__float128' __float128 ^ /usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/bits/std_abs.h:102:7: error: unknown type name '__float128' abs(__float128 __x) ^ 2 errors generated. ``` Clang 4.0 seems fine with this source file so the problem has already been addressed upstream so we don't need to file a bug. We just need to move to a newer LLVM version to fix this properly! To work around this the test has been made into a C program rather than a C++ program to avoid including the C++ headers. The program wasn't using any important C++ features anyway so this seems like a sensible change.
2017-03-15Fix test case for OSX: only weak aliases are supported on darwinAndrea Mattavelli
Rewritten tests by replacing 'XFAIL: darwin' with 'REQUIRES: not-darwin'
2017-03-01Updated test cases that check warning messages.Cristian Cadar
2017-02-14Merge pull request #574 from delcypher/read_expr_missed_constaint_foldAndrea Mattavelli
ReadExpr::create() was missing an opportunity to constant fold
2017-02-14ReadExpr::create() was missing an opportunity to constant fold when handling ↵Dan Liew
constant arrays.
2017-02-10test: fix broken Vararg testMartijn Thé
The helper function had int return type, while no value was being returned. Signed-off-by: Jiri Slaby <jslaby@suse.cz>
2017-01-08tests: Added substitution for llvm-arAdrian Herrera
Brings llvm-ar into line with llvm-as and lli, removing the assumption that llvm-ar is installed system wide
2016-11-23Renamed .pc to .kquery (kleaver query)Eric Rizzi
2016-11-09Fix BFS searcherMartin Nowack
For performance reasons, if KLEE branches, one state is reused and it is progressed by adding new constraints. Make sure both new states end up at the end of the BFS searcher queue.