about summary refs log tree commit diff homepage
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-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-26tests: add some missing headersFrank Busse
2023-03-26fix unused variables warningDaniel Schemmel
2023-03-23Fix detection and installation of Ubuntu-provided llvm/clang packagesMartin Nowack
2023-03-23Transition to GitHub Container Registry hostingMartin Nowack
2023-03-23fix unused variable warningDaniel Schemmel
2023-03-23Remove model_version from the POSIX runtime, as we have never used it.Cristian Cadar
2023-03-23tests: add Feature/KleeStatsTermClasses.cFrank Busse
2023-03-23stats: add termination class statsFrank Busse
2023-03-23tests: add Feature/KleeStatsBranches.cFrank 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-23Run KDAlloc/rusage unittest a few times to allow for swapfile interferenceDaniel Schemmel
2023-03-22Added more test cases for --entry-point. EntryPointMissing is currently ↵Cristian Cadar
expected to fail.
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-22use C++17Julian Büning
2023-03-22Require minimal version of CMake 3.16 for KLEEMartin Nowack
This is the default version for Ubuntu 20.04 and should be available for most distributions. Moreover this should allow to move STP forward with their changes. (https://github.com/stp/stp/issues/375#issuecomment-889178863)
2023-03-22Remove hard to understand and debug pcregrep testCristian Cadar
2023-03-22klee-stats: improve error message for missing tabulate packageFrank Busse
2023-03-22Fixed typoMartin Nowack
2023-03-22Handle fail of KLEE gracefullyMartin Nowack
Under 64bit architecture, a ptr-error might be found. Ignore this for now.
2023-03-22Explicitly check if 32bit support is enabled for testingMartin Nowack
Ignore test in the first place, if no 32bit is enabled.
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: port test/Feature/VarArgByVal.c to LLVM 14Lukáš Zaoral
LLVM 14 has introduced the noundef function argument attribute.
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-20llvm14: Add LLVM 14 job to GitHub ActionsLukáš Zaoral
2023-03-20llvm14: Add LLVM 14 to lit.cfgLukáš Zaoral
2023-03-17Update KDAlloc unittestsMartin Nowack
2023-03-17Update CI componentsMartin Nowack
* Use Ubuntu 22.04 instead of 18.04 * Use LLVM 11 instead of 9 * Use TCMalloc 2.9.1 * Use Z3 4.8.15 * Use Sqlite3 3400100 Clean-up comments and structure to satisfy yaml linter
2023-03-17Fix script to build all the containers we require for GitHub actionsMartin Nowack
2023-03-17Update Docker build componentsMartin Nowack
* Use Ubuntu 22.04 * Use newer TCMalloc 2.9.1 * use Z3 4.8.15 * Use SQLite 3400100
2023-03-17Use newer LLVM_DIR config option to build FreeBSDMartin Nowack
2023-03-17Don't fail `KleeStats.c` test if it takes 1s or longerMartin Nowack
2023-03-17Disable `const_array_opt1` for ubsan as wellMartin Nowack
2023-03-17Fix uninitialised memory access while reading last path entryMartin Nowack
`>>` can fail and sets internal error information in the istream. Check the state of istream before pushing the value onto the buffer.
2023-03-17Fix building of runtime library and klee-replayMartin Nowack
Former build system provided additional flags for building bitcode while they were not required, e.g. under BSD or MacOS.
2023-03-17Add support to disable memsan instrumentation; update UB/Asan suppressionMartin Nowack
2023-03-17Update build scriptsMartin Nowack
* Support for Ubuntu 22.04 * Remove support for Python2 * Better separation between sanitizer builds and non-sanitizer builds * Fix build of metaSMT on newer Ubuntu versions * Use ninja to build LLVM * Simplifying building arbitrary LLVM configurations, e.g. different LLVM sanitizer builds (MemSan, UBSan, ASan) * Use MemSan with origin tracking * Build sqlite3 container correctly * Add support to provide sqlite3 version number
2023-03-17[MemSan] Mark memory objects modified by syscalls as initialisedMartin Nowack
2023-03-17Fix compiler warning with newer compilersMartin Nowack
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-26 00:11:20 +0000