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 | 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. | |||
2023-06-11 | Rewrote has_permission in the POSIX runtime. We now only return with ↵ | Cristian Cadar | |
permission error a single time in symbolic execution mode. The rewrite also fixes a bug reported in #1230. Rewrote the FilePerm.c test accordingly. | |||
2023-03-26 | tests: add some missing headers | Frank Busse | |
2023-02-06 | Disable memcpy_chk_err.c on FreeBSD, where a call to __memcpy_chk is not ↵ | Cristian Cadar | |
generated | |||
2023-02-06 | Add an extra check to test/Runtime/FreeStanding/memcpy_chk_err.c ensuring ↵ | Cristian Cadar | |
that a call to __memcpy_chk is emitted | |||
2022-06-15 | Spelling Fixes | m-davis | |
2022-03-11 | FD_Fail: use /dev/zero instead of /etc/mtab | Morgan Jones | |
/etc/mtab doesn't exist in the Nix build sandbox since /etc doesn't exist. However, /dev/zero is more common on UNIX systems and does. | |||
2021-10-17 | test/Runtime/POSIX/Futimesat: futimesat(2) requires _GNU_SOURCE on glibc ↵ | Lukas Zaoral | |
platforms | |||
2021-10-17 | test/Runtime/POSIX/Futimesat: Compile with -std=c99 | Lukas Zaoral | |
.. so that `linux` is not a defined macro. Without the `-std=c99` option, linux is an implicitly defined macro so all such substrings in the given path will be replaced with `1` during stringification. Unfortunately, Fedora's rpmbuild uses `x86_64-redhat-linux-gnu` as a build directory for all CMake projects which leads to a failure due to a change to `x86_64-redhat-1-gnu`. Fixes: #1424 | |||
2021-06-19 | Test failure for WSL 1 | Pavel Yatcheniy | |
2020-12-23 | tests: add getcwd EINVAL test | Frank Busse | |
2020-12-23 | klee-libc: simplify mempcpy | Frank Busse | |
2020-11-09 | Test checking that __strcpy_chk is handled correctly when uclibc is used | Cristian Cadar | |
2020-11-09 | Test checking that __strcat_chk is handled correctly with klee-libc | Cristian Cadar | |
2020-11-09 | Added test checking that a simple overflow is caught via -D_FORTIFY_SOURCE | Cristian Cadar | |
2020-11-09 | Test checking that __memchk_chk is handled correctly with the freestanding ↵ | Cristian Cadar | |
library. | |||
2020-11-03 | fix: bcmp with n==0 | Alastair Reid | |
This was executing the loop when n==0 leading to an out of bound pointer error. Found while verifying Rust code that compares strings. | |||
2020-10-30 | Add test for atexit order | Tomas Jasek | |
2020-08-28 | Definition of __cxa_thread_atexit_impl for the KLEE libc. | Alastair Reid | |
This is a thread-local version of __cxa_atexit (but, in the absence of threads, it is sufficient to just call __cxa_atexit). The test is based on the existing test for atexit in test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c The motivation for adding this function is to support the Rust standard library that calls __cxa_thread_atexit_impl. This function is usually a weak symbol but, in KLEE, this behaves like a call to an unknown function and chaos ensues. Worse, it happens just as the program is cleanly shutting itself down, so programs that are cleanly exiting crash with the wrong message. | |||
2020-04-09 | [posix-runtime] Improve model to handle full-path symbolic files | Timotej Kapus | |
2020-04-09 | [posix-runtime] Add test for full path consistency for symbolic files | Timotej Kapus | |
2020-03-22 | [posix-runtime] Simple GET/SET_LK model | Timotej Kapus | |
2019-11-07 | Added test for 3-argument main. | Cristian Cadar | |
2019-11-05 | [test] Fix missing includes | Martin Nowack | |
Fix multiple missing includes | |||
2019-10-31 | klee-libc: add bcmp | Julian Büning | |
2019-08-14 | Moved Gen*Bout.c tests outside the test/Runtime/POSIX directory, as they ↵ | Cristian Cadar | |
don't need POSIX support to run. | |||
2019-08-14 | Replace sprintf with snprintf throughout codebase | Cristian Cadar | |
2019-08-14 | Create all files in the replay directory and chdir to this directory before ↵ | Cristian Cadar | |
executing the program. | |||
2019-08-14 | Updated error messages in Gen*Bout.c | Cristian Cadar | |
2019-08-14 | Cleaned up messages emitted by klee-replay, and prefixed them all with ↵ | Cristian Cadar | |
"KLEE-REPLAY:" to distinguish them from those printed by the replayed program | |||
2019-08-01 | tests: fix Gen(Random)Bout.c: cd - command not found | Frank Busse | |
2019-03-31 | Made test/Runtime/POSIX/GenBout.c run in an isolated directory | Andrew Santosa | |
2019-03-31 | Various updates to gen-random-bout.cpp | Andrew Santosa | |
* Added handling of --sym-arg * Resolved the crash when minimum and maximum number of arguments for --sym-args are equal * Replaced "range" with "n_args" produced by --sym-args * Added model_version variable (constrained to 1), to prevent klee complaining about insufficient input * Allow a single dash to prefix an option * Arrange the elements in the correct order: command-line arguments, files, stdin, stdout * Added test/Runtime/POSIX/GenRandomBout.c test, with a substitution for %gen-random-bout in test/lit.cfg | |||
2019-03-15 | Renamed --seed-out to --seed-file and --seed-out-dir to --seed-dir, and ↵ | Cristian Cadar | |
placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace. | |||
2019-03-07 | Renamed %llvmgcc and %llvmgxx to %clang and %clangxx respectively. | Cristian Cadar | |
2018-12-19 | Added checks option category, moved --optimize to starting category, renamed ↵ | Cristian Cadar | |
original --run-in option to --running-dir | |||
2018-11-02 | Replaced --no-externals and --allow-external-sym-calls with ↵ | Cristian Cadar | |
--external-calls, updated tests accordingly, and improved documentation on external calls | |||
2018-10-29 | add %OOopt to recently added tests and Concrete | Julian Büning | |
2018-10-26 | Added gen-bout tool to generate ktest file (file.bout) using specified ↵ | Andrew Santosa | |
concrete arguments and files. * Sample use cases: * Using an interesting input as a seed, such as a crashing input. * Analyzing the path condition of a crashing input. * Also added the test: test/Runtime/POSIX/GenBout.c | |||
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-09-29 | Changed code to create up to 100 properly-numbered symbolic arguments, and ↵ | Cristian Cadar | |
add a corresponding check. | |||
2018-09-29 | Add checks for correct usage of the POSIX model, together with an associated ↵ | Cristian Cadar | |
test. | |||
2018-09-20 | Removed unused --sym-files 0 0 argument from FD_Fail test and rewrote the ↵ | Cristian Cadar | |
test to use FileCheck instead of grep | |||
2018-09-20 | Updated IoCtl test to use --sym-stdin instead of --sym-files 0 x to make ↵ | Cristian Cadar | |
stdin symbolic and removed unused arguments to main. | |||
2018-09-20 | Updated DirSeek test to use --sym-stdin instead of --sym-files 0 x to make ↵ | Cristian Cadar | |
stdin symbolic. | |||
2018-09-10 | Add testcase to run POSIX environment and main without arguments | 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-09-06 | runtime: fix memory error in canonicalize_file_name | Frank Busse | |
Fixes #46 and reverts #47. As stated in #46, the solution works for musl, glibc etc. However, the code in stub.c is executed by uclibc and uclibc doesn't allocate the target buffer in realpath. The memory error occured while running df for 10min with DFS. | |||
2018-07-04 | Reorder linking and optimizations | Martin Nowack | |
Link intrinsic library before executing optimizations. This makes sure that any optimization run by KLEE on the module is executed for the intrinsic library as well. Support .ll files as input for KLEE as well. |