From 58d1592fa3fd84aded956801183949b9c710490e Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Tue, 9 Jun 2009 08:42:08 +0000 Subject: 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 --- test/Expr/Evaluate.pc | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'test') 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)) -- cgit 1.4.1