about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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-20Remove additional quotation marksMartin Nowack
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-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-14ci: run ShellCheck on `*.inc` shell scriptsJan Macku
2023-04-14Modify name of variables in generated cvc files.ITWOI
2023-04-06Disable "disabling of warnings" for LLVM >= 14Martin Nowack
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-30fix CMake: -UNDEBUGJulian Büning
2023-03-27ci(lint): add shell linter - Differential ShellCheckJan Macku
It performs differential ShellCheck scans and report results directly in pull request. documentation: https://github.com/redhat-plumbers-in-action/differential-shellcheck Signed-off-by: Jan Macku <jamacku@redhat.com>
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 12:17:31 +0000