Age | Commit message (Collapse) | Author |
|
- The are parsed, printed, and solved now.
- Remove some members of ArrayDecl which are only duplicates of Array members.
- KLEE still doesn't create these, but you can write them by hand.
The EXE style constant array optimization for STP (turning the initial writes
into asserts) is now only a stones throw away, but I need to leave something fun
to do tomorrow. :)
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73133 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- This doesn't actually start using them, it just attempts to update all
clients to do the right thing in the presence of them.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73130 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- The sole remaining client was IVC, which is currently disabled for other
correctness issues. I patched it to compile and left a FIXME that we will
have to resolve this before we can reenable IVC.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73129 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73128 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
constructors I missed.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73127 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73125 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- The right way to handle this is by using constant arrays, where the semantics
are easier to define and implement.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73124 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73046 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
these, but the parser can).
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73033 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73032 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73030 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Printing current prints all declarations, and we allow redefinition, since
the printer doesn't know what has already been printed.
- Names don't print right yet, since the Array* object doesn't have the name.
- Various things are unsupported.
o Array domain/range must be w32/w8.
o Concrete initializers for arrays are unsupported.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73026 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73019 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- For now, this means the isRooted flag for arrays isn't propogated to the
kquery language. We should figure out how to do this, but allow anonymous
versions isn't the right way.
Also, improved the error on invalid writes a bit.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73018 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72997 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- There are two optional lists following the constraints and the
query expression. The first is a list of expressions to give values
for and the second is a list of arrays to provide values for.
- Update ExprPPrinter to accept extra arguments to print these
arguments.
- Add Parser support.
- Add more ArrayDecl support.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72938 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72935 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72931 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
asserts.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72924 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72921 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72863 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Propogate ConstantExpr to various places, or cast as appropriate.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72862 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72859 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- These should use cast<>, isa<>, or dyn_cast<> as appropriate (or better yet,
changed to use ref<ConstantExpr> when the type is known).
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72857 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72853 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
the same width. Added a test case that was previously triggering an
assert violation.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72850 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72847 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72845 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72841 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
broken (it was written for n-ary Concats, but now we have binary
Concats.)
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72840 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Ref.h is now freestanding.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72824 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
more standard reference counting wrapper.
- The only interesting changes here are in Ref.h, everything else is just
updating foo.method to use foo->method instead.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72777 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
hashValue.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72752 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- This function should go away...
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72751 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
(Extraneous uses are going away shortly)
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72749 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- The "constant optimization" embedded inside ref<Expr> is going away.
- No functionality change.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72730 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72518 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
|