| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-02-29 | Test case for externally concretized variables and constraint fully symbolic ↵ | Martin Nowack | |
| variables The test case is based on the example provided by Mingyi Liu from the KLEE mailing list. | |||
| 2024-02-27 | Small refactorings and reformatting in callExternalFunction | Cristian Cadar | |
| 2024-02-27 | This commit fixes the concretization of arguments following an external call ↵ | Cristian Cadar | |
| with symbolic arguments. It also introduces a new external call policy, where the symbolic inputs are left unconstrained following such a call, useful for certain external calls such as printf. | |||
| 2024-02-27 | Two test cases exercising two policies for calling external calls with ↵ | Cristian Cadar | |
| symbolic arguments. One of them is currently expected to fail. | |||
| 2024-02-17 | Remove the not Darwin requirement for the test TargetMismatch.c | Cristian Cadar | |
| 2024-02-16 | drop llvm 9 and 10 | Daniel Schemmel | |
| 2024-02-12 | Fix brittleness in Feature/VarArgByVal test | Daniel Schemmel | |
| 2024-02-08 | Fix test cases to support opaque pointers | Martin Nowack | |
| 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 | Add checks to the seed concretization tests about the expected number of queries | Cristian Cadar | |
| 2024-01-30 | Added a test for --allow-seed-extension | Cristian Cadar | |
| 2024-01-30 | Removed --zero-seed-extension, and merge it with --allow-seed-extension. ↵ | Cristian Cadar | |
| This reworked logic also fixes a buffer overflow which could be triggered during seed extension. | |||
| 2024-01-30 | On a symbolic allocation, retrieve size from a seed, if available | Cristian Cadar | |
| 2024-01-30 | Concretize arguments to external function calls using seeds, if available. ↵ | Cristian Cadar | |
| Added a test case. | |||
| 2024-01-30 | Concretize constants using seed values, when available. Added two tests (w/ ↵ | Cristian Cadar | |
| and w/o seed extension) based on FP concretization. | |||
| 2024-01-12 | Remove check for the number of solver queries | Tomasz Kuchta | |
| 2024-01-12 | Make test more deterministic | Tomasz Kuchta | |
| 2024-01-12 | Follow-up: applied review comments, implemented meta-data cleanup (one more ↵ | Tomasz Kuchta | |
| map added to ExecutionState); now storing addresses of MemoryObjects for easier cleanup | |||
| 2024-01-12 | Feature: implement single memory object resolution for symbolic addresses. | Tomasz Kuchta | |
| This feature implements tracking of and resolution of memory objects in the presence of symbolic addresses. For example, an expression like the following: int x; klee_make_symbolic(&x, sizeof(x), "x"); int* tmp = &b.y[x].z; For a concrete array object "y", which is a member of struct "b", a symbolic offset "x" would normally be resolved to any matching memory object - including the ones outside of the object "b". This behaviour is consistent with symbex approach of exploring all execution paths. However, from the point of view of security testing, we would only be interested to know if we are still in-bounds or there is a buffer overflow. The implemented feature creates and tracks (via the GEP instruction) the mapping between the current symbolic offset and the base object it refers to: in our example we are able to tell that the reference should happen within the object "b" (as the array "y" is inside the same memory blob). As a result, we are able to minimize the symbolic exploration to only two paths: one within the bounds of "b", the other with a buffer overflow bug. The feature is turned on via the single-object-resolution command line flag. A new test case was implemented to illustrate how the feature works. | |||
| 2024-01-12 | Renamed PTree to ExecutionTree (and similar) | Cristian Cadar | |
| 2024-01-12 | Rename files from PTree to ExecutionTree (and similar) | Cristian Cadar | |
| 2024-01-12 | new: persistent ptree (-write-ptree) and klee-ptree | Frank Busse | |
| Introduce three different kinds of process trees: 1. Noop: does nothing (e.g. no allocations for DFS) 2. InMemory: same behaviour as before (e.g. RandomPathSearcher) 3. Persistent: similar to InMemory but writes nodes to ptree.db and tracks information such as branch type, termination type or source location (asm) in nodes. Enabled with -write-ptree ptree.db files can be analysed/plotted with the new "klee-ptree" tool. | |||
| 2023-09-11 | Changed use-after-free and double-free tests to expect KDAlloc, plus some ↵ | Cristian Cadar | |
| small improvements. | |||
| 2023-07-12 | Replaced --suppress-external-warnings and --all-external-warnings with ↵ | Cristian Cadar | |
| --external-call-warnings=none|once-per-function|all. This eliminates the ambiguity when both of the old options were set. Added test for the new option. | |||
| 2023-06-05 | test/Feature/StackTraceOutput.c: relative checks, clang-format | Julian Büning | |
| 2023-06-05 | re-enable StackTraceOutput.c test | Julian Büning | |
| This test previously had a REQUIRES line with geq-llvm-7.0. Because LLVM version 7.0 is no longer "known" (test/lit.cfg), the required feature is not available and the test is discarded as unsupported by llvm-lit. | |||
| 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 | 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-03-26 | tests: add some missing headers | Frank Busse | |
| 2023-03-23 | tests: add Feature/KleeStatsTermClasses.c | Frank Busse | |
| 2023-03-23 | tests: add Feature/KleeStatsBranches.c | Frank Busse | |
| 2023-03-22 | Added more test cases for --entry-point. EntryPointMissing is currently ↵ | Cristian Cadar | |
| expected to fail. | |||
| 2023-03-20 | llvm14: port test/Feature/VarArgByVal.c to LLVM 14 | Lukáš Zaoral | |
| LLVM 14 has introduced the noundef function argument attribute. | |||
| 2023-03-17 | Don't fail `KleeStats.c` test if it takes 1s or longer | Martin Nowack | |
| 2023-03-17 | Disable `const_array_opt1` for ubsan as well | Martin Nowack | |
| 2023-03-16 | Integrate KDAlloc into KLEE | Daniel Schemmel | |
| 2023-01-06 | fix output check in test const_arr_opt1 | Matthis Gördel | |
| 2022-12-09 | fix FileCheck cmd of VarArgByVal test | Matthis Gördel | |
| 2022-09-26 | Improve the message for when large arrays become symbolic. Only print this ↵ | Cristian Cadar | |
| warning once per array. Add test case. | |||
| 2022-09-14 | Improve pattern for FileCheck in UBSan's tests | Pavel | |
| 2022-09-14 | Improve pattern for FileCheck in UBSan's tests | Pavel | |
| 2022-09-14 | Eliminate .undefined_behavior.err category and simplify tests | Pavel | |
| 2022-09-14 | Remove LLVM version < 9 | Pavel | |
| 2022-09-14 | Check extensions of generated files in tests | Pavel | |
| 2022-09-14 | Remove LLVM version < 6 | Pavel | |
| 2022-09-14 | Support UBSan-enabled binaries | Pavel Yatcheniy | |
| 2022-07-04 | Inline asm external call | Mikhail | |
| 2022-06-30 | remove LLVM < 9 | Frank Busse | |
| 2022-06-27 | Fix error with empty EntryPoint | Saveliy Grigoryev | |
| 2022-06-13 | tests: add StackTraceOutput.c | Frank Busse | |
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |