| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73345 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- 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
|
|
- 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
|
|
- 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@72931 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
|
