about summary refs log tree commit diff homepage
path: root/lib
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-09-11Make KDAlloc the default memory allocatorCristian Cadar
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-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-06rename Allocator::location_info to Allocator::locationInfo forDaniel Schemmel
consistency
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-11SpecialFunctionHandler: use std::array for handlerInfoJulian Büning
2023-06-09Fixed a format specifier pointed to by a compiler warning.Cristian Cadar
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-05CMake: use built-in FindSQLite3 moduleJulian Büning
available since CMake version 3.14
2023-05-26Improve error message when KDAlloc fails to create a mappingDaniel 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-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-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
2023-04-06Use newer C++ standard for KLEE's iterators; fixes deprecation warningMartin Nowack
2023-04-06Support disabling compiler warnings; Use with external headersMartin Nowack
2023-04-06Mark variable as potentially unusedMartin Nowack
2023-04-01remove include/klee/Support/IntEvaluation.hDaniel Schemmel
2023-03-30Prevent fallthrough warningDaniel Schemmel
2023-03-27Core/Executor: long double on i686 must be aligned to 4 bytesLukáš Zaoral
According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes. Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes were used. This commit fixes the following out of bound pointer access. ``` $ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc $ klee varalign.bc KLEE: output directory is "/home/lukas/klee/klee-out-19" KLEE: Using Z3 solver backend KLEE: WARNING: undefined reference to function: printf KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17 i1, i2, i3: 1, 2, 3 l1: 4 i4: 5 ld1: 6.000000 KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 499 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ```
2023-03-23stats: add termination class statsFrank Busse
2023-03-23stats: add branch type statsFrank Busse
2023-03-23stats: rename States -> ActiveStates, add StatesFrank Busse
2023-03-23stats: add AllocationsFrank Busse
2023-03-23stats: rename numQueries/Queries -> SolverQueries, add QueriesFrank Busse
2023-03-23stats: add ExternalCallsFrank Busse
2023-03-23stats: add QCacheHits/MissesFrank Busse
2023-03-23stats: add InhibitedForksFrank Busse
2023-03-23remove obsolete headerDaniel Schemmel
2023-03-22STP: add option to switch SAT solver: --stp-sat-solver and set default to ↵Frank Busse
CryptoMinisat
2023-03-22Change `llvm_map_components_to_libnames` to `llvm_config` CMake functionMartin Nowack
With recent LLVM versions, this should allow to link against dynamic LLVM libraries.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 07:13:45 +0000