Age | Commit message (Collapse) | Author | |
---|---|---|---|
2024-02-08 | Assume C compiler's default standard is `-std=gnu17` | Martin Nowack | |
Newer compilers use `-std=gnu17` as the default when compiling C code. Fix all the test cases that violate this behaviour or explicitly request older standards `-std=c89` where necessary. | |||
2024-01-30 | Avoid generating array names in solver builders that could accidently collide | Martin Nowack | |
If an array name ended with a number, adding a number-only suffix could generate the same name used as part of the solvers. In the specific testcase `val_1` became solver array `val_111` which collided with array `val_11` that became `val_111` as well. Using an `_` as prefix for the suffix, solves that problem in general, i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`. Fixes #1668 | |||
2023-09-11 | Changed use-after-free and double-free tests to expect KDAlloc, plus some ↵ | Cristian Cadar | |
small improvements. | |||
2023-06-05 | fix BatchingSearcher's disabled time budget | Julian Büning | |
The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own. | |||
2023-04-21 | Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency ↵ | Cristian Cadar | |
with recent changes. | |||
2023-03-26 | tests: add some missing headers | Frank Busse | |
2022-07-04 | Inline asm external call | Mikhail | |
2022-06-30 | rename CallSite to CallBase | Frank Busse | |
2022-06-15 | Spelling Fixes | m-davis | |
2022-06-13 | tests: invoke LLVM tools through their corresponding macros | Lukáš Zaoral | |
2022-03-17 | LLVM < 6 leftovers | Julian Büning | |
2022-03-17 | remove LLVM < 6 from build/test scripts | Frank Busse | |
2021-05-04 | test: count paths with -dump-states-on-halt=false | Frank Busse | |
2021-04-18 | tests: Invoke tools through their corresponding macros | Lukas Zaoral | |
2020-10-09 | fix: fabs() working on the wrong argument | David Laprell | |
2020-09-30 | tests: support .test and introduce %klee-stats | Frank Busse | |
2020-06-25 | add simple unknown bitcast alias test from the original issue | Julian Büning | |
2020-06-25 | add known bitcast test for comparison | Julian Büning | |
2020-06-25 | regression test for unknown bitcast alias | Julian Büning | |
2020-05-01 | Add test case from #1257 to reproduce behaviour | Martin Nowack | |
2020-04-30 | Removed the Internal directory from include/klee | Cristian Cadar | |
2019-11-05 | Mark all constant global memory objects as constant | Martin Nowack | |
Fixes #264. We first aggregate all constant memory objects initialise them and initialise their counter parts in the concrete memory. After that, we mark memory objects as constant such that they can't be modified (i.e. this includes marking them symbolic). | |||
2019-11-05 | [test] Fix missing includes | Martin Nowack | |
Fix multiple missing includes | |||
2019-10-31 | Executor: fix missing default case in switch instruction | Frank Busse | |
2019-10-07 | Do not use klee_range() in regression/2014-09-13-debug-info.c test, as it is | Gleb Popov | |
incompatible with klee_prefer_cex. Fixes https://github.com/klee/klee/issues/1161 While there, remove dependence on `sort` utility, which might help porting KLEE Windows eventually. | |||
2019-08-14 | Update basic block iterator after deleting instruction; add test case | Martin Nowack | |
2019-07-30 | Use #include "klee/..." (instead of #include <klee/...>) consistently. | Cristian Cadar | |
2019-04-04 | klee-stats: add - to to-csv/grafana options | Frank Busse | |
2019-04-04 | Change the .stats format into sqlite3 | Timotej Kapus | |
Improves querying of the .stats file, reduces its size, speeds up reads and writes and has better defined fail behaviour. | |||
2019-03-21 | remove tests for LLVM <= 3.7 | Julian Büning | |
2019-03-07 | Renamed %llvmgcc and %llvmgxx to %clang and %clangxx respectively. | Cristian Cadar | |
2019-03-05 | add regression test for LLVM PR39177 | Julian Büning | |
2019-03-05 | fix Executor::initializeGlobals for aliases pointing to another alias | Julian Büning | |
2018-12-19 | regression/2014-09-13-debug-info.c: use 'int: ' instead of 'data:' | Frank Busse | |
2018-12-19 | Various fixes for ktest-tool | Frank Busse | |
* switch to Python 3 * add file encoding * some PEP8 reformatting * fix TOCTOU for open * replace trimZeros() with rstrip * remove unused pos/args variables * remove --write-ints (print by default) * remove progname section (unused) * added/modified output rows - "data:" now shows the Python representation (for use in scripts) - "hex :" shows the hex representation - "text:" shows ASCII, all out-of-range/non-printable characters are replaced by a dot - "int :"/"uint:" print (unsigned) 8/16/32/64 bit integers * reduce width for object counter to needed minimum instead of 4 * refactor printing into function | |||
2018-12-19 | Renamed --stop-after-n-instructions to --max-instructions, as suggested by @251 | Cristian Cadar | |
2018-10-29 | add %OOopt to recently added tests and Concrete | Julian Büning | |
2018-10-26 | llvm5: test, add -disable-O0-optnone to -O0 | Jiri Slaby | |
Otherwise optimizations done in klee won't have any effect. Signed-off-by: Jiri Slaby <jirislaby@gmail.com> | |||
2018-10-10 | fix handling of failing external calls | Frank Busse | |
Currently KLEE only handles the first segfault in external calls as it doesn't unblock SIGSEGV afterwards. This patch unblocks the signal and enables handling of multiple failing calls. | |||
2018-09-10 | Add POSIX runtime as dependency for the test case | Martin Nowack | |
2018-09-10 | Unify the error message if that function has not been found. | Martin Nowack | |
2018-09-06 | Use FileCheck and LINE instead of grep if possible | Martin Nowack | |
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers. | |||
2018-06-29 | fix out of range access in KleeHandler::getKTestFilesInDir | Frank Busse | |
2018-06-13 | klee_int: allow NULL as name | Frank Busse | |
2018-05-24 | test: add versions of some tests for LLVM 3.7 | Richard Trembecký | |
Clone some tests to have their 3.7 version. 'call's, 'load's and 'getelementptr's match the new specification in them. @andreamattavelli: Fixed test cases: BitCastAlias test cases included modification to alias specifications that require LLVM 3.8 [v2] added comments what was changed and why [v3] the new tests are without suffix, the old ones have ".leq36". Signed-off-by: Jiri Slaby <jirislaby@gmail.com> | |||
2018-05-18 | tests: use names in klee_make_symbolic | Frank Busse | |
2018-05-06 | Moved regression test to proper location. Fixes #705 | Cristian Cadar | |
2018-04-09 | doDumpStates: incorrectly increments stats | Frank Busse | |
doDumpStates calls stepInstruction and therefore indirectly increases time and instruction statistics for all dangling (dumped) states. This patch removes the call, but now the timing stats for the last executed state are lost, as StatsTracker::stepInstruction isn't called anymore. | |||
2018-02-18 | Add missing endian information to avoid selecction of big endian systems | Martin Nowack | |
2017-12-11 | fix regression test: use `%klee` instead of `klee` | Felix Rath | |