about summary refs log tree commit diff homepage
path: root/include
AgeCommit message (Collapse)Author
2023-06-06Further improve KDAlloc memory usage with infinite quarantineDaniel Schemmel
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-05-26add unsized free to kdallocDaniel Schemmel
2023-05-26Improve LOH deallocation schemeDaniel 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-04-21use unique_ptr all throughout the solver chainDaniel Schemmel
2023-04-21use unique_ptr in SolverDaniel Schemmel
2023-04-21use unique_ptr in StagedSolverImplDaniel Schemmel
2023-04-20Remove additional quotation marksMartin Nowack
2023-04-20remove unused rng adaptor functionsDaniel Schemmel
2023-04-20use `std::mt19937` instead of the custom implementationDaniel Schemmel
2023-04-18change some obsolete KDAlloc commentsJulian Büning
- mappings were only shared in a former version of KDAlloc - `AllocationFactory(std::size_t, std::uint32_t)`'s second parameter is used for quarantine size, not the location of the mapping
2023-04-06Disable "disabling of warnings" for LLVM >= 14Martin 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-27(gcc-13) include cstdint for *int*_tJiri Slaby
Otherwise we see errors like this with gcc13: include/klee/Statistics/Statistic.h:31:10: error: no type named 'uint32_t' in namespace 'std'
2023-03-23stats: add termination class statsFrank Busse
2023-03-23stats: add branch type statsFrank Busse
2023-03-23stats: rename numQueries/Queries -> SolverQueries, add QueriesFrank Busse
2023-03-23remove obsolete headerDaniel Schemmel
2023-03-20ConstantArrayExprVisitor: Fix detection of multiple array indicesLukáš Zaoral
Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the `incompatible` flag would not be set. Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected: if ((array1[k] + array2[x] + array2[k]) == 0) Resulting in the following output: KLEE: WARNING: OPT_I: infeasible branch! KLEE: WARNING: OPT_I: successful
2023-03-20llvm14: PointerType::getElementType() was deprecatedLukáš Zaoral
... for LLVM 14 in [1] and has already been removed from the LLVM 15 branch in [2]. Some changes are only temporary to silence the warning though, as Type::getPointerElementType() is planned to be removed as well. [3] [1] https://reviews.llvm.org/D117885/new/ [2] https://github.com/llvm/llvm-project/commit/d593cf7 [3] https://llvm.org/docs/OpaquePointers.html#migration-instructions
2023-03-17Use bitcode library paths via config generation instead of `-D` flagsMartin Nowack
2023-03-16Add the KDAlloc allocator using both of its suballocatorsDaniel Schemmel
2023-03-16The KDAlloc loh allocator is useful for variable sized (large) allocationsDaniel Schemmel
2023-03-16The KDAlloc slot allocator is useful for small sized allocationsDaniel Schemmel
2022-09-14Eliminate .undefined_behavior.err category and simplify testsPavel
2022-09-14Introduce separate categories for different kinds of undefined behaviorPavel
2022-07-24Support arguments of width 128, 256 and 512 bits for external callsPavel
2022-07-04Inline asm external callMikhail
2022-07-04Fix memory leak in crosscheck core solver mechanismDaniel Schemmel
2022-06-30remove LLVM < 9Frank Busse
2022-04-28Make Uclibc support a runtime option, not a compile-time one.Gleb Popov
2022-04-25use mallinfo2 if availableFrank Busse
2022-03-17remove obsolete KLEE_LLVM legacy definesJulian Büning
2022-03-17ADT/Ref.h: remove headerFrank Busse
2022-03-17remove LLVM < 6 from sourcesFrank Busse
2022-03-17Document that GetTotalMallocUsage returns the usage in bytesCristian Cadar
2022-01-05introduce BranchTypesFrank Busse
2021-12-23Introduce termination categoriesFrank Busse
Track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated.
2021-05-04differentiate between partial and completed paths in summary and fix paths ↵Frank Busse
stats when not dumping states
2020-12-23klee.h: fix compiler warnings (function declaration is not a prototype)Frank Busse
2020-11-12Casting.h: isa_and_nonnull<>Julian Büning
2020-11-12Ref: implement operator bool()Julian Büning
2020-11-04Link to the different runtime libraries depending on the application to test.Martin Nowack
Currently, only 32bit vs. 64bit is supported.
2020-10-12Exception handling only for LLVM >= 8.0.0Julian Büning