Age | Commit message (Collapse) | Author |
|
|
|
|
|
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
|
|
|
|
Added units for some of the data and
modified klee-stats source code to provide solver time
as a fraction of walltime along with fork, resolve
and cexcache time.
|
|
|
|
This Dockerfile provides a Grafana server with a preconfigured dashboard
and a datasource that will connect to klee-stats, as soon as klee-stats
is run.
|
|
the function name is "getTreeStream" but here's a spelling error
|
|
|
|
|
|
|
|
due to fixes from #315 and #316.
|
|
Some of these leaks were introduced by the factory constructor for Array
objects (f049ff3bc04daead8c3bb9f06e89e71e2054c82a) but a few others have
been around for far longer.
This leak was fixed by introducing a ``ArrayCache`` object which has two
purposes
* Retains ownership of all created ``Array`` objects and destroys them when
the ``ArrayCache`` destructor is called.
* Mimic the caching behaviour for symbolic arrays that was introduced
by f049ff3bc04daead8c3bb9f06e89e71e2054c82a where arrays with the same
name and size get "uniqued".
The Executor now maintains a ``arrayCache`` member that it uses and
passes by pointer to objects that need to construct ``Array`` objects (i.e.
``ObjectState``). This way when the Executor is destroyed all the
``Array`` objects get freed which seems like the right time to do this.
For Kleaver the ``ParserImpl`` has a ``TheArrayCache`` member that is
used for building ``Array`` objects. This means that the Parser must
live as long as the built expressions will be used otherwise we will
have a use after free. I'm not sure this is the right design choice.
It might be better to transfer ownership of the ``Array`` objects to
the root ``Decl`` returned by the parser.
|
|
The overloaded assignment operator previously only deleted the head
``UpdateNode`` if the ``UpdateList`` had exclusive ownership which left the remaining
list of ``UpdateNode``s dangling if those nodes had ``refCount`` of 1.
To fix this the logic that was previously in the ``UpdateList`` destructor
for deleting nodes that were exclusively referenced by the UpdateList
has been moved into ``UpdateList::tryFreeNodes()`` so that it can be
called from ``UpdateList::operator=()``.
It looks like this bug has been in KLEE since the beginning.
|
|
which is required to suppress all the leaks I'm currently seeing in KLEE
when running ``make unittests`` and ``make check``.
Ideally there should be no leaks but we aren't there yet. Hopefully
at some point we won't need to suppress any leaks and then we can
have a TravisCI build that builds with ASan.
The leak of the expression objects when running the executor is worrying
and I will investigate this next.
|
|
|
|
- This consumes the treestream files produced with --write-paths or
--write-sym-paths, and renders out the tree in a very ad-hoc funky way.
Your mileage may vary! :)
Example image: http://klee.llvm.org/data/treegraph_example.jpg
Example movie: http://klee.llvm.org/data/treegraph_example.avi
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102869 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74365 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73344 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73057 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Lots more tweaks, documentation, and web page content is needed,
but this should compile & work on OS X & Linux.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
|