Age | Commit message (Collapse) | Author |
|
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.
|
|
Add some missing header to silence
compiler warnings
|
|
|
|
|
|
|
|
Major issue was that puts was used for the succeed printf calls.
With newer gcc/clang versions, printf is always used.
The former took different code paths leading to much more possibilities
to trigger failed writes and therefore generating more test cases.
This patch avoids the generation of puts.
And checks for the 4 possible generated test cases for 2 possible errors.
|
|
prevents the hang we are seeing.
|
|
parallel.
- It would be nice if there was an easier way to do this that didn't involve
editing all of the tests (like running each test in its own directory), but
this approach fixes #146 and doesn't involve changing 'lit' or writing a
wrapper harness. My assumption is a lot of tests start are derived from
another one, so hopefully following this convention won't be burdensome, and
I updated 'make check' so that it will produce an error if any test runs klee
without --output-dir (by checking for the existing of klee-last files).
- This also helps with #147 but I still can't fully run tests in parallel (I
start hitting STP errors).
|
|
a call fprintf(stderr,...). llvm-gcc transforms this to a call to
fwrite() however clang does not so klee-uclibc's fprintf will be
called instead and if klee-uclibc is compiled with KLEE_SYM_PRINTF
then output will always go stdout if the FILE is stdout or stderr.
The end result of this is that when we build with Clang under LLVM3.3
is that the fprintf(stderr,...) print outs go to standard output instead
and so the test would fail because it expects the fprintf(stderr,...)
to be on stderr.
This test sort of fixes this by having the test check stdout for
the fprintf(stderr,...) statements too.
|
|
support.
|
|
Say hello to our new friend, llvm-lit :)
|
|
time.
|
|
tests from being executed if not enabled at configure time.
|
|
a file created by KLEE exists. A big difference between
DejaGNU and llvm-lit is that in DejaGNU the working directory
is the test output directory (e.g. test/Feature/Output) but
in llvm-lit the working directory is the test directory
(e.g. test/Feature )
To fix this I have used the %T substitution variable for llvm-lit.
I have also improved some tests by using LLVM's FileCheck tool
and removing of hard coded constants for data type size in
some places.
This commit inevitably breaks running the tests under DejaGNU.
Although it is possible to hack by introducing the %T substitution
variable some tests would still be broken because the use of shell
pipes in DejaGNU doesn't seem to work properly. I could work around
this but it's really not worth the effort.
|
|
uclibc is compiled without symbolic printf support
|
|
|
|
https://github.com/ccadar/klee/issues/32) and fixed an #include in one of the tests.
|
|
|
|
heuristics in KLEE. The new options are documented at
http://klee.llvm.org/klee-options.html.
Cleaned a bit the code in UserSearcher.cpp, and fixed some test cases
to use the new options.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163711 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154110 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
regression suite (see http://llvm.org/bugs/show_bug.cgi?id=7423)
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106431 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
renaming of '08.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72748 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Lots more tweaks, documentation, and web page content is needed,
but this should compile & work on OS X & Linux.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
|