| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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.
|
|
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
|
|
|
|
|
|
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.
|
|
small improvements.
|
|
--external-call-warnings=none|once-per-function|all.
This eliminates the ambiguity when both of the old options were set.
Added test for the new option.
|
|
permission error a single time in symbolic execution mode.
The rewrite also fixes a bug reported in #1230.
Rewrote the FilePerm.c test accordingly.
|
|
|
|
This test previously had a REQUIRES line with geq-llvm-7.0. Because LLVM
version 7.0 is no longer "known" (test/lit.cfg), the required feature is
not available and the test is discarded as unsupported by llvm-lit.
|
|
The functionality of the batching searcher that increases the time
budget if it is shorter than the time between two calls to
`selectState()` ignored the disabled time budget. Effectively, the
batching searcher thus picks a very arbitrary time budget on its own.
|
|
|
|
The sqlite3 databases used for the stats are journalled and potentially
must be written to. Therefore, the sqlite3 driver used by `klee-stats`
requires write permissions on the database files.
By copying the stats files to the test directory, we can now compile and
test an out-of-tree build without requiring any write permissions on the
source folder at all.
|
|
main() should not be processed if the entry point is a different function.
This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (#1572)
|
|
with recent changes.
|
|
|
|
|
|
|
|
|
|
expected to fail.
|
|
CryptoMinisat
|
|
With recent LLVM versions, this should allow to link against dynamic LLVM
libraries.
|
|
|
|
|
|
Under 64bit architecture, a ptr-error might be found.
Ignore this for now.
|
|
Ignore test in the first place, if no 32bit is enabled.
|
|
Previously, the code did two consecutive checks. First one succeeded
only if the given index was not already seen and the second one did
an analogous check but for arrays. However, if the given index usage
was already detected for some array, its usage for another array that
already had some other index detected would be silently skipped and the
`incompatible` flag would not be set.
Therefore, if the code contained e.g. the following conditional jump on two
arrays with two symbolic indices, the multi-index access would remain
undetected:
if ((array1[k] + array2[x] + array2[k]) == 0)
Resulting in the following output:
KLEE: WARNING: OPT_I: infeasible branch!
KLEE: WARNING: OPT_I: successful
|
|
LLVM 14 has introduced the noundef function argument attribute.
|
|
|
|
|
|
|
|
LLVM became more complex, use LLVM's CMake functionality directly instead
of replicating this behaviour in KLEE's build system.
Use the correct build flags provided by LLVM itself.
This is influenced by the way LLVM is built in the first place.
Remove older CMake support (< 3.0).
|
|
|
|
|
|
|
|
generated
|
|
that a call to __memcpy_chk is emitted
|
|
|
|
|
