Age | Commit message (Collapse) | Author |
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73363 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73351 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73312 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Cleaned up enough to build on Darwin & Linux.
- I don't really care to have too many programs in the test suite, but this
works until we have some better place for them.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73303 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
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73020 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
|
|
- 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
|
|
- Currently only handles validity queries.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72933 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72920 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72851 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@72841 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
renaming of '08.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72748 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
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72206 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
|