Age | Commit message (Collapse) | Author | |
---|---|---|---|
2023-05-26 | Write `Control::meta` in C++17 style | Daniel Schemmel | |
2023-05-26 | Use unique_ptr for MemoryManager and avoid re-creating it in the first place | Martin Nowack | |
No need to re-create and re-alloc all the memory again after execution. | |||
2023-05-26 | Cleaned up and updated codecov file. | Cristian Cadar | |
2023-04-21 | Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency ↵ | Cristian Cadar | |
with recent changes. | |||
2023-04-21 | Replaced "-data" and "-stat" by "_data" and "_stat" in the ktest-(rand)gen ↵ | Cristian Cadar | |
tools for consistency with recent changes. | |||
2023-04-21 | use unique_ptr all throughout the solver chain | Daniel Schemmel | |
2023-04-21 | use unique_ptr in Solver | Daniel Schemmel | |
2023-04-21 | use unique_ptr in QueryLoggingSolver | Daniel Schemmel | |
2023-04-21 | use unique_ptr in IndependentSolver | Daniel Schemmel | |
2023-04-21 | use unique_ptr in CexCachingSolver | Daniel Schemmel | |
2023-04-21 | use unique_ptr in AssignmentValidatingSolver | Daniel Schemmel | |
2023-04-21 | use unique_ptr in CachingSolver | Daniel Schemmel | |
2023-04-21 | use unique_ptr in StagedSolverImpl | Daniel Schemmel | |
2023-04-21 | use unique_ptr in Z3SolverImpl | Daniel Schemmel | |
2023-04-21 | use unique_ptr in ValidatingSolver | Daniel Schemmel | |
2023-04-21 | use unique_ptr in STPSolverImpl | Daniel Schemmel | |
2023-04-20 | Remove additional quotation marks | Martin Nowack | |
2023-04-20 | ensure that the right mt19937 constructor is chosen during overload resolution | Daniel Schemmel | |
2023-04-20 | remove unused rng adaptor functions | Daniel Schemmel | |
2023-04-20 | use `std::mt19937` instead of the custom implementation | Daniel Schemmel | |
2023-04-18 | change some obsolete KDAlloc comments | Julian 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-14 | ci: run ShellCheck on `*.inc` shell scripts | Jan Macku | |
2023-04-14 | Modify name of variables in generated cvc files. | ITWOI | |
2023-04-06 | Disable "disabling of warnings" for LLVM >= 14 | Martin Nowack | |
2023-04-06 | Use newer C++ standard for KLEE's iterators; fixes deprecation warning | Martin Nowack | |
2023-04-06 | Support disabling compiler warnings; Use with external headers | Martin Nowack | |
2023-04-06 | Mark variable as potentially unused | Martin Nowack | |
2023-04-01 | remove include/klee/Support/IntEvaluation.h | Daniel Schemmel | |
2023-03-30 | Prevent fallthrough warning | Daniel Schemmel | |
2023-03-30 | fix CMake: -UNDEBUG | Julian Büning | |
2023-03-27 | ci(lint): add shell linter - Differential ShellCheck | Jan 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-27 | Core/Executor: long double on i686 must be aligned to 4 bytes | Lukáš 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*_t | Jiri 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-26 | tests: add some missing headers | Frank Busse | |
2023-03-26 | fix unused variables warning | Daniel Schemmel | |
2023-03-23 | Fix detection and installation of Ubuntu-provided llvm/clang packages | Martin Nowack | |
2023-03-23 | Transition to GitHub Container Registry hosting | Martin Nowack | |
2023-03-23 | fix unused variable warning | Daniel Schemmel | |
2023-03-23 | Remove model_version from the POSIX runtime, as we have never used it. | Cristian Cadar | |
2023-03-23 | tests: add Feature/KleeStatsTermClasses.c | Frank Busse | |
2023-03-23 | stats: add termination class stats | Frank Busse | |
2023-03-23 | tests: add Feature/KleeStatsBranches.c | Frank Busse | |
2023-03-23 | stats: add branch type stats | Frank Busse | |
2023-03-23 | stats: rename States -> ActiveStates, add States | Frank Busse | |
2023-03-23 | stats: add Allocations | Frank Busse | |
2023-03-23 | stats: rename numQueries/Queries -> SolverQueries, add Queries | Frank Busse | |
2023-03-23 | stats: add ExternalCalls | Frank Busse | |
2023-03-23 | stats: add QCacheHits/Misses | Frank Busse | |
2023-03-23 | stats: add InhibitedForks | Frank Busse | |
2023-03-23 | remove obsolete header | Daniel Schemmel | |