about summary refs log tree commit diff homepage
path: root/test/Runtime
diff options
context:
space:
mode:
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;
 }