diff options
| author | Daniel Dunbar <daniel@zuster.org> | 2009-06-09 08:42:08 +0000 |
|---|---|---|
| committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-09 08:42:08 +0000 |
| commit | 58d1592fa3fd84aded956801183949b9c710490e (patch) | |
| tree | 097d091d23bf0f5906f9e3542531c5ddb39c4588 /test/Expr/Evaluate.pc | |
| parent | 54d8a1aee4b05daee1244ee1d34df8059a40d5a9 (diff) | |
| download | klee-58d1592fa3fd84aded956801183949b9c710490e.tar.gz | |
More constant Array support.
- 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
Diffstat (limited to 'test/Expr/Evaluate.pc')
| -rw-r--r-- | test/Expr/Evaluate.pc | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/test/Expr/Evaluate.pc b/test/Expr/Evaluate.pc index 0dac0cc8..418a712d 100644 --- a/test/Expr/Evaluate.pc +++ b/test/Expr/Evaluate.pc @@ -13,4 +13,11 @@ array arr1[8] : w32 -> w8 = symbolic (query [(Eq N0:(ReadLSB w32 0 arr1) 10) (Eq N1:(ReadLSB w32 4 arr1) 20)] (Eq (Add w32 N0 N1) - 30)) \ No newline at end of file + 30)) + +# RUN: grep "Query 2: VALID" %t.log +# Query 2 +array hello[4] : w32 -> w8 = [ 1 2 3 5 ] +(query [] (Eq (Add w8 (Read w8 0 hello) + (Read w8 3 hello)) + 6)) |