Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-03-19 | Add Read consistency test case, spelling | Timotej Kapus | |
2019-03-18 | Disable optimisation for functions that contain KLEE calls | Martin Nowack | |
Compilers are allowed to hoist function calls and do GVE. This is currently done even without `--optimization` enabled. This is unfortunate in the context of KLEE function calls that might depend on specific code position without direct control flow dependencies. In such cases, function calls can be hoisted. To circumvent this, disallow to optimise functions that contain such calls by default. This might reduce optimisation for some functions containing such function calls but still allows it for all others. This patch adds an additional pass, that detects all functions starting with a prefix `klee_` and disable optimisations for functions containing such calls. This is enabled by default but can be disabled by `--klee-call-optimisation=false`. | |||
2019-03-18 | make test/Feature/srem.c more explicit | Julian Büning | |
2019-03-17 | Fix libc++ testcases | Martin Nowack | |
* remove wrapper script invocation and script * add build instruction to test cases * added additional checks * add check to avoid execution of tests if KLEE is not compiled with libc++ | |||
2019-03-17 | Added libcxx flag | Lukas Wölfer | |
2019-03-15 | Renamed --seed-out to --seed-file and --seed-out-dir to --seed-dir, and ↵ | Cristian Cadar | |
placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace. | |||
2019-03-13 | Renamed --no-output to --write-no-tests and placed it in the test case ↵ | Cristian Cadar | |
category (with --write-cov, --write-cvcs etc.) | |||
2019-03-12 | Exclude testcases not compatible with MSan | Martin Nowack | |
2019-03-12 | Add support to compile KLEE with MemorySanitizer (MSan) | Martin Nowack | |
2019-03-12 | Fixed comments to objectsize.ll and objectsize.leq49.ll | Cristian Cadar | |
2019-03-12 | Removed unneeded and confusing disable-opt option, reformatted Optimize() ↵ | Cristian Cadar | |
function and updated some .ll tests to use --optimize=false instead of --disable-opt | |||
2019-03-07 | tests: rename xxclang to clangxx | Frank Busse | |
2019-03-07 | Renamed %llvmgcc and %llvmgxx to %clang and %clangxx respectively. | Cristian Cadar | |
2019-03-05 | add regression test for LLVM PR39177 | Julian Büning | |
2019-03-05 | fix Executor::initializeGlobals for aliases pointing to another alias | Julian Büning | |
2018-12-19 | regression/2014-09-13-debug-info.c: use 'int: ' instead of 'data:' | Frank Busse | |
2018-12-19 | Various fixes for ktest-tool | Frank Busse | |
* switch to Python 3 * add file encoding * some PEP8 reformatting * fix TOCTOU for open * replace trimZeros() with rstrip * remove unused pos/args variables * remove --write-ints (print by default) * remove progname section (unused) * added/modified output rows - "data:" now shows the Python representation (for use in scripts) - "hex :" shows the hex representation - "text:" shows ASCII, all out-of-range/non-printable characters are replaced by a dot - "int :"/"uint:" print (unsigned) 8/16/32/64 bit integers * reduce width for object counter to needed minimum instead of 4 * refactor printing into function | |||
2018-12-19 | Added checks option category, moved --optimize to starting category, renamed ↵ | Cristian Cadar | |
original --run-in option to --running-dir | |||
2018-12-19 | Renamed --stop-after-n-instructions to --max-instructions, as suggested by @251 | Cristian Cadar | |
2018-11-23 | Implemented memalign with alignment | Lukas Wölfer | |
2018-11-06 | fix: actually set -O0 in test/concrete/CMakeLists.txt | Julian Büning | |
`-O0` has to be used in conjunction with, not instead of `-Xclang -disable-O0-optnone` | |||
2018-11-05 | Fixed crash on zero size arrays | Lukas Wölfer | |
2018-11-05 | Check for stack overflow in a tested program | Martin 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-02 | Added test for the case where external calls are encountered but disallowed | Cristian Cadar | |
2018-11-02 | Replaced --no-externals and --allow-external-sym-calls with ↵ | Cristian Cadar | |
--external-calls, updated tests accordingly, and improved documentation on external calls | |||
2018-11-02 | The test DeterministicSwitch.c does not need to allow external symbolic calls | Cristian Cadar | |
2018-10-29 | add %OOopt to recently added tests and Concrete | Julian Büning | |
2018-10-26 | Added gen-bout tool to generate ktest file (file.bout) using specified ↵ | Andrew Santosa | |
concrete arguments and files. * Sample use cases: * Using an interesting input as a seed, such as a crashing input. * Analyzing the path condition of a crashing input. * Also added the test: test/Runtime/POSIX/GenBout.c | |||
2018-10-26 | llvm5: test, add -disable-O0-optnone to -O0 | Jiri Slaby | |
Otherwise optimizations done in klee won't have any effect. Signed-off-by: Jiri Slaby <jirislaby@gmail.com> | |||
2018-10-26 | llvm5: test, change objectsize | Jiri Slaby | |
@llvm.objectsize has now three aguments, so fix the tests accordingly. Signed-off-by: Jiri Slaby <jirislaby@gmail.com> | |||
2018-10-24 | Add testcase for shift check | Martin Nowack | |
Validate non-optimised and optimised variant of added checks. | |||
2018-10-24 | Add test case for div checker | Martin 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-24 | Added lowering pass | Rafael Zaehl | |
2018-10-23 | Added support for KLEE value-based array optimization | Andrea Mattavelli | |
2018-10-23 | Added support for KLEE index-based array optimization | Andrea Mattavelli | |
2018-10-17 | tests: disable CompressedExprLogging on zlib-less systems | Frank Busse | |
2018-10-10 | fix handling of failing external calls | Frank Busse | |
Currently KLEE only handles the first segfault in external calls as it doesn't unblock SIGSEGV afterwards. This patch unblocks the signal and enables handling of multiple failing calls. | |||
2018-10-10 | cmake/lit: add asan/non-asan, ubsan/non-ubsan flags | Frank Busse | |
2018-10-08 | add support for klee-replay on OSX | Frank Busse | |
* also adds klee-replay as dependency for systemtests | |||
2018-09-30 | Fix a crash when the last running state is terminated during merging | Lukas Wölfer | |
2018-09-29 | Changed code to create up to 100 properly-numbered symbolic arguments, and ↵ | Cristian Cadar | |
add a corresponding check. | |||
2018-09-29 | Add checks for correct usage of the POSIX model, together with an associated ↵ | Cristian Cadar | |
test. | |||
2018-09-20 | Removed unused --sym-files 0 0 argument from FD_Fail test and rewrote the ↵ | Cristian Cadar | |
test to use FileCheck instead of grep | |||
2018-09-20 | Updated IoCtl test to use --sym-stdin instead of --sym-files 0 x to make ↵ | Cristian Cadar | |
stdin symbolic and removed unused arguments to main. | |||
2018-09-20 | Updated DirSeek test to use --sym-stdin instead of --sym-files 0 x to make ↵ | Cristian Cadar | |
stdin symbolic. | |||
2018-09-10 | Add testcase to run POSIX environment and main without arguments | Martin Nowack | |
2018-09-10 | Add POSIX runtime as dependency for the test case | Martin Nowack | |
2018-09-10 | Unify the error message if that function has not been found. | Martin Nowack | |
2018-09-06 | Use FileCheck and LINE instead of grep if possible | Martin Nowack | |
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers. | |||
2018-09-06 | runtime: fix memory error in canonicalize_file_name | Frank Busse | |
Fixes #46 and reverts #47. As stated in #46, the solution works for musl, glibc etc. However, the code in stub.c is executed by uclibc and uclibc doesn't allocate the target buffer in realpath. The memory error occured while running df for 10min with DFS. |