From 24e065075e7ec973db84639725696b9f84975b2f Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Sun, 7 Jun 2009 07:36:26 +0000 Subject: Eliminate anonymous versions. - 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 --- test/Expr/Parser/TypeChecking.pc | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'test') diff --git a/test/Expr/Parser/TypeChecking.pc b/test/Expr/Parser/TypeChecking.pc index 4633313d..9e29d0db 100644 --- a/test/Expr/Parser/TypeChecking.pc +++ b/test/Expr/Parser/TypeChecking.pc @@ -6,4 +6,9 @@ (query [(Eq (ReadLSB w32 0 arr1) true)] false) -# RUN: grep "TypeChecking.pc: parse failure: 1 errors." %t.log +# RUN: grep "TypeChecking.pc:12:25: error: invalid write index (doesn't match array domain)" %t.log +# RUN: grep "TypeChecking.pc:12:35: error: invalid write value (doesn't match array range)" %t.log +# FIXME: Add array declarations +(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr0) 0)] false) + +# RUN: grep "TypeChecking.pc: parse failure: 3 errors." %t.log -- cgit 1.4.1