about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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
2023-06-05docs/CMakeLists.txt: drop support for old CMake versionsJulian Büning
minimum CMake version is 3.16.0 as of 3a0e434dc9d4053d75e9c0bbe6faa6dfb46717ae
2023-06-05CMake: remove obsolete commentsJulian Büning
obsoleted by changes in 3ef5c9d0cd51babb7c4ec2d7bb76d0cb7e47a65c
2023-06-05CMake: remove obsolete KLEE_COMPONENT_EXTRA_LIBRARIESJulian Büning
This variable was previously used by `klee_add_component()`, which got removed as part of 3ef5c9d0cd51babb7c4ec2d7bb76d0cb7e47a65c.
2023-06-05CMake: remove unused TARGET_LIBS variableJulian Büning
It appears that this variable was never used, already when it was first set in 7e75b491d389c15d48a5cfc455ba9442d7c108ed.
2023-05-26Copy stats to test directory when running testsDaniel Schemmel
The sqlite3 databases used for the stats are journalled and potentially must be written to. Therefore, the sqlite3 driver used by `klee-stats` requires write permissions on the database files. By copying the stats files to the test directory, we can now compile and test an out-of-tree build without requiring any write permissions on the source folder at all.
2023-05-26Some basic refactoring and pass through comments. In particular, it brings ↵Cristian Cadar
some related code together (deadline with EntryPoint and ReplayPathFile respectively) which was unnecessarily separated.
2023-05-26Refactored and fixed the code dealing with the entry point.Cristian Cadar
main() should not be processed if the entry point is a different function. This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (#1572)
2023-05-26add unsized free to kdallocDaniel Schemmel
2023-05-26Improve LOH deallocation schemeDaniel Schemmel
2023-05-26Improve error message when KDAlloc fails to create a mappingDaniel Schemmel
2023-05-26Add `getMapping` primitive to allocator directlyDaniel Schemmel
2023-05-26Add `getSize` primitive to kdallocDaniel Schemmel
2023-05-26prevent assertions from failing unnecessarilyDaniel Schemmel
2023-05-26Write `Control::meta` in C++17 styleDaniel Schemmel
2023-05-26Use unique_ptr for MemoryManager and avoid re-creating it in the first placeMartin Nowack
No need to re-create and re-alloc all the memory again after execution.
2023-05-26Cleaned up and updated codecov file.Cristian Cadar
2023-04-21Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency ↵Cristian Cadar
with recent changes.
2023-04-21Replaced "-data" and "-stat" by "_data" and "_stat" in the ktest-(rand)gen ↵Cristian Cadar
tools for consistency with recent changes.
2023-04-21use unique_ptr all throughout the solver chainDaniel Schemmel
2023-04-21use unique_ptr in SolverDaniel Schemmel
2023-04-21use unique_ptr in QueryLoggingSolverDaniel Schemmel
2023-04-21use unique_ptr in IndependentSolverDaniel Schemmel
2023-04-21use unique_ptr in CexCachingSolverDaniel Schemmel
2023-04-21use unique_ptr in AssignmentValidatingSolverDaniel Schemmel
2023-04-21use unique_ptr in CachingSolverDaniel Schemmel
2023-04-21use unique_ptr in StagedSolverImplDaniel Schemmel
2023-04-21use unique_ptr in Z3SolverImplDaniel Schemmel
2023-04-21use unique_ptr in ValidatingSolverDaniel Schemmel
2023-04-21use unique_ptr in STPSolverImplDaniel Schemmel
2023-04-20Remove additional quotation marksMartin Nowack
2023-04-20ensure that the right mt19937 constructor is chosen during overload resolutionDaniel Schemmel
2023-04-20remove unused rng adaptor functionsDaniel Schemmel
2023-04-20use `std::mt19937` instead of the custom implementationDaniel Schemmel