about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2023-05-26Copy stats to test directory when running testsDaniel 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-26Some 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-26Refactored 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-26add unsized free to kdallocDaniel Schemmel
2023-05-26Improve LOH deallocation schemeDaniel Schemmel
2023-05-26Improve error message when KDAlloc fails to create a mappingDaniel Schemmel
2023-05-26Add `getMapping` primitive to allocator directlyDaniel Schemmel
2023-05-26Add `getSize` primitive to kdallocDaniel Schemmel
2023-05-26prevent assertions from failing unnecessarilyDaniel Schemmel
2023-05-26Write `Control::meta` in C++17 styleDaniel Schemmel
2023-05-26Use unique_ptr for MemoryManager and avoid re-creating it in the first placeMartin Nowack
No need to re-create and re-alloc all the memory again after execution.
2023-05-26Cleaned up and updated codecov file.Cristian Cadar
2023-04-21Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency ↵Cristian Cadar
with recent changes.
2023-04-21Replaced "-data" and "-stat" by "_data" and "_stat" in the ktest-(rand)gen ↵Cristian Cadar
tools for consistency with recent changes.
2023-04-21use unique_ptr all throughout the solver chainDaniel Schemmel
2023-04-21use unique_ptr in SolverDaniel Schemmel
2023-04-21use unique_ptr in QueryLoggingSolverDaniel Schemmel
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-21 06:34:50 +0000