diff options
| author | Daniel Dunbar <daniel@zuster.org> | 2009-06-05 10:09:13 +0000 |
|---|---|---|
| committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-05 10:09:13 +0000 |
| commit | 1c21929692bf5b6c063c3faaba9da90d04b2e332 (patch) | |
| tree | 79aef6e34cb8d8ee7e603f70a6a4be6789fe08b3 /test/Feature | |
| parent | 40ddb7ac71682a881d9d0cd856295d4f0240dc24 (diff) | |
| download | klee-1c21929692bf5b6c063c3faaba9da90d04b2e332.tar.gz | |
Support the extended query command syntax.
- 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
Diffstat (limited to 'test/Feature')
| -rw-r--r-- | test/Feature/ExprLogging.c | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c index 2abf0070..2329279d 100644 --- a/test/Feature/ExprLogging.c +++ b/test/Feature/ExprLogging.c @@ -1,9 +1,8 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc // RUN: %klee --use-query-pc-log --write-pcs --write-cvcs %t1.bc 2> %t2.log -// RUN: %kleaver -print-ast klee-last/test000001.pc - -// FIXME: Ideally we would verify a roundtrip that we parsed the pc -// file and can dump it back out as the same file. +// RUN: %kleaver -print-ast klee-last/queries.pc > %t3.log +// RUN: %kleaver -print-ast %t3.log > %t4.log +// RUN: diff %t3.log %t4.log #include <assert.h> |