about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
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
2022-06-30remove LLVM < 9Frank Busse
2022-06-28Implement getArrayForUpdate iterativelyDaniel Schemmel
2022-06-26Intrinsics: Add support for @llvm.f{ma,muladd}.f*Lukáš Zaoral
2022-06-15Spelling Fixesm-davis
2022-06-13.err files: minor readability changes to stack trace outputFrank Busse
2022-06-13Update SpecialFunctionHandler.cppChaoqi Zhang
use size() to get N in bind(), just like the way in prepare().
2022-05-05cl flags: document default values, remove dead option: --replay-keep-symbolicFrank Busse
2022-04-25use mallinfo2 if availableFrank Busse
2022-04-01Remove unnecessary call to deprecated function sqlite3_enable_shared_cacheCristian Cadar
2022-03-21Fixed a wrong type when computing memory usage on macOSCristian Cadar
2022-03-17remove obsolete KLEE_LLVM legacy definesJulian Büning
2022-03-17LLVM < 6 leftoversJulian Büning
2022-03-17remove LLVM < 6 from sourcesFrank Busse
2022-03-17Fixed GetTotalMallocUsage on macOS to look at all zones. (The test ↵Cristian Cadar
MemoryLimit.h fails on macOS 12.1 without this fix.)
2022-03-09Core/Executor: Fix unaligned write of fp80 argumentsLukáš Zaoral
... in Executor::callExternalFunction. Fixes the following error reported in Feature/VarArg{Alignment,LongDouble}.c tests: lib/Expr/Expr.cpp:366:5: runtime error: store to misaligned address 0x7ffc011d3528 for type 'long double', which requires 16 byte alignment
2022-03-09Core/ExecutionState: Fix uninitialized reads in unit testsLukáš Zaoral
... by initialising all members of fundamental types of the ExecutionState class. Fixes the following error in SearcherTest.{Two,}RandomPath unit tests: lib/Core/ExecutionState.cpp:114:22: runtime error: load of value 254, which is not a valid value for type 'bool'
2022-01-07stats: remove reachableUncovered (unused)Frank Busse
2022-01-06Comment the code dealing with un/flushed bytes, and resolve old naming issue ↵Cristian Cadar
by renaming flushMask to unflushedMask
2022-01-05introduce BranchTypesFrank Busse
2022-01-05Remove outdated reference to klee_make_symbolic_nameCristian Cadar
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 15:08:25 +0000