| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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
|
|
|
|
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.
|
|
Shifting by bitwidth-1 is valid
|
|
parallel.
- It would be nice if there was an easier way to do this that didn't involve
editing all of the tests (like running each test in its own directory), but
this approach fixes #146 and doesn't involve changing 'lit' or writing a
wrapper harness. My assumption is a lot of tests start are derived from
another one, so hopefully following this convention won't be burdensome, and
I updated 'make check' so that it will produce an error if any test runs klee
without --output-dir (by checking for the existing of klee-last files).
- This also helps with #147 but I still can't fully run tests in parallel (I
start hitting STP errors).
|
|
(independently).
In our recently switch to llvm::raw_ostream (and friends) (I think this
is d934d983692c8952cdb887cbcd59f2df0001b9c0) we forgot to flush the
llvm::raw_string_ostream to the underlying string used for error report
files (e.g. test000001.overshift.err) so we would end up writing an
empty string to error report files.
Also added a test case to catch this.
|
|
|
|
|
|
Say hello to our new friend, llvm-lit :)
|
|
DejaGNU testing used to have this flag in its substitution variable
but for llvm-lit this has not been done.
I could replicate what DejaGNU did but by forcing developers to be
explicit when creating LLVM bitcode
* Remove test suite inconsistentcies. Some tests explictly use
-emit-llvm
* Allows for tests to be written in the future that invoke
the compiler as a native compiler
|
|
a file created by KLEE exists. A big difference between
DejaGNU and llvm-lit is that in DejaGNU the working directory
is the test output directory (e.g. test/Feature/Output) but
in llvm-lit the working directory is the test directory
(e.g. test/Feature )
To fix this I have used the %T substitution variable for llvm-lit.
I have also improved some tests by using LLVM's FileCheck tool
and removing of hard coded constants for data type size in
some places.
This commit inevitably breaks running the tests under DejaGNU.
Although it is possible to hack by introducing the %T substitution
variable some tests would still be broken because the use of shell
pipes in DejaGNU doesn't seem to work properly. I could work around
this but it's really not worth the effort.
|
|
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168798 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
Includes test case.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@157463 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135598 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100422 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
backward compatibility. Also changed KLEE_RUNTEST to KTEST_FILE. Updated tutorial-1.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72312 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- For compatibility we still accept 2 argument form of klee_make_symbolic, but
this will go away eventually.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72265 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
|
