Age | Commit message (Collapse) | Author |
|
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
|
|
|
|
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.
|
|
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.
|
|
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
|
|
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>
|
|
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>
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
Clone some tests to have their 3.7 version. 'call's, 'load's and
'getelementptr's match the new specification in them.
@andreamattavelli: Fixed test cases: BitCastAlias test cases included
modification to alias specifications that require LLVM 3.8
[v2] added comments what was changed and why
[v3] the new tests are without suffix, the old ones have ".leq36".
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Some compilers are picky, so avoid the warning by additional parentheses:
test/VectorInstructions/integer_ops_unsigned_symbolic.c:85:22: warning: & has lower precedence than <; < will be evaluated first [-Wparentheses]
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
options. Make klee_abort() call abort() in replay, and removed trivial test which cannot be easily integrated into the test suite.
|
|
corresponding tests
|
|
|
|
doDumpStates calls stepInstruction and therefore indirectly increases time and
instruction statistics for all dangling (dumped) states. This patch removes the
call, but now the timing stats for the last executed state are lost, as
StatsTracker::stepInstruction isn't called anymore.
|