Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-07-29 | Fixed incorrect requires directive | Cristian Cadar | |
2019-05-30 | fix tests for macOS | Julian Büning | |
2019-05-30 | implement FunctionAliasPass | Julian Büning | |
2019-05-30 | remove klee_alias_function() | Julian Büning | |
this function can be used to modify the control flow of the program on different paths, enabling self-modifying code. | |||
2019-05-06 | Add 'freebsd' feature in lit.cfg and use it to XFAIL LargeReturnTypes.cpp test. | Gleb Popov | |
2019-04-04 | Add klee-stats test, fix microseconds bug | Timotej Kapus | |
2019-03-21 | remove tests for LLVM <= 3.7 | Julian Büning | |
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-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 | 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 | fix Executor::initializeGlobals for aliases pointing to another alias | Julian Büning | |
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-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 | 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-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-17 | tests: disable CompressedExprLogging on zlib-less systems | Frank Busse | |
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 | Avoid Vararg non-deterministic allocation | Martin 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-01 | test: remove geq-llvm-3.4 | Julian Büning | |
2018-07-28 | remove last comma from -debug-print-escaping-functions | Julian Büning | |
2018-07-28 | test/Feature/EscapingFunctionsAlias.c: clarify alias(ee) casting | Julian Büning | |
2018-07-28 | add declarations to escapingFunctions | Julian Büning | |
2018-07-23 | ModuleUtil: improve and test valueIsOnlyCalled | Julian Büning | |
* handle BlockAddress (which is not a valid function pointer) * there is no instruction with opcode 0 * add test for functionality | |||
2018-07-12 | llvm38: test, change some tests | Jiri 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-11 | Removed 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-10 | test: remove undefined behaviour | Jiri 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-29 | Make ConstantExpr hashing function faster and modify affected test | Timotej Kapus | |
2018-05-24 | test: add versions of some tests for LLVM 3.7 | Richard 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-18 | tests: use names in klee_make_symbolic | Frank Busse | |
2018-05-17 | Improve error messages for ReadStringAtAddress | Timotej Kapus | |
2018-05-06 | Moved regression test to proper location. Fixes #705 | Cristian Cadar | |
2018-05-01 | add blockaddress and indirectbr instructions | Frank Busse | |
2018-03-23 | fix 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-18 | Add testcase for constant array handling | Martin Nowack | |
2017-11-24 | klee_make_symbolic: add test cases for API | Frank Busse | |
2017-10-15 | Fixed assert in BFSSearcher that does not hold as part of interleaved searcher | Julian Büning | |
2017-10-06 | Removed the word 'unsigned' from integer overflow error messages | Andrew Santosa | |
2017-08-09 | Merge pull request #742 from ccadar/fold | Cristian Cadar | |
Added checks for div/mod by zero and overshifts in constant expressio… |