about summary refs log tree commit diff homepage
path: root/test/Feature
AgeCommit message (Collapse)Author
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.
2016-08-10Extended support for assembler raisingMartin Nowack
Improved support for assembler handling. Providing additional triple information to raise assembler for supported architectures only. Implemented support for raising full assembly memory fence. Added initial support for memory fences in Executor.
2016-08-04klee: add exit-on-error-type parameterJiri Slaby
It allows stopping the execution on some conditions like assertions. The use is like: klee -exit-on-error-type=Assert -exit-on-error-type=External file.llvm This is especially useful in the SV-COMP. A test to cover the new parameter was added too. Signed-off-by: Jiri Slaby <jslaby@suse.cz>
2016-07-11Executor: do not crash on non-sized globalsJiri Slaby
Sometimes, globals are not sized and ->getTypeStoreSize on such type crashes inside the LLVM. Check whether type is sized prior to calling the function above. A minimalistic example of Y being unsized with no effect on the actual code is put to tests. [v2] Use klee_warning for printing. And use %.*s formatting string given StringRef.data() need not be null terminated. Signed-off-by: Jiri Slaby <jslaby@suse.cz>
2016-07-08Generate forked states for switch instructions deterministicallyMartin Nowack
This patch generates the states based on the order of switch-cases. Before, switch-constraints were randomly assigned to forked states. As generated code might be different between LLVM versions, we use the case values, order them, and iterate in that order over the cases. This way we can also support deterministic execution of older LLVM versions.
2016-07-08Use vector instead of set to add/remove statesMartin Nowack
Deterministic adding/removing of states.
2016-07-08Support gzip-based compression of raw_outstreamsMartin Nowack
Provide initial zlib-based compression support for raw_outstreams. Replacing llvm::raw_fd_outstreams with compressed_fd_outstreams automatically compresses data in gzip format before writing to file. Options added: * --compress-log to compress all query log files (e.g. *.pc, *.smt2) on the fly. Every query log file gets extended with .gz. * --debug-compress-instructions to compress logfile for instruction stream on the fly.
2016-05-18Modified -debug-print-instructions to allow to write directly on log file.Andrea Mattavelli
The option now contains 4 different options: 1) all:stderr, which logs all instructions to file in format [src, inst_id, llvm_inst]; 2) src:stderr, which logs all instructions to file in format [src, inst_id]; 3) compact:stderr, which logs all instructions to file in format [inst_id]; 4) all:file, which logs all instructions to file in format [src, inst_id, llvm_inst]; 5) src:file, which logs all instructions to file in format [src, inst_id]; 6) compact:file, which logs all instructions to file in format [inst_id]; Writing to file gives a speedup of ~50x.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 23:42:17 +0000