about summary refs log tree commit diff homepage
path: root/test/Runtime
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2018-09-05 09:55:48 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-09-06 13:29:31 +0100
commitcdce3e8385927bf2cf2a21902d6563ecea37262c (patch)
tree3b3daf8731b30acddb7783a28e8eb97637dae291 /test/Runtime
parentd2285e097656936c866ae6518e0a496cf4499517 (diff)
downloadklee-cdce3e8385927bf2cf2a21902d6563ecea37262c.tar.gz
Use FileCheck and LINE instead of grep if possible
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers.
Diffstat (limited to 'test/Runtime')
-rw-r--r--test/Runtime/POSIX/FreeArgv.c9
-rw-r--r--test/Runtime/POSIX/Isatty.c24
2 files changed, 15 insertions, 18 deletions
diff --git a/test/Runtime/POSIX/FreeArgv.c b/test/Runtime/POSIX/FreeArgv.c
index 8f812b5d..7a5445a3 100644
--- a/test/Runtime/POSIX/FreeArgv.c
+++ b/test/Runtime/POSIX/FreeArgv.c
@@ -6,18 +6,17 @@
 // RUN: test -f %t.klee-out/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")) {
+  switch (klee_range(0, 3, "range")) {
   case 0:
-    // CHECK: free of global
+    // CHECK-DAG: [[@LINE+1]]: free of global
     free(argv);
     break;
   case 1:
-    // CHECK: free of global
+    // CHECK-DAG: [[@LINE+1]]: free of global
     free(argv[0]);
     break;
   case 2:
-    // CHECK: free of global
+    // CHECK-DAG: [[@LINE+1]]: free of global
     free(argv[1]);
     break;
   }
diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c
index fdfc6ceb..b9232e01 100644
--- a/test/Runtime/POSIX/Isatty.c
+++ b/test/Runtime/POSIX/Isatty.c
@@ -5,35 +5,33 @@
 // RUN: test -f %t.klee-out/test000002.ktest
 // RUN: test -f %t.klee-out/test000003.ktest
 // RUN: test -f %t.klee-out/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
-// RUN: grep -q "stdout is NOT a tty" %t.log
+// RUN: FileCheck --input-file=%t.log %s
 
 // Depending on how uClibc is compiled (i.e. without -DKLEE_SYM_PRINTF)
 // fprintf prints out on stdout even if stderr is provided.
-#include <unistd.h>
-#include <stdio.h>
 #include <assert.h>
+#include <stdio.h>
+#include <unistd.h>
 
-// FIXME: Use new FileCheck to check klee's output
-int main(int argc, char** argv) {
+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) 
+  if (r)
     fprintf(stderr, "stdin is a tty\n");
-  else fprintf(stderr, "stdin is NOT 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) 
+  if (r)
     fprintf(stderr, "stdout is a tty\n");
-  else fprintf(stderr, "stdout is NOT a tty\n");
+  else
+    fprintf(stderr, "stdout is NOT a tty\n");
 
   return 0;
 }