Age | Commit message (Collapse) | Author |
|
Tracking function locations separately correctly without prefixing
it with a directory.
|
|
Assuming a `klee-out-*` directory is moved to a different path location, subsequent analysis of the run.istats with KCachegrind focusing on assembly is impossible as the `assembly.ll` cannot be found.
The reason is that the absolute path of the object file (assembly.ll) is hard-coded as part of the generated run.istats.
To fix this, assume that the file is local to the `run.istats`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
this function can be used to modify the control flow of the program
on different paths, enabling self-modifying code.
|
|
|
|
|
|
|
|
Compilers are allowed to hoist function calls and do GVE.
This is currently done even without `--optimization` enabled.
This is unfortunate in the context of KLEE function calls that might
depend on specific code position without direct control flow
dependencies. In such cases, function calls can be hoisted.
To circumvent this, disallow to optimise functions that contain such
calls by default. This might reduce optimisation for some functions
containing such function calls but still allows it for all others.
This patch adds an additional pass, that detects all functions starting with a
prefix `klee_` and disable optimisations for functions containing such
calls.
This is enabled by default but can be disabled by
`--klee-call-optimisation=false`.
|
|
|
|
placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace.
|
|
category (with --write-cov, --write-cvcs etc.)
|
|
|
|
function and updated some .ll tests to use --optimize=false instead of --disable-opt
|
|
|
|
|
|
|
|
|
|
|
|
Check if a state reaches the maximum number of stack frames allowed.
To be performant, the number of stack frames are checked.
In comparison, native execution checks the size of the stack.
Still, this is good enough to find possible stack overflows.
The limit can be changed with `-max-stack-frames`. The current
default is 8192 frames.
|
|
|
|
--external-calls, updated tests accordingly, and improved documentation on external calls
|
|
|
|
|
|
Otherwise optimizations done in klee won't have any effect.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Validate non-optimised and optimised variant of added checks.
|
|
Check that only important div instructions are annotated.
Check the optimized case as well: the call to the validating function
might not be part of the code anymore but already inlined - make sure
the instruction still has the metadata attached.
|
|
|
|
|
|
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers.
|
|
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
|
|
|
|
|
|
|
|
|
|
* 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>
|
|
|
|
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>
|
|
|
|
|
|
|
|
|