about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2024-01-12new: persistent ptree (-write-ptree) and klee-ptreeFrank Busse
Introduce three different kinds of process trees: 1. Noop: does nothing (e.g. no allocations for DFS) 2. InMemory: same behaviour as before (e.g. RandomPathSearcher) 3. Persistent: similar to InMemory but writes nodes to ptree.db and tracks information such as branch type, termination type or source location (asm) in nodes. Enabled with -write-ptree ptree.db files can be analysed/plotted with the new "klee-ptree" tool.
2023-10-23replace deprecated (as of c++20) std::is_pod with std::trivial && ↵Daniel Schemmel
std::is_standard_layout
2023-09-11Make KDAlloc the default memory allocatorCristian Cadar
2023-09-11Changed use-after-free and double-free tests to expect KDAlloc, plus some ↵Cristian Cadar
small improvements.
2023-09-07Remove broken experimental optimisation for validity (--cex-cache-exp)Cristian Cadar
2023-07-21Add code to only keep in the --help menu the KLEE/Kleaver option categoriesCristian Cadar
2023-07-21Move some options to the klee namespace and declare them in OptionCategories.hCristian Cadar
2023-07-12Replaced --suppress-external-warnings and --all-external-warnings with ↵Cristian Cadar
--external-call-warnings=none|once-per-function|all. This eliminates the ambiguity when both of the old options were set. Added test for the new option.
2023-07-10remove timings from kdalloc testsDaniel Schemmel
2023-07-10Simplify KDAlloc testsDaniel Schemmel
2023-07-08Combine all `ConstantExpr::toMemory` cases into one.Daniel Schemmel
Note that (as it did previously), this relies on the native types having the same internal representation as the ApInt type.
2023-07-08Using std::memcpy prevents alignment problems and removes an unnecessary ↵Daniel Schemmel
special case
2023-07-06Implement getLocationInfo in the same style as getSizeDaniel Schemmel
2023-07-06Have CoWPtr::get and CoWPtr::getOwned return pointers instead of referencesDaniel Schemmel
2023-07-06rename Allocator::location_info to Allocator::locationInfo forDaniel Schemmel
consistency
2023-07-06Perform location_info tests in KDAlloc's random testDaniel Schemmel
2023-06-26RefTest: suppress -Wself-moveJulian Büning
This warning (introduced with GCC 13, also present in clang) warns precisely about what we want to test here.
2023-06-26Consistently use ".ktest" when referring to .ktest files in the help menuCristian Cadar
2023-06-26Remove parentheses around klee_ intrinsics from the help menuCristian Cadar
2023-06-26Fixed a couple of spelling issues in the help menuCristian Cadar
2023-06-26Improved help message for --exit-on-error-type=AbortCristian Cadar
2023-06-11Rewrote has_permission in the POSIX runtime. We now only return with ↵Cristian Cadar
permission error a single time in symbolic execution mode. The rewrite also fixes a bug reported in #1230. Rewrote the FilePerm.c test accordingly.
2023-06-11SpecialFunctionHandler: use std::array for handlerInfoJulian Büning
2023-06-11fix ktest-randgen: use after freeJulian Büning
2023-06-09Fixed a format specifier pointed to by a compiler warning.Cristian Cadar
2023-06-07Changed version to 3.1-preCristian Cadar
2023-06-07Release notes for KLEE 3.0 v3.0 3.0.xCristian Cadar
2023-06-07Set version number to 3.0Cristian Cadar
2023-06-07Fixed end date in the 2.3 release notesCristian Cadar
2023-06-07Build and push Docker image as part of a releaseMartin Nowack
2023-06-07Use recommended LLVM 13 as part of the Docker imageMartin Nowack
2023-06-07unittests/CMakeLists.txt: set gtest include dir only if necessaryJulian Büning
2023-06-07unittests/CMakeLists.txt: do not echo GTEST_SRC_DIR on errorJulian Büning
This prevents the error message to include the internal "GTEST_SRC_DIR-NOTFOUND" value.
2023-06-07unittests/CMakeLists.txt: no UNITTEST_MAIN_LIBSJulian Büning
variable obsoleted by 5607a7f1910e579acc0b93b1ae2caba88e7d5fd7
2023-06-07unittests/CMakeLists.txt: remove obsolete policyJulian Büning
Checking for policy CMP0077 is obsolete as we now require CMake 3.16.0 as minimum version.
2023-06-07unittests/CMakeLists.txt: fix LLVM find_package supportJulian Büning
broken by 3ef5c9d0cd51babb7c4ec2d7bb76d0cb7e47a65c, which removed the "USE_CMAKE_FIND_PACKAGE_LLVM" variable and no longer includes AddLLVM.cmake
2023-06-07unittests/CMakeLists.txt: gtest check for LLVM 13+Julian Büning
We previously used `LLVM_EXPORTED_TARGETS` defined in LLVMConfig.cmake. This variable is no longer defined starting from LLVM 13. Alternatively, we use the fact that LLVM's gtest target always depends on LLVMSupport.
2023-06-06ktest-gen: remove unused functionFrank Busse
2023-06-06Further improve KDAlloc memory usage with infinite quarantineDaniel Schemmel
2023-06-05test/Feature/StackTraceOutput.c: relative checks, clang-formatJulian Büning
2023-06-05re-enable StackTraceOutput.c testJulian Büning
This test previously had a REQUIRES line with geq-llvm-7.0. Because LLVM version 7.0 is no longer "known" (test/lit.cfg), the required feature is not available and the test is discarded as unsupported by llvm-lit.
2023-06-05make BatchingSearcher more readableJulian Büning
2023-06-05fix BatchingSearcher's disabled time budgetJulian Büning
The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own.
2023-06-05also check for default CHECK directive in ArrayOpt TestsMatthis Gördel
2023-06-05CMake: use check_c_source_compiles() for FSTATAT_PATH_ACCEPTS_NULLJulian Büning
is a bit more convenient and avoids an extra file
2023-06-05config.h: include FSTATAT_PATH_ACCEPTS_NULLJulian Büning
This variable was introduced by d2f5906da4ae37a41ae257e5308d50e19689877b but not included in `config.h` before. As a result `#ifdef` would always fail. Moving the code is necessary to set the variable before `config.h` is created using `configure_file()` in CMakeLists.txt.
2023-06-05.clang-format: c++17Julian Büning
From the `clang-format` documentation: - "`Cpp11` is a deprecated alias for `Latest`" - `Latest`: "Parse and format using the latest supported language version."
2023-06-05doxygen.cfg.in: DOXYGEN_OUTPUT_DIRJulian Büning
resolves a FIXME to streamline doxygen.cfg generation a bit
2023-06-05CMake: use built-in FindSQLite3 moduleJulian Büning
available since CMake version 3.14
2023-06-05README-CMake.md: clean up top-level targetsJulian Büning
* the old build system is long gone * clean_doxygen was removed by d5cbc2002bbf75f08036f7adf861b027768a0622 * clean_runtime was removed by 6156b4eeb9a429ccc370782d719d0d6c787a6f72 * clean_all was removed by a00424e64d56ff881a72bfd99ea0dbcbe6898b49