Age | Commit message (Collapse) | Author |
|
/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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
library.
|
|
This was executing the loop when n==0 leading to an out of bound pointer
error.
Found while verifying Rust code that compares strings.
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
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>
|