| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com>
(cherry picked from commit 1ea1a7576300a4da01d925df42db109660ef54d2)
|
|
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com>
(cherry picked from commit 5d61fb6114bafbf67c59899d15e397684d4ceb28)
|
|
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com>
(cherry picked from commit 5d9af025ee5a01b1650f11ed0612a10357a98308)
|
|
|
|
|
|
They are not supported anymore for newer LLVM versions.
|
|
The wording changed slightly in newer versions.
Update the test case to support this.
|
|
The optimiser generates different code and calls fwrite directly instead.
|
|
Similar functionality needs to be added using a new pass manager
|
|
Handle like `memalign` for now.
|
|
`Intrinsic::flt_rounds` got removed
|
|
|
|
|
|
|
|
|
|
This automatically lifts old-style pointers to opaque pointers.
More recent versions use opaque pointers automatically and do not need
an explicit enabling.
|
|
Currently, we assume C++11 support being used to by the tested software.
This needs to change if newer C++ standards should be supported.
|
|
Newer compilers use `-std=gnu17` as the default when compiling C code.
Fix all the test cases that violate this behaviour or explicitly request
older standards `-std=c89` where necessary.
|
|
compilers
|
|
|
|
|
|
|
|
To support multiple include directories for c++ header files, use
`%libcxx_includes`. This string contains the `-I` compiler directive for
each include path as well.
Update test cases to use new directive.
|
|
`libc++` include headers are now split between platform dependent and
platform independent code.
Before, only include files for the platform independent code were
considered. Add support to automatically find platform dependent
includes as well.
Simplify the detection of libraries and paths.
Instead of pointing to the `v1` directory, pointing to the include
directory for `-DKLEE_LIBCXX_INCLUDE_PATH` is enough.
Update build script to support this as well.
|
|
|
|
`-DLLVM_ENABLE_PROJECTS` does not include runtimes anymore,
instead a `-DLLVM_ENABLE_RUNTIMES` should be used in addition
|
|
|
|
If an array name ended with a number, adding a number-only suffix could
generate the same name used as part of the solvers.
In the specific testcase `val_1` became solver array `val_111` which
collided with array `val_11` that became `val_111` as well.
Using an `_` as prefix for the suffix, solves that problem in general,
i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`.
Fixes #1668
|
|
callers
|
|
|
|
|
|
|
|
This reworked logic also fixes a buffer overflow which could be triggered during seed extension.
|
|
|
|
|
|
Added a test case.
|
|
and w/o seed extension) based on FP concretization.
|
|
|
|
|
|
|
|
map added to ExecutionState); now storing addresses of MemoryObjects for easier cleanup
|
|
This feature implements tracking of and resolution of memory objects in the presence of
symbolic addresses.
For example, an expression like the following:
int x;
klee_make_symbolic(&x, sizeof(x), "x");
int* tmp = &b.y[x].z;
For a concrete array object "y", which is a member of struct "b", a symbolic offset "x" would normally be resolved to any matching
memory object - including the ones outside of the object "b".
This behaviour is consistent with symbex approach of exploring all execution paths.
However, from the point of view of security testing, we would only be interested to know if we are still
in-bounds or there is a buffer overflow.
The implemented feature creates and tracks (via the GEP instruction) the mapping between the current
symbolic offset and the base object it refers to: in our example we are able to tell that the reference
should happen within the object "b" (as the array "y" is inside the same memory blob). As a result, we are able to minimize
the symbolic exploration to only two paths: one within the bounds of "b", the other with a buffer overflow bug.
The feature is turned on via the single-object-resolution command line flag.
A new test case was implemented to illustrate how the feature works.
|
|
|
|
|
|
|
|
Introduce three different kinds of process trees:
1. Noop: does nothing (e.g. no allocations for DFS)
2. InMemory: same behaviour as before (e.g. RandomPathSearcher)
3. Persistent: similar to InMemory but writes nodes to ptree.db
and tracks information such as branch type, termination
type or source location (asm) in nodes. Enabled with
-write-ptree
ptree.db files can be analysed/plotted with the new "klee-ptree"
tool.
|
|
std::is_standard_layout
|
|
|
