| Age | Commit message (Collapse) | Author |
|---|
|
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).
|
|
Fix multiple missing includes
|
|
|
|
incompatible with klee_prefer_cex. Fixes https://github.com/klee/klee/issues/1161
While there, remove dependence on `sort` utility, which might help porting KLEE
Windows eventually.
|
|
|
|
|
|
|
|
Improves querying of the .stats file, reduces its size, speeds up reads and
writes and has better defined fail behaviour.
|
|
|
|
|
|
|
|
|
|
|
|
* switch to Python 3
* add file encoding
* some PEP8 reformatting
* fix TOCTOU for open
* replace trimZeros() with rstrip
* remove unused pos/args variables
* remove --write-ints (print by default)
* remove progname section (unused)
* added/modified output rows
- "data:" now shows the Python representation (for use in scripts)
- "hex :" shows the hex representation
- "text:" shows ASCII, all out-of-range/non-printable characters are replaced by a dot
- "int :"/"uint:" print (unsigned) 8/16/32/64 bit integers
* reduce width for object counter to needed minimum instead of 4
* refactor printing into function
|
|
|
|
|
|
Otherwise optimizations done in klee won't have any effect.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Currently KLEE only handles the first segfault in external calls
as it doesn't unblock SIGSEGV afterwards. This patch unblocks the
signal and enables handling of multiple failing calls.
|
|
|
|
|
|
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers.
|
|
|
|
|
|
Clone some tests to have their 3.7 version. 'call's, 'load's and
'getelementptr's match the new specification in them.
@andreamattavelli: Fixed test cases: BitCastAlias test cases included
modification to alias specifications that require LLVM 3.8
[v2] added comments what was changed and why
[v3] the new tests are without suffix, the old ones have ".leq36".
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
doDumpStates calls stepInstruction and therefore indirectly increases time and
instruction statistics for all dangling (dumped) states. This patch removes the
call, but now the timing stats for the last executed state are lost, as
StatsTracker::stepInstruction isn't called anymore.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Rewritten tests by replacing 'XFAIL: darwin' with 'REQUIRES: not-darwin'
|
|
|
|
variables when possible.
Previously an alignment 8 was always used which did not faithfully
emulate what was either explicitly requested in the LLVM IR or what
the default alignment was for the target.
|
|
`klee::getDirectCallTarget(llvm::CallSite)`.
The problem is that it doesn't handle bitcasted functions that call a
weak alias.
|
|
function) (#455)
|
|
POSIX runtime. If the check fails, exit with an error. (#457)
|
|
Fix for klee_get_obj_size() crashing on 64-bit, resolves #446
|
|
|
|
Added test case exposing division by zero failure reported by @kren1 and made division total in STP to fix it.
|
|
Generated STP equality expressions have to be the same type.
If a shift with different types as operands was used,
therefore equality expressions of different width were generated.
Beside avoiding the different sizes, this patch restores the
original behavior to extract just the part involved in shifting
and therefore should generate smaller expressions.
Enable sdiv test case
|
|
recently fixed in STP.
|
|
Bug fix in IndependentSolver
|
|
it after the division bug is fixed.
|
|
https://github.com/klee/klee/issues/334, which triggers a bug in solver-optimize-divides, and which is for now expected to fail.
|
|
The problem was that ``assertCreatedPointEvaluatesToTrue()`` used in the
IndependentSolver assumed that it would be given an assignment for every
array. If this wasn't the case the ``Assignment`` object by default
would just replace every read of an unknown array with a byte filled
with zeros.
This problem would appear if
``IndependentSolver::getInitialValues(...)`` was called without asking
for assignment for used arrays.
I saw two ways of fixing this
* Get an assignment for all arrays even if the client didn't ask
for them. This guarantees that is the query is satisfiable then
we can compute a concrete assignment.
* Just do a "best effort" check and only check expressions that can
be fully assigned to.
I chose the latter because the first option seems pretty wasteful,
especially for an assert.
The second option isn't ideal though as it would be possible to
compute an assignment that for the whole query leads to "unsat"
but we wouldn't notice.
|
|
for it
|
|
Fix signed division by constant 1/ -1
|
