| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-02-29 | Test case for externally concretized variables and constraint fully symbolic ↵ | Martin Nowack | |
| variables The test case is based on the example provided by Mingyi Liu from the KLEE mailing list. | |||
| 2024-02-29 | Release notes for KLEE 3.1 | Cristian Cadar | |
| 2024-02-29 | Set version number to 3.1 | Cristian Cadar | |
| 2024-02-28 | Compare LLVM_VERSION_SHORT to "140" rather than "14". | Michael Herstine | |
| In commit 2b07721, support was added to p-libcxx.inc & p-llvm.inc for LLVM versions 14+ (in which, apparently, certain build flags were changed). To detect these recent versions, the variable LLVM_VERSION_SHORT was compared numerically to "14"-- the intent obviously being to express "LLVM version 14 or later". However, in both v-clang.inc & v-llvm.inc, LLVM_VERSION_SHORT is defined as the concatenation of LLVM_VERSION_MAJOR and LLVM_VERSION_MINOR. Therefore, on a machine with, say, LLVM 13.0 installed, LLVM_VERSION_SHORT will be "130" which compares as larger than "14". This patch changes the comparison to be against "140". | |||
| 2024-02-27 | Small refactorings and reformatting in callExternalFunction | Cristian Cadar | |
| 2024-02-27 | Simplified callExternalFunction by using toConstant instead of getValue | Cristian Cadar | |
| 2024-02-27 | Extend toConstant() to take an additional boolean argument that decides ↵ | Cristian Cadar | |
| whether the expression is concretised. Also changed a C string argument to std::string. | |||
| 2024-02-27 | This commit fixes the concretization of arguments following an external call ↵ | Cristian Cadar | |
| with symbolic arguments. It also introduces a new external call policy, where the symbolic inputs are left unconstrained following such a call, useful for certain external calls such as printf. | |||
| 2024-02-27 | Two test cases exercising two policies for calling external calls with ↵ | Cristian Cadar | |
| symbolic arguments. One of them is currently expected to fail. | |||
| 2024-02-19 | Rename --ptree-batch-size to --exec-tree-batch size, and ↵ | Cristian Cadar | |
| --compress-execution-tree to --compress-exec-tree. Fix an incorrect reference to --write-exec-tree. | |||
| 2024-02-17 | Remove the not Darwin requirement for the test TargetMismatch.c | Cristian Cadar | |
| 2024-02-17 | Fixed incorrect reference in ExternalCallWarnings | Cristian Cadar | |
| 2024-02-16 | drop llvm 9 and 10 | Daniel Schemmel | |
| 2024-02-12 | Fix brittleness in Feature/VarArgByVal test | Daniel Schemmel | |
| 2024-02-08 | Add space between include and main function for updated test cases | MartinNowack | |
| Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com> (cherry picked from commit 1ea1a7576300a4da01d925df42db109660ef54d2) | |||
| 2024-02-08 | Mention default value in help text for `--strip-all` and `--strip-debug` | MartinNowack | |
| Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com> (cherry picked from commit 5d61fb6114bafbf67c59899d15e397684d4ceb28) | |||
| 2024-02-08 | Use `std::` namespace for `uint64_t` | MartinNowack | |
| Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com> (cherry picked from commit 5d9af025ee5a01b1650f11ed0612a10357a98308) | |||
| 2024-02-08 | Enable CI to test newer LLVM versions | Martin Nowack | |
| 2024-02-08 | Support newer LLVM versions in `lit` | Martin Nowack | |
| 2024-02-08 | Update test case for expressions using `udiv`, `urem`, `sdiv` and `srem` | Martin Nowack | |
| They are not supported anymore for newer LLVM versions. | |||
| 2024-02-08 | Handle check for thrown libc++ exceptions more general | Martin Nowack | |
| The wording changed slightly in newer versions. Update the test case to support this. | |||
| 2024-02-08 | Disable `2018-10-30-llvm-pr39177.ll` for newer LLVM versions. | Martin Nowack | |
| The optimiser generates different code and calls fwrite directly instead. | |||
| 2024-02-08 | Disable unsupported passes for newer LLVM versions | Martin Nowack | |
| Similar functionality needs to be added using a new pass manager | |||
| 2024-02-08 | Add support to `aligned_alloc` generated by LLVM | Martin Nowack | |
| Handle like `memalign` for now. | |||
| 2024-02-08 | Add support for `Intrinsic::get_rounding` for LLVM 16 | Martin Nowack | |
| `Intrinsic::flt_rounds` got removed | |||
| 2024-02-08 | Use APIs of newer LLVM versions instead of unsupported ones | Martin Nowack | |
| 2024-02-08 | Fix test case: using unsupported `CHECK_NEXT` instead of `CHECK-NEXT` | Martin Nowack | |
| 2024-02-08 | Fix test cases to support opaque pointers | Martin Nowack | |
| 2024-02-08 | Add support for opaque pointers | Martin Nowack | |
| 2024-02-08 | Explicitly enable opaque pointer support for LLVM 15 | Martin Nowack | |
| This automatically lifts old-style pointers to opaque pointers. More recent versions use opaque pointers automatically and do not need an explicit enabling. | |||
| 2024-02-08 | Explicitly build KLEE's exception handling runtime with C++11 | Martin Nowack | |
| Currently, we assume C++11 support being used to by the tested software. This needs to change if newer C++ standards should be supported. | |||
| 2024-02-08 | Assume C compiler's default standard is `-std=gnu17` | Martin Nowack | |
| Newer compilers use `-std=gnu17` as the default when compiling C code. Fix all the test cases that violate this behaviour or explicitly request older standards `-std=c89` where necessary. | |||
| 2024-02-08 | Use KLEE's uClibc v1.4 as default to support the compilation with newer ↵ | Martin Nowack | |
| compilers | |||
| 2024-02-08 | Refactor invocation of old pass manager into legacy function | Martin Nowack | |
| 2024-02-08 | Fix `klee_eh_cxx.cpp` compiler error | Martin Nowack | |
| 2024-02-08 | Fix `klee-libc/memchr.c` compiler warning | Martin Nowack | |
| 2024-02-08 | Replace `%libcxx_include` with `%libcxx_includes` for multi-include directories | Martin Nowack | |
| To support multiple include directories for c++ header files, use `%libcxx_includes`. This string contains the `-I` compiler directive for each include path as well. Update test cases to use new directive. | |||
| 2024-02-08 | Add support for newer `libc++`; Simplify path detection | Martin Nowack | |
| `libc++` include headers are now split between platform dependent and platform independent code. Before, only include files for the platform independent code were considered. Add support to automatically find platform dependent includes as well. Simplify the detection of libraries and paths. Instead of pointing to the `v1` directory, pointing to the include directory for `-DKLEE_LIBCXX_INCLUDE_PATH` is enough. Update build script to support this as well. | |||
| 2024-02-08 | MERGE libc++ build system | Martin Nowack | |
| 2024-02-08 | Add support to build newer LLVM versions | Martin Nowack | |
| `-DLLVM_ENABLE_PROJECTS` does not include runtimes anymore, instead a `-DLLVM_ENABLE_RUNTIMES` should be used in addition | |||
| 2024-01-30 | Change `GetConstraintLog` to work with `std::string`s instead of `char*`s | Daniel Schemmel | |
| 2024-01-30 | Avoid generating array names in solver builders that could accidently collide | Martin Nowack | |
| If an array name ended with a number, adding a number-only suffix could generate the same name used as part of the solvers. In the specific testcase `val_1` became solver array `val_111` which collided with array `val_11` that became `val_111` as well. Using an `_` as prefix for the suffix, solves that problem in general, i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`. Fixes #1668 | |||
| 2024-01-30 | Modify getValueFromSeeds() to include more functionality and simplify its ↵ | Cristian Cadar | |
| callers | |||
| 2024-01-30 | Make Assignment::evaluate be const | Cristian Cadar | |
| 2024-01-30 | Add checks to the seed concretization tests about the expected number of queries | Cristian Cadar | |
| 2024-01-30 | Added a test for --allow-seed-extension | Cristian Cadar | |
| 2024-01-30 | Removed --zero-seed-extension, and merge it with --allow-seed-extension. ↵ | Cristian Cadar | |
| This reworked logic also fixes a buffer overflow which could be triggered during seed extension. | |||
| 2024-01-30 | Refactored some code related to seeding. | Cristian Cadar | |
| 2024-01-30 | On a symbolic allocation, retrieve size from a seed, if available | Cristian Cadar | |
| 2024-01-30 | Concretize arguments to external function calls using seeds, if available. ↵ | Cristian Cadar | |
| Added a test case. | |||
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |