| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-06-25 | Enforce fork/branch limits in branch() and fix double termination | Frank Busse | |
| * extend help messages for -max-memory and -max-memory-inhibit * introduces branchingPermitted() * enforces fork/branch limits in branch() (vector version) * changes main loop * calls updateStates() before checkMemoryUsage() * calls updateStates() again in case we early terminate states This should prevent double termination for now. Other solutions are imho more expensive as we would have to compare possibly large vectors of states (either states(arr) in checkMemoryUsage() or removedStates in terminateState()). | |||
| 2020-06-25 | fix Executor: initializeGlobalAliases | Julian Büning | |
| 2020-06-19 | Added test reported in https://github.com/klee/klee/issues/189 for byval ↵ | Cristian Cadar | |
| variadic arguments | |||
| 2020-06-19 | Renamed Vararg.c to VarArg.c for consistency with the other var arg tests ↵ | Cristian Cadar | |
| and reformatted comments. | |||
| 2020-06-19 | Added test checking for correct alignment of variadic arguments | Cristian Cadar | |
| 2020-06-19 | Added test checking that KLEE correctly handles variadic arguments with the ↵ | Cristian Cadar | |
| byval attribute | |||
| 2020-06-06 | [Module] Add testcase for inline asm lifting | Martin Nowack | |
| 2020-04-08 | test: add a new test for readStringAtAddress | Marek Chalupa | |
| Read strings from different parts of objects. | |||
| 2020-01-18 | Fix handling of debug information for functions | Martin Nowack | |
| Tracking function locations separately correctly without prefixing it with a directory. | |||
| 2020-01-13 | Assume assembly.ll is local to the run.istats file | Martin Nowack | |
| Assuming a `klee-out-*` directory is moved to a different path location, subsequent analysis of the run.istats with KCachegrind focusing on assembly is impossible as the `assembly.ll` cannot be found. The reason is that the absolute path of the object file (assembly.ll) is hard-coded as part of the generated run.istats. To fix this, assume that the file is local to the `run.istats`. | |||
| 2019-10-07 | test/Feature/SolverTimeout.c: re-enable for Z3 | Julian Büning | |
| 2019-09-20 | Move intrinsics tests to the proper directory | Mateusz Naściszewski | |
| 2019-09-20 | Add tests for saturating arithmetic | Mateusz Naściszewski | |
| 2019-07-30 | Use #include "klee/..." (instead of #include <klee/...>) consistently. | Cristian Cadar | |
| 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> | |||
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |