Age | Commit message (Collapse) | Author | |
---|---|---|---|
2023-06-05 | doxygen.cfg.in: DOXYGEN_OUTPUT_DIR | Julian Büning | |
resolves a FIXME to streamline doxygen.cfg generation a bit | |||
2023-06-05 | CMake: use built-in FindSQLite3 module | Julian Büning | |
available since CMake version 3.14 | |||
2023-06-05 | README-CMake.md: clean up top-level targets | Julian Büning | |
* the old build system is long gone * clean_doxygen was removed by d5cbc2002bbf75f08036f7adf861b027768a0622 * clean_runtime was removed by 6156b4eeb9a429ccc370782d719d0d6c787a6f72 * clean_all was removed by a00424e64d56ff881a72bfd99ea0dbcbe6898b49 | |||
2023-06-05 | docs/CMakeLists.txt: drop support for old CMake versions | Julian Büning | |
minimum CMake version is 3.16.0 as of 3a0e434dc9d4053d75e9c0bbe6faa6dfb46717ae | |||
2023-06-05 | CMake: remove obsolete comments | Julian Büning | |
obsoleted by changes in 3ef5c9d0cd51babb7c4ec2d7bb76d0cb7e47a65c | |||
2023-06-05 | CMake: remove obsolete KLEE_COMPONENT_EXTRA_LIBRARIES | Julian Büning | |
This variable was previously used by `klee_add_component()`, which got removed as part of 3ef5c9d0cd51babb7c4ec2d7bb76d0cb7e47a65c. | |||
2023-06-05 | CMake: remove unused TARGET_LIBS variable | Julian Büning | |
It appears that this variable was never used, already when it was first set in 7e75b491d389c15d48a5cfc455ba9442d7c108ed. | |||
2023-05-26 | Copy stats to test directory when running tests | Daniel Schemmel | |
The sqlite3 databases used for the stats are journalled and potentially must be written to. Therefore, the sqlite3 driver used by `klee-stats` requires write permissions on the database files. By copying the stats files to the test directory, we can now compile and test an out-of-tree build without requiring any write permissions on the source folder at all. | |||
2023-05-26 | Some basic refactoring and pass through comments. In particular, it brings ↵ | Cristian Cadar | |
some related code together (deadline with EntryPoint and ReplayPathFile respectively) which was unnecessarily separated. | |||
2023-05-26 | Refactored and fixed the code dealing with the entry point. | Cristian Cadar | |
main() should not be processed if the entry point is a different function. This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (#1572) | |||
2023-05-26 | add unsized free to kdalloc | Daniel Schemmel | |
2023-05-26 | Improve LOH deallocation scheme | Daniel Schemmel | |
2023-05-26 | Improve error message when KDAlloc fails to create a mapping | Daniel Schemmel | |
2023-05-26 | Add `getMapping` primitive to allocator directly | Daniel Schemmel | |
2023-05-26 | Add `getSize` primitive to kdalloc | Daniel Schemmel | |
2023-05-26 | prevent assertions from failing unnecessarily | Daniel Schemmel | |
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 | |