Age | Commit message (Collapse) | Author |
|
using "../"
|
|
|
|
The code assumed that the passed pointer points at the beginning
of the object. Remove this assumption and support any (constant)
pointer. The string is read util either the end of the object
is hit (in which case a warning is issued as the string
was not zero terminated) or until the terminating zero is found.
|
|
The code is simpler and more in the spirit of C++.
|
|
ArrayHashTime
* fix binding order for assignments when KLEE_ARRAY_DEBUG enabled
* always write ArrayHashTime column to run.stats, assign -1 when KLEE_ARRAY_DEBUG disabled
* remove unused NumObjects column from run.stats
* remove NumObjects panel from Grafana
|
|
|
|
This uses the `ref<>`-based memory handling of MemoryObjects.
This makes it explicit that references are held in:
- ExecutionState::symbolics
- ObjectState
|
|
Remove additional reference counting as part of UpdateNodeList and
UpdateNode. Simplifies code.
|
|
Using KLEE's `ref<>` shared ptr requires the referenced object
to contain a reference counter to be added and initialised to 0
as part of the constructor.
To support better reuse of the `ref<>` ptr add a `ReferenceCounter`
struct.
Just adding this struct to a new class/struct as member enables
reference counting with `ref<>` - no additional counter management
needed.
|
|
Statistics encoded in `run.istats` were limited to a maximum number of 13 due to encoding in a `uint64_t` variable.
This approach has multiple limitations:
- a maximum number of 13 statistics were allowed
- a subtle bug can be triggered if many more statistics are added - independent of the selected statistics for `run.istats`
Depending on the linking order, statistics will get a different ID. Previously, the ID was used to shift a `1` to its position marking the statistic as being used.
This will lead to undefined behaviour if more than 63 statistics are used.
Using an llvm::SmallBitVector instead fixes both problems.
|
|
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`.
|
|
|
|
Having both weight and depth in execution state is wasteful,
therefore this patch removes weight.
The nurs:depth searcher is replaced by nurs:rp, which uses pow to compute
the weight
A new nurs:depth searcher is introduced that biases the search with depth,
making it the only other searcher that prefers to go deep (similar to dfs).
|
|
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de>
|
|
numSeeds is unused since commit 4eb050e2999b (ExecutorTimers: refactor
and move to support lib), so remove it.
|
|
Fixes #264.
We first aggregate all constant memory objects initialise them and initialise their counter parts in the concrete memory.
After that, we mark memory objects as constant such that they can't be modified (i.e. this includes marking them symbolic).
|
|
|
|
|
|
- moves timer handling from Executor into support lib
- introduces TimerGroup, removes TimerInfo/WriteStatsTimer/UpdateReachableTimer/WriteIStatsTimer classes
- removes ExecutorTimers.cpp and ExecutorTimerInfo.h
- removes -max-instruction-time flag (see #1114)
|
|
- adds -timer-interval threshold for timer checks
- fixes #831
|
|
|
|
|
|
|
|
|
|
* creates two new methods: dumpStates, dumpPTree
|
|
|
|
|
|
|
|
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
|
|
|
|
|
|
|
|
consistent naming convention
|
|
|
|
|
|
this function can be used to modify the control flow of the program
on different paths, enabling self-modifying code.
|
|
|
|
|
|
|
|
Improves querying of the .stats file, reduces its size, speeds up reads and
writes and has better defined fail behaviour.
|
|
on FreeBSD
|
|
|
|
|
|
|
|
|
|
|
|
Better debug information
|
|
|
|
them to 0
|
|
namespace in Executor.cpp
|