Age | Commit message (Collapse) | Author |
|
|
|
to have only solver options.
|
|
Currently KLEE only handles the first segfault in external calls
as it doesn't unblock SIGSEGV afterwards. This patch unblocks the
signal and enables handling of multiple failing calls.
|
|
|
|
|
|
* also adds klee-replay as dependency for systemtests
|
|
Merge unittest coverage results and system tests coverage results
into one coverage report.
|
|
|
|
|
|
|
|
|
|
AddressSpace::checkPointerInObject() that is called in both the forward and the backward searches. This makes the code more modular and removes a large part of duplicated code and should also address the non-deterministic coverage in the resolve() function which affects Codecov reports.
|
|
|
|
add a corresponding check.
|
|
test.
|
|
|
|
|
|
test to use FileCheck instead of grep
|
|
stdin symbolic and removed unused arguments to main.
|
|
stdin symbolic.
|
|
change)
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Starting with LLVM 4, we have getStructTypeOrNull(), so use it.
operator* in post-4 will have a different semantics.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
So handle the type specially whenever needed.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
LLVM 4 removes the old time interface and starts using the C++11's
chrono. So switch to that in klee for LLVM 4 too.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
LLVM 4 renamed and splitted some headers. Take this into account in
includes.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
So that we do not optimize the library during build. It should be
optimized only on runtime, depending on the -optimize parameter.
It could cause various failures like:
inlinable function call in a function with debug info must have a !dbg location
call void @klee_overshift_check(i64 64, i64 %int_cast_to_i64)
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
llvm-config from llvm 3.9 was broken. Fix handling of improperly
returned libraries.
From:
liblibLLVM-3.9.so.so
To:
libLLVM-3.9.so
Fixes #895.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
|
|
Validate if the user-selected entry function exists. Do not assume it is
`main`.
|
|
To enable the POSIX support, the former implementation instrumented the
main function and inserted a call to `klee_init_env` at the beginning.
This has multiple disadvantages:
* debugging information was not correctly propagated leaving the call to
`klee_init_env` without debug information
* the main function always required `int arg, char**` as part of the
function definition of `main`
Based on the new linking infrastructure, we can now add an additional
wrapper `__klee_posix_wraper(int, char**)` that gets always called when
POSIX support is enabled. It executes `klee_init_env` and after that
calls the `main` function.
Enabling POSIX support only requires the renaming of the user provided
`main` into `__klee_posix_wrapped_main` in addition to linking.
|
|
|
|
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.
|
|
|
|
Vararg test can fail if KLEE is able to resolve the
intended out-of-bound memory address to a memory object.
To avoid this, allocate memory explicitly deterministic with
sufficient space between the allocations.
Enables support for Mac OSX again
|
|
|
|
|
|
|
|
klee_make_symbolic. Changed a test case to check this feature.
|
|
Replace the remaining occurrences of `Inst::Create()` with
`llvm::Builder` to manage metadata automatically and to fold
instructions.
C++11 it and clang-format
|
|
Code files in `test/` might contain comment lines that are longer
as they contain `// RUN` commands. clang-formatting breaks the
tests. Stop clang-formatting from doing that.
|
|
|