| # RUN: %kleaver -evaluate %s > %t.log |
| |
| array arr0[4] : w32 -> w8 = symbolic |
| array arr1[8] : w32 -> w8 = symbolic |
| |
| # RUN: grep "Query 0: INVALID" %t.log |
| # Query 0 |
| (query [] (Not (Ult (ReadLSB w32 0 arr0) |
| 16))) |
| |
| # RUN: grep "Query 1: VALID" %t.log |
| # Query 1 |
| (query [(Eq N0:(ReadLSB w32 0 arr1) 10) |
| (Eq N1:(ReadLSB w32 4 arr1) 20)] |
| (Eq (Add w32 N0 N1) |
| 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)) |
| |
| # RUN: grep "Query 3: VALID" %t.log |
| # Query 2 |
| (query [] (Eq (Not w8 (Read w8 0 arr1)) |
| (Xor w8 (Read w8 0 arr1) 0xff))) |
