about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
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.
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-20ConstantArrayExprVisitor: Deduplicate `visitConcat` and `visitRead`Lukáš Zaoral
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-20llvm14: TargetRegistry.h was moved from Support to MCLukáš Zaoral
2023-03-17Fix compiler warning with newer compilersMartin Nowack
2023-03-17[cmake] Use LLVM's CMake functionality onlyMartin Nowack
LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0).
2023-03-16Integrate KDAlloc into KLEEDaniel Schemmel
2023-03-16The KDAlloc slot allocator is useful for small sized allocationsDaniel Schemmel
2022-09-26Improve the message for when large arrays become symbolic. Only print this ↵Cristian Cadar
warning once per array. Add test case.
2022-09-24Pass llvm.experimental.noalias.scope.decl to IntrinsicLowering so that it ↵Pavel
strips out these intrinsics
2022-09-14Eliminate .undefined_behavior.err category and simplify testsPavel
2022-09-14Introduce separate categories for different kinds of undefined behaviorPavel
2022-09-14Support UBSan-enabled binariesPavel Yatcheniy
2022-08-26Use true instead of Z3_TRUE (removed in z3 4.11.0)Jerry James
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-30rename CallSite to CallBaseFrank Busse
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 06:33:31 +0000