| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
|
|
* handle BlockAddress (which is not a valid function pointer)
* there is no instruction with opcode 0
* add test for functionality
|
|
With version 3.5, LLVM introduced a subtle semantic change in the API of
`Value`. With that change, `use_begin()` is renamed to `user_begin()`.
Additionally, a new method `use_begin()` with a different meaning was
introduced. Now, `use_begin()` actually iterates over `Use`s, whereas
before, dereferencing it would give a `User *`. For further details,
please refer to https://reviews.llvm.org/rL203364.
Due to the reintroduction of `use_begin()`, existing code may still
compile, although the semantics have changed. In the code changed with
this patch, all `dyn_cast`s for `Use` fail and the else branch is
always taken.
|
|
addresses comment made by @adrianherrera in #385
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
alias in LLVM 3.8 has a new format, it adds an AliaseeTy parameter. So
handle this in the tests.
[v2] add comments about what was changed and why
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
LLVM commit eac309550f25 removed implicit iterator conversions. So we
have to get the iterators explicitly now.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
After LLVM commit 25569fdcdab0, archive iterator returns
object::Archive::Child instead of child_iterator, adapt to that.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
LLVM commit d912be98f8eb changed the prototype of linkModules to accept
std::unique_ptr. Adapt to that.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
No need to flush it, see llvm-mirror/llvm@d4177b2
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
createFunctionAttrsPass was split to createPostOrderFunctionAttrsPass
and createReversePostOrderFunctionAttrsPass in LLVM commit e96fb9ab15d4.
createGlobalsModRefPass was changed to createGlobalsAAWrapperPass in
LLVM commit 9146833fa313.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
The rounding was removed because it was never needed:
llvm-mirror/llvm@ff278be
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
|
|
clang-format on patch)
|
|
deprecated for many years now and causes problems during replay. Changed and simplified affected test case.
|
|
Shifting negative values is implementation-defined.
Shifting by equal number of the bits as is the size of the type is
undefined.
So fix both of these.
This fixes #911.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
runtime
|
|
|
|
|
|
|
|
|
|
|
|
Building/managing dependencies of KLEE are not easy. This script should change
this.
Features:
* script install different versions in their specific directories
This allows:
- to have different versions in parallel installed: llvm, solvers
- to have different optimization levels installed (Debug, no-debug,
assertions, optimized)
- to have different versions of instrumentation enabled (address, memory,
leakage, undefined behavior)
* the script is kept distribution agnostic: assuming basic packages are
installed (a compiler), use `scripts/build/ubuntu-dependencies.sh` to install
ubuntu specific ones
* the script does not install any file into system directories (sudo is not
required) files are only installed into a user specified BASE directory
The same scripts are used for either local setup (`scripts/build/local_install.sh`)
or create a docker image based of your current source folder (`scripts/build/build_docker.sh`)
Change the defaults permanently by modifying (`scripts/build/common-defaults.sh`)
or change them on the fly by providing them as environment variables on the
command line.
The same scripts are also used for TravisCI, so we test what we are using.
|
|
|
|
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.
|
|
Strictly differentiate between the following type of libraries:
* FreeStanding: contains minimal amount of methods a compiler would expect
* klee-libc: contains a minimal libc implementation
* POSIX: contains a POSIX layer that can be used on top of a libc implementation
* Intrinsic: contains additional runtime functions which provide KLEE-specific functionalities, (e.g. checks)
Builds always archives instead of single modules.
This allows to reduce linked-in dependencies of tested applications.
|
|
|
|
|
|
|
|
|
