Age | Commit message (Collapse) | Author |
|
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.
|
|
This reworked logic also fixes a buffer overflow which could be triggered during seed extension.
|
|
permission error a single time in symbolic execution mode.
The rewrite also fixes a bug reported in #1230.
Rewrote the FilePerm.c test accordingly.
|
|
|
|
/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.
|
|
platforms
|
|
.. 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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fix multiple missing includes
|
|
don't need POSIX support to run.
|
|
|
|
executing the program.
|
|
|
|
"KLEE-REPLAY:" to distinguish them from those printed by the replayed program
|
|
|
|
|
|
* 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
|
|
placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace.
|
|
|
|
original --run-in option to --running-dir
|
|
--external-calls, updated tests accordingly, and improved documentation on external calls
|
|
|
|
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
|
|
Otherwise optimizations done in klee won't have any effect.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
add a corresponding check.
|
|
test.
|
|
test to use FileCheck instead of grep
|
|
stdin symbolic and removed unused arguments to main.
|
|
stdin symbolic.
|
|
|
|
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers.
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
|
|
If an external function in KLEE is invoked, it might update errno.
Previously, the errno specific variable in a state was only updated
if it was part of the executed instructions.
That opened up a timeframe that increased the likelihood of errno being
overwritten by another method call.
This patch fixes two issues:
* the errno of the KLEE process state is updated before the external
function call allowing to detect changes to it later on
* after the external call, the memory object of errno is directly
updated
with its new value, reducing the likelihood to be overwritten by
another
call
Additional features:
* Add support for `errno()` for Darwin as well.
* Simplified errno handling in POSIX layer
|
|
|
|
In our build environments, /etc/fstab is an empty file. Use /etc/mtab,
which should be non-empty anywhere, hopefully.
For the reference, the test fails as follows:
FAIL: KLEE :: Runtime/POSIX/FD_Fail.c (188 of 212)
************ TEST 'KLEE :: Runtime/POSIX/FD_Fail.c' FAILED ************
Script:
--
clang-3.8 -Iinclude test/Runtime/POSIX/FD_Fail.c -emit-llvm -O0 -c -o build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc
rm -rf build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out
build/bin/klee --output-dir=build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out --libc=uclibc --posix-runtime build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc --sym-files 0 0 --max-fail 1 > build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fread(): ok" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fread(): fail" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fclose(): ok" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fclose(): fail" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
--
Exit Code: 1
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
* remove unused stat variable
* use %ld for long int
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
This causes problems on a shared machine where multiple users are running the
KLEE unit tests.
|
|
|