| Age | Commit message (Collapse) | Author |
|---|
|
due to fixes from #315 and #316.
|
|
Try to fix leaking Array objects detected by ASan.
|
|
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.
|
|
helper functions.
|
|
for it
|
|
Use "-debug-dump-stp-queries" argument for KLEE/Kleaver
to print out each STP query sent to the STP Solver.
Queries have the format which `stp` frontend can understand.
|
|
|
|
|
|
|
|
Support directory
|
|
Fix a memory leak in ``UpdateList`` detected by AddressSanitizer.
|
|
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.
|
|
MemorySanitzer and ThreadSanitizer environment variables when running
lit tests.
This makes it easy suppress errors in sanitized versions of KLEE
|
|
build. Spotted by @domainexpert
|
|
|
|
template braces get reformatted the C++11 way and that breaks
compilation.
|
|
flag as suggested by @ccadar
|
|
``--silent-klee-assume=0`` is no longer passed. This ensures that we
also check that ``--silent-klee-assume`` is off by default.
|
|
infeasible assumptions.
|
|
``stp/stplog.h`` header file in the current version of STP
and no support in the build system for setting this define so
this code is completly dead.
|
|
|
|
Fixing klee-clang to strip all flags not understood by llvm-link
|
|
|
|
Removing -fstack-protector-strong for clang <= 3.4
|
|
It's not supported and breaks compilation. This affects in particular
Debian Jessie and probably all derived distros, too
|
|
|
|
|
|
[STPBuilder] Generate SRrem expressions correctly
|
|
Specify klee uclibc version
|
|
branch for klee-uclibc.
|
|
"klee_uclibc_v1.0.0" release of uclibc.
|
|
|
|
Don't use /tmp for futimesat unit test
|
|
This causes problems on a shared machine where multiple users are running the
KLEE unit tests.
|
|
The '%' operater in C is not Gauss Modulo
but remainder operations.
Using a negative number as right operand
can result in a negative number.
Fix appropriate SRem building
Note: MetaSMTlib implementation doesn't have that bug.
|
|
Fix signed division by constant 1/ -1
|
|
Allow to generate initial values for queries with empty constraint set.
|
|
|
|
Travis: Support KLEE with different STP versions, in particular 2.1.0; Disable r940
|
|
Say farewell to r940.
|
|
Build STP version based on provided branch.
Build current STP version 2.1.0 by default and test with master branch
as well
|
|
Division by constant divisor get optimized
using shift and multiplication operations in STP builder.
The used method cannot be applied for divisor 1 and -1.
In that case use slow path.
|
|
Added option to specify a different entry point from main(). Remove some whitespaces.
|
|
Fix assertion failure in getDirectCallTarget
|
|
|
|
|
|
|
|
Added link in README.md to coverage information for KLEE's codebase
|
|
|
