about summary refs log tree commit diff homepage
path: root/test/Runtime
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/Runtime
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/Runtime')
-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
7 files changed, 35 insertions, 26 deletions
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>