about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2014-01-12 21:34:59 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2014-01-20 14:45:07 +0000
commit38a084fb50cfb38570d0194bb076805e4f752c99 (patch)
tree598b00ceae9e12773e61b6e6657d654afc00360e /test
parent313390c68fc808d5fe7cf746a7a65b1e018362dc (diff)
downloadklee-38a084fb50cfb38570d0194bb076805e4f752c99.tar.gz
Fixed many tests that make use of the file tool to check
a file created by KLEE exists. A big difference between
DejaGNU and llvm-lit is that in DejaGNU the working directory
is the test output directory (e.g. test/Feature/Output) but
in llvm-lit the working directory is the test directory
(e.g. test/Feature )

To fix this I have used the %T substitution variable for llvm-lit.

I have also improved some tests by using LLVM's FileCheck tool
and removing of hard coded constants for data type size in
some places.

This commit inevitably breaks running the tests under DejaGNU.
Although it is possible to hack by introducing the %T substitution
variable some tests would still be broken because the use of shell
pipes in DejaGNU doesn't seem to work properly. I could work around
this but it's really not worth the effort.
Diffstat (limited to 'test')
-rw-r--r--test/Feature/CallToUndefinedExternal.cpp5
-rw-r--r--test/Feature/DanglingConcreteReadExpr.c2
-rw-r--r--test/Feature/DoubleFree.c5
-rw-r--r--test/Feature/DumpStatesOnHalt.c5
-rw-r--r--test/Feature/ExprLogging.c8
-rw-r--r--test/Feature/InAndOutOfBounds.c14
-rw-r--r--test/Feature/IntrinsicTrap.ll8
-rw-r--r--test/Feature/KleeReportError.c9
-rw-r--r--test/Feature/LowerSwitch.c4
-rw-r--r--test/Feature/MakeConcreteSymbolic.c4
-rw-r--r--test/Feature/MultipleFreeResolution.c13
-rw-r--r--test/Feature/MultipleReallocResolution.c4
-rw-r--r--test/Feature/OneFreeError.c8
-rw-r--r--test/Feature/OneOutOfBounds.c10
-rw-r--r--test/Feature/OverlappedError.c4
-rw-r--r--test/Feature/PreferCex.c3
-rw-r--r--test/Feature/Realloc.c4
-rw-r--r--test/Feature/ReplayPath.c2
-rw-r--r--test/Feature/Vararg.c2
-rw-r--r--test/Feature/WriteCov.c4
-rw-r--r--test/Runtime/POSIX/FD_Fail2.c14
-rw-r--r--test/Runtime/POSIX/FilePerm.c6
-rw-r--r--test/Runtime/POSIX/FreeArgv.c14
-rw-r--r--test/Runtime/POSIX/Isatty.c13
-rw-r--r--test/Runtime/POSIX/Openat.c2
-rw-r--r--test/Runtime/POSIX/PrgName.c4
-rw-r--r--test/Runtime/POSIX/SeedAndFail.c8
-rw-r--r--test/Solver/LargeIntegers.pc12
-rw-r--r--test/regression/2007-10-11-free-of-alloca.c7
-rw-r--r--test/regression/2007-10-11-illegal-access-after-free-and-branch.c7
-rw-r--r--test/regression/2008-03-04-free-of-global.c7
31 files changed, 123 insertions, 89 deletions
diff --git a/test/Feature/CallToUndefinedExternal.cpp b/test/Feature/CallToUndefinedExternal.cpp
index 84b5a3b4..26e8fc55 100644
--- a/test/Feature/CallToUndefinedExternal.cpp
+++ b/test/Feature/CallToUndefinedExternal.cpp
@@ -1,10 +1,11 @@
 // RUN: %llvmgxx %s -emit-llvm -g -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.external.err
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.external.err
 
 extern "C" void poof(void);
 
 int main() {
+  // CHECK: failed external call: poof
   poof();
 
   return 0;
diff --git a/test/Feature/DanglingConcreteReadExpr.c b/test/Feature/DanglingConcreteReadExpr.c
index 1bf44c3f..204187a2 100644
--- a/test/Feature/DanglingConcreteReadExpr.c
+++ b/test/Feature/DanglingConcreteReadExpr.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee %t1.bc
-// RUN: grep "total queries = 2" klee-last/info
+// RUN: grep "total queries = 2" %T/klee-last/info
 
 #include <assert.h>
 
diff --git a/test/Feature/DoubleFree.c b/test/Feature/DoubleFree.c
index 3727ef2b..d97e0c08 100644
--- a/test/Feature/DoubleFree.c
+++ b/test/Feature/DoubleFree.c
@@ -1,10 +1,11 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.ptr.err
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ptr.err
 
 int main() {
   int *x = malloc(4);
   free(x);
+  // CHECK: memory error: invalid pointer: free
   free(x);
   return 0;
 }
diff --git a/test/Feature/DumpStatesOnHalt.c b/test/Feature/DumpStatesOnHalt.c
index d86b786b..c65d5568 100644
--- a/test/Feature/DumpStatesOnHalt.c
+++ b/test/Feature/DumpStatesOnHalt.c
@@ -1,8 +1,9 @@
 // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --stop-after-n-instructions=1 --dump-states-on-halt=true %t1.bc
-// RUN: test -f klee-last/test000001.ktest
+// RUN: %klee --stop-after-n-instructions=1 --dump-states-on-halt=true %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ktest
 
 int main() {
   int x = 10;
   return x;
 }
+// CHECK: halting execution, dumping remaining states
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
index 9e9df87a..abab8031 100644
--- a/test/Feature/ExprLogging.c
+++ b/test/Feature/ExprLogging.c
@@ -1,14 +1,14 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
 // We disable the cex-cache to eliminate nondeterminism across different solvers, in particular when counting the number of queries in the last two commands
 // RUN: %klee --use-cex-cache=false --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log
-// RUN: %kleaver -print-ast klee-last/all-queries.pc > %t3.log
+// RUN: %kleaver -print-ast %T/klee-last/all-queries.pc > %t3.log
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
-// RUN: %kleaver -print-ast klee-last/solver-queries.pc > %t3.log
+// RUN: %kleaver -print-ast %T/klee-last/solver-queries.pc > %t3.log
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
-// RUN: grep "^; Query" klee-last/all-queries.smt2 | wc -l | grep -q 17
-// RUN: grep "^; Query" klee-last/solver-queries.smt2 | wc -l | grep -q 17
+// RUN: grep "^; Query" %T/klee-last/all-queries.smt2 | wc -l | grep -q 17
+// RUN: grep "^; Query" %T/klee-last/solver-queries.smt2 | wc -l | grep -q 17
 
 #include <assert.h>
 
diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c
index ba655b83..3a559075 100644
--- a/test/Feature/InAndOutOfBounds.c
+++ b/test/Feature/InAndOutOfBounds.c
@@ -1,8 +1,8 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.ptr.err -o -f klee-last/test000002.ptr.err 
-// RUN: test ! -f klee-last/test000001.ptr.err -o ! -f klee-last/test000002.ptr.err 
-// RUN: test ! -f klee-last/test000003.ktest
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ptr.err -o -f %T/klee-last/test000002.ptr.err 
+// RUN: test ! -f %T/klee-last/test000001.ptr.err -o ! -f %T/klee-last/test000002.ptr.err 
+// RUN: test ! -f %T/klee-last/test000003.ktest
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
@@ -12,7 +12,9 @@ unsigned klee_urange(unsigned start, unsigned end) {
 }
 
 int main() {
-  int *x = malloc(4);
+  int *x = malloc(sizeof(int));
+  // FIXME: Use newer FileCheck syntax to support relative line numbers
+  // CHECK: InAndOutOfBounds.c:18: memory error: out of bound pointer
   x[klee_urange(0,2)] = 1;
   free(x);
   return 0;
diff --git a/test/Feature/IntrinsicTrap.ll b/test/Feature/IntrinsicTrap.ll
index 5af46225..13b93e4d 100644
--- a/test/Feature/IntrinsicTrap.ll
+++ b/test/Feature/IntrinsicTrap.ll
@@ -1,8 +1,6 @@
 ; RUN: llvm-as %s -f -o %t1.bc
 ; RUN: %klee -disable-opt %t1.bc
-; RUN: grep abort() klee-last/assembly.ll | wc -l | grep -q 2
-; RUN: echo "llvm.trap()" > %t2.ll
-; RUN: grep llvm.trap() klee-last/assembly.ll %t2.ll | wc -l | grep -q 1
+; RUN: FileCheck %s --input-file=%T/klee-last/assembly.ll
 
 target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-f128:128:128-n8:16:32:64"
 target triple = "x86_64-unknown-linux-gnu"
@@ -15,6 +13,8 @@ entry:
   br i1 %c, label %btrue, label %bfalse
 
 btrue:
+  ; CHECK-NOT: call void @llvm.trap()
+  ; CHECK: call void @abort()
   call void @llvm.trap() noreturn nounwind
   unreachable
 
@@ -25,4 +25,6 @@ return:
   ret i32 0
 }
 
+; CHECK-NOT: call void @llvm.trap()
+; CHECK: declare void @abort()
 declare void @llvm.trap() noreturn nounwind
diff --git a/test/Feature/KleeReportError.c b/test/Feature/KleeReportError.c
index dda72fd0..37c07ed1 100644
--- a/test/Feature/KleeReportError.c
+++ b/test/Feature/KleeReportError.c
@@ -1,6 +1,6 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
-// RUN: %klee --emit-all-errors %t2.bc > %t3.log
-// RUN: ls klee-last/ | grep .my.err | wc -l | grep 2
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --emit-all-errors %t2.bc 2>&1 | FileCheck %s
+// RUN: ls %T/klee-last/ | grep .my.err | wc -l | grep 2
 #include <stdio.h>
 #include <assert.h>
 
@@ -16,6 +16,9 @@ int main(int argc, char** argv) {
 
   if (y) {
     fprintf(stderr, "My error\n");
+    // CHECK: KleeReportError.c:22: My error
+    // CHECK: KleeReportError.c:22: My error
+    // FIXME: Use FileCheck's relative line number syntax
     klee_report_error(__FILE__, __LINE__, "My error", "my.err");
   }
 
diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c
index 1b92e398..49cad076 100644
--- a/test/Feature/LowerSwitch.c
+++ b/test/Feature/LowerSwitch.c
@@ -1,8 +1,8 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc
 // RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc
-// RUN: not test -f klee-last/test000010.ktest
+// RUN: not test -f %T/klee-last/test000010.ktest
 // RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc
-// RUN: test -f klee-last/test000010.ktest
+// RUN: test -f %T/klee-last/test000010.ktest
 
 #include <stdio.h>
 
diff --git a/test/Feature/MakeConcreteSymbolic.c b/test/Feature/MakeConcreteSymbolic.c
index 29b43a04..bfbb807d 100644
--- a/test/Feature/MakeConcreteSymbolic.c
+++ b/test/Feature/MakeConcreteSymbolic.c
@@ -1,8 +1,8 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
 // RUN: %klee --exit-on-error %t1.bc
-// RUN: grep "done: total queries = 0" klee-last/info
+// RUN: grep "done: total queries = 0" %T/klee-last/info
 // RUN: %klee --make-concrete-symbolic=1 --exit-on-error %t1.bc
-// RUN: grep "done: total queries = 2" klee-last/info
+// RUN: grep "done: total queries = 2" %T/klee-last/info
 
 
 #include <assert.h>
diff --git a/test/Feature/MultipleFreeResolution.c b/test/Feature/MultipleFreeResolution.c
index 8a36f459..cd8a383b 100644
--- a/test/Feature/MultipleFreeResolution.c
+++ b/test/Feature/MultipleFreeResolution.c
@@ -1,7 +1,7 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --emit-all-errors %t1.bc
-// RUN: ls klee-last/ | grep .ktest | wc -l | grep 4
-// RUN: ls klee-last/ | grep .err | wc -l | grep 3
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --emit-all-errors %t1.bc 2>&1 | FileCheck %s
+// RUN: ls %T/klee-last/ | grep .ktest | wc -l | grep 4
+// RUN: ls %T/klee-last/ | grep .err | wc -l | grep 3
 
 #include <stdlib.h>
 #include <stdio.h>
@@ -31,9 +31,14 @@ int main() {
 
   free(buf[s]);
 
+  // CHECK: MultipleFreeResolution.c:39: memory error: out of bound pointer
+  // CHECK: MultipleFreeResolution.c:39: memory error: out of bound pointer
+  // CHECK: MultipleFreeResolution.c:39: memory error: out of bound pointer
+  // FIXME: Use FileCheck's relative line numbers
   for (i=0; i<3; i++) {
     printf("*buf[%d] = %d\n", i, *buf[i]);
   }
 
   return 0;
 }
+// CHECK: KLEE: done: generated tests = 4
diff --git a/test/Feature/MultipleReallocResolution.c b/test/Feature/MultipleReallocResolution.c
index b1a14ace..1f77485f 100644
--- a/test/Feature/MultipleReallocResolution.c
+++ b/test/Feature/MultipleReallocResolution.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee %t1.bc
-// RUN: ls klee-last/ | grep .err | wc -l | grep 2
-// RUN: ls klee-last/ | grep .ptr.err | wc -l | grep 2
+// RUN: ls %T/klee-last/ | grep .err | wc -l | grep 2
+// RUN: ls %T/klee-last/ | grep .ptr.err | wc -l | grep 2
 
 #include <assert.h>
 #include <stdlib.h>
diff --git a/test/Feature/OneFreeError.c b/test/Feature/OneFreeError.c
index 8eb13298..e83b535a 100644
--- a/test/Feature/OneFreeError.c
+++ b/test/Feature/OneFreeError.c
@@ -1,10 +1,12 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.ptr.err
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ptr.err
 
 int main() {
   int *x = malloc(4);
   free(x);
+  // CHECK: OneFreeError.c:10: memory error: out of bound pointer
+  // FIXME: Use FileCheck's relative line numbers
   x[0] = 1;
   return 0;
 }
diff --git a/test/Feature/OneOutOfBounds.c b/test/Feature/OneOutOfBounds.c
index 11a9eecb..72d36b70 100644
--- a/test/Feature/OneOutOfBounds.c
+++ b/test/Feature/OneOutOfBounds.c
@@ -1,9 +1,11 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.ptr.err
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ptr.err
 
 int main() {
-  int *x = malloc(4);
+  int *x = malloc(sizeof(int));
+  // CHECK: OneOutOfBounds.c:9: memory error: out of bound pointer
+  // FIXME: Use FileCheck's relative line numbers
   x[1] = 1;
   free(x);
   return 0;
diff --git a/test/Feature/OverlappedError.c b/test/Feature/OverlappedError.c
index aa220ed9..886c7ec8 100644
--- a/test/Feature/OverlappedError.c
+++ b/test/Feature/OverlappedError.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee %t1.bc
-// RUN: ls klee-last/ | grep .ktest | wc -l | grep 4
-// RUN: ls klee-last/ | grep .ptr.err | wc -l | grep 2
+// RUN: ls %T/klee-last/ | grep .ktest | wc -l | grep 4
+// RUN: ls %T/klee-last/ | grep .ptr.err | wc -l | grep 2
 
 #include <stdlib.h>
 
diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c
index 97ce5101..6cdb8446 100644
--- a/test/Feature/PreferCex.c
+++ b/test/Feature/PreferCex.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee --exit-on-error %t1.bc
-// RUN: ktest-tool klee-last/test000001.ktest | grep -F 'Hi\x00\x00'
+// RUN: ktest-tool %T/klee-last/test000001.ktest | FileCheck %s
 
 #include <assert.h>
 #include <stdlib.h>
@@ -10,6 +10,7 @@ int main() {
   char buf[4];
 
   klee_make_symbolic(buf, sizeof buf);
+  // CHECK: Hi\x00\x00
   klee_prefer_cex(buf, buf[0]=='H');
   klee_prefer_cex(buf, buf[1]=='i');
   klee_prefer_cex(buf, buf[2]=='\0');
diff --git a/test/Feature/Realloc.c b/test/Feature/Realloc.c
index a47adad6..62aa170b 100644
--- a/test/Feature/Realloc.c
+++ b/test/Feature/Realloc.c
@@ -1,6 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --exit-on-error %t1.bc
-// RUN: grep "KLEE: WARNING ONCE: Large alloc" klee-last/warnings.txt
+// RUN: %klee --exit-on-error %t1.bc 2>&1 | FileCheck %s
 
 #include <assert.h>
 #include <stdlib.h>
@@ -11,6 +10,7 @@ int main() {
   assert(p);
   p[1] = 52;
 
+  // CHECK: KLEE: WARNING ONCE: Large alloc
   int *p2 = realloc(p, 1<<30);
   assert(p2[1] == 52);
 
diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c
index f88ad6dc..ccf59657 100644
--- a/test/Feature/ReplayPath.c
+++ b/test/Feature/ReplayPath.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -DCOND_EXIT -c -o %t1.bc
 // RUN: klee --write-paths %t1.bc > %t3.good
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
-// RUN: %klee --replay-path klee-last/test000001.path %t2.bc >%t3.log
+// RUN: %klee --replay-path %T/klee-last/test000001.path %t2.bc > %t3.log
 // RUN: diff %t3.log %t3.good
 
 #include <unistd.h>
diff --git a/test/Feature/Vararg.c b/test/Feature/Vararg.c
index 9f6643bc..31eee235 100644
--- a/test/Feature/Vararg.c
+++ b/test/Feature/Vararg.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee %t1.bc > %t2.out
 // RUN: grep "types: (52, 37, 2.00, (9,12,15))" %t2.out
-// RUN: test -f klee-last/test000001.ptr.err
+// RUN: test -f %T/klee-last/test000001.ptr.err
 
 #include <stdarg.h>
 #include <assert.h>
diff --git a/test/Feature/WriteCov.c b/test/Feature/WriteCov.c
index bb2d64e8..45e7bc43 100644
--- a/test/Feature/WriteCov.c
+++ b/test/Feature/WriteCov.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t2.bc
 // RUN: %klee --exit-on-error --write-cov %t2.bc
-// RUN: grep -c WriteCov.c:15  klee-last/test000001.cov klee-last/test000002.cov  >%t3.txt
-// RUN: grep -c WriteCov.c:17  klee-last/test000001.cov klee-last/test000002.cov >>%t3.txt
+// RUN: grep -c WriteCov.c:15  %T/klee-last/test000001.cov %T/klee-last/test000002.cov  >%t3.txt
+// RUN: grep -c WriteCov.c:17  %T/klee-last/test000001.cov %T/klee-last/test000002.cov >>%t3.txt
 // RUN: grep klee-last/test000001.cov:0 %t3.txt
 // RUN: grep klee-last/test000001.cov:1 %t3.txt
 // RUN: grep klee-last/test000002.cov:0 %t3.txt
diff --git a/test/Runtime/POSIX/FD_Fail2.c b/test/Runtime/POSIX/FD_Fail2.c
index b42e03bf..624329fc 100644
--- a/test/Runtime/POSIX/FD_Fail2.c
+++ b/test/Runtime/POSIX/FD_Fail2.c
@@ -1,12 +1,12 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee --libc=uclibc --posix-runtime --search=dfs %t1.bc --sym-files 1 10 --max-fail 1
-// RUN: test -f klee-last/test000001.ktest
-// RUN: test -f klee-last/test000002.ktest
-// RUN: test -f klee-last/test000003.ktest
-// RUN: test -f klee-last/test000004.ktest
-// RUN: test -f klee-last/test000005.ktest
-// RUN: test -f klee-last/test000006.ktest
-// RUN: test -f klee-last/test000007.ktest
+// RUN: test -f %T/klee-last/test000001.ktest
+// RUN: test -f %T/klee-last/test000002.ktest
+// RUN: test -f %T/klee-last/test000003.ktest
+// RUN: test -f %T/klee-last/test000004.ktest
+// RUN: test -f %T/klee-last/test000005.ktest
+// RUN: test -f %T/klee-last/test000006.ktest
+// RUN: test -f %T/klee-last/test000007.ktest
 
 #include <stdio.h>
 #include <assert.h>
diff --git a/test/Runtime/POSIX/FilePerm.c b/test/Runtime/POSIX/FilePerm.c
index d387c2a9..1346c09a 100644
--- a/test/Runtime/POSIX/FilePerm.c
+++ b/test/Runtime/POSIX/FilePerm.c
@@ -1,8 +1,8 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
 // RUN: %klee --posix-runtime %t.bc --sym-files 1 10 --sym-stdout 2>%t.log 
-// RUN: test -f klee-last/test000001.ktest
-// RUN: test -f klee-last/test000002.ktest
-// RUN: test -f klee-last/test000003.ktest
+// RUN: test -f %T/klee-last/test000001.ktest
+// RUN: test -f %T/klee-last/test000002.ktest
+// RUN: test -f %T/klee-last/test000003.ktest
 
 #include <stdio.h>       
 #include <sys/types.h>
diff --git a/test/Runtime/POSIX/FreeArgv.c b/test/Runtime/POSIX/FreeArgv.c
index ceec4de2..4d2e5b75 100644
--- a/test/Runtime/POSIX/FreeArgv.c
+++ b/test/Runtime/POSIX/FreeArgv.c
@@ -1,18 +1,22 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --posix-runtime %t.bc --sym-args 1 1 1
-// RUN: test -f klee-last/test000001.free.err
-// RUN: test -f klee-last/test000002.free.err
-// RUN: test -f klee-last/test000003.free.err
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --posix-runtime %t.bc --sym-args 1 1 1 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.free.err
+// RUN: test -f %T/klee-last/test000002.free.err
+// RUN: test -f %T/klee-last/test000003.free.err
 
 int main(int argc, char **argv) {
+  // FIXME: Use FileCheck's CHECK-DAG to check source locations
   switch(klee_range(0, 3, "range")) {
   case 0:
+    // CHECK: free of global
     free(argv);
     break;
   case 1:
+    // CHECK: free of global
     free(argv[0]);
     break;
   case 2:
+    // CHECK: free of global
     free(argv[1]);
     break;
   }
diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c
index 293ee653..bd514d48 100644
--- a/test/Runtime/POSIX/Isatty.c
+++ b/test/Runtime/POSIX/Isatty.c
@@ -1,9 +1,9 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
 // RUN: %klee --libc=uclibc --posix-runtime %t.bc --sym-files 0 10 --sym-stdout 2>%t.log
-// RUN: test -f klee-last/test000001.ktest
-// RUN: test -f klee-last/test000002.ktest
-// RUN: test -f klee-last/test000003.ktest
-// RUN: test -f klee-last/test000004.ktest
+// RUN: test -f %T/klee-last/test000001.ktest
+// RUN: test -f %T/klee-last/test000002.ktest
+// RUN: test -f %T/klee-last/test000003.ktest
+// RUN: test -f %T/klee-last/test000004.ktest
 // RUN: grep -q "stdin is a tty" %t.log
 // RUN: grep -q "stdin is NOT a tty" %t.log
 // RUN: grep -q "stdout is a tty" %t.log
@@ -15,16 +15,21 @@
 #include <stdio.h>
 #include <assert.h>
 
+// FIXME: Use new FileCheck to check klee's output
 int main(int argc, char** argv) {
   int fd0 = 0; // stdin
   int fd1 = 1; // stdout
 
   int r = isatty(fd0);
+  // CHECK-DAG: stdin is a tty
+  // CHECK-DAG: stdin is NOT a tty
   if (r) 
     fprintf(stderr, "stdin is a tty\n");
   else fprintf(stderr, "stdin is NOT a tty\n");
   
   r = isatty(fd1);
+  // CHECK-DAG: stdout is a tty
+  // CHECK-DAG: stdout is NOT a tty
   if (r) 
     fprintf(stderr, "stdout is a tty\n");
   else fprintf(stderr, "stdout is NOT a tty\n");
diff --git a/test/Runtime/POSIX/Openat.c b/test/Runtime/POSIX/Openat.c
index d417ee47..3c17f976 100644
--- a/test/Runtime/POSIX/Openat.c
+++ b/test/Runtime/POSIX/Openat.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
 // RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
-// RUN: test -f klee-last/test000001.ktest
+// RUN: test -f %T/klee-last/test000001.ktest
 
 #include <assert.h>
 #include <fcntl.h>
diff --git a/test/Runtime/POSIX/PrgName.c b/test/Runtime/POSIX/PrgName.c
index dc6a4b8c..6bc682ca 100644
--- a/test/Runtime/POSIX/PrgName.c
+++ b/test/Runtime/POSIX/PrgName.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
 // RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-arg 10 >%t.log
-// RUN: test -f klee-last/test000001.ktest
-// RUN: test -f klee-last/test000002.ktest
+// RUN: test -f %T/klee-last/test000001.ktest
+// RUN: test -f %T/klee-last/test000002.ktest
 // RUN: grep -q "No" %t.log
 // RUN: grep -qv "Yes" %t.log
 
diff --git a/test/Runtime/POSIX/SeedAndFail.c b/test/Runtime/POSIX/SeedAndFail.c
index 740db664..d9bd7f8d 100644
--- a/test/Runtime/POSIX/SeedAndFail.c
+++ b/test/Runtime/POSIX/SeedAndFail.c
@@ -1,8 +1,8 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
-// RUN: rm -rf tmp-123
-// RUN: %klee --libc=uclibc --output-dir=tmp-123 --posix-runtime %t.bc --sym-files 1 10  2>%t.log
-// RUN: %klee --seed-out-dir=tmp-123 --zero-seed-extension --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1
-// RUN: ls klee-last | grep -c assert | grep 4
+// RUN: rm -rf %T/tmp-123
+// RUN: %klee --libc=uclibc --output-dir=%T/tmp-123 --posix-runtime %t.bc --sym-files 1 10  2>%t.log
+// RUN: %klee --seed-out-dir=%T/tmp-123 --zero-seed-extension --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1
+// RUN: ls %T/klee-last | grep -c assert | grep 4
 
 #include <string.h>
 #include <assert.h>
diff --git a/test/Solver/LargeIntegers.pc b/test/Solver/LargeIntegers.pc
index 53ff3a51..e0921393 100644
--- a/test/Solver/LargeIntegers.pc
+++ b/test/Solver/LargeIntegers.pc
@@ -2,16 +2,16 @@
 
 array a[64] : w32 -> w8 = symbolic
 
-# RUN: grep -A 1 \"Query 0\" %t > %t2
-# RUN: grep \"Expr 0:\t18446744073709551618\" %t2
+# RUN: grep -A 1 "Query 0" %t > %t2
+# RUN: grep "Expr 0:	18446744073709551618" %t2
 (query [] false [(Concat w128 (w64 1) (w64 2))])
 
-# RUN: grep -A 1 \"Query 1\" %t > %t2
-# RUN: grep \"Expr 0:\t16\" %t2
+# RUN: grep -A 1 "Query 1" %t > %t2
+# RUN: grep "Expr 0:	16" %t2
 (query [] false [(Extract w5 60 (Concat w128 (w64 1) (w64 2)))])
 
-# RUN: grep -A 1 \"Query 2\" %t > %t2
-# RUN: grep \"Array 0:\ta.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1\" %t2
+# RUN: grep -A 1 "Query 2" %t > %t2
+# RUN: grep "Array 0:	a.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1" %t2
 (query [(Eq 0x0102030405060708090A0B0C0D0E0F10 (ReadLSB w128 0 a))] 
        false 
        [] [a])
diff --git a/test/regression/2007-10-11-free-of-alloca.c b/test/regression/2007-10-11-free-of-alloca.c
index 71a16f6b..44a9ed4e 100644
--- a/test/regression/2007-10-11-free-of-alloca.c
+++ b/test/regression/2007-10-11-free-of-alloca.c
@@ -1,9 +1,10 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.free.err
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.free.err
 
 int main() {
   int buf[4];
+  // CHECK: 2007-10-11-free-of-alloca.c:8: free of alloca
   free(buf); // this should give runtime error, not crash
   return 0;
 }
diff --git a/test/regression/2007-10-11-illegal-access-after-free-and-branch.c b/test/regression/2007-10-11-illegal-access-after-free-and-branch.c
index fbbb99c3..73b3ed3f 100644
--- a/test/regression/2007-10-11-illegal-access-after-free-and-branch.c
+++ b/test/regression/2007-10-11-illegal-access-after-free-and-branch.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
-// RUN: %klee --optimize %t1.bc
-// RUN: test -f klee-last/test000001.ptr.err
+// RUN: %klee --optimize %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.ptr.err
 
 #include <stdlib.h>
 #include <stdio.h>
@@ -13,7 +13,10 @@ int main(int argc, char **argv) {
   unsigned char x = buf[1];
   free(buf);
   if (x)
+  {
+    // CHECK: 2007-10-11-illegal-access-after-free-and-branch.c:18: memory error: out of bound pointer
     return buf[2];
+  }
   klee_silent_exit(0);
   return 0;
 }
diff --git a/test/regression/2008-03-04-free-of-global.c b/test/regression/2008-03-04-free-of-global.c
index 7821398d..5351128d 100644
--- a/test/regression/2008-03-04-free-of-global.c
+++ b/test/regression/2008-03-04-free-of-global.c
@@ -1,10 +1,11 @@
-// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.free.err
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc 2>&1 | FileCheck %s
+// RUN: test -f %T/klee-last/test000001.free.err
 
 int buf[4];
 
 int main() {
+  // CHECK: 2008-03-04-free-of-global.c:9: free of global
   free(buf); // this should give runtime error, not crash
   return 0;
 }