diff options
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> |