diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2018-09-05 09:55:48 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-09-06 13:29:31 +0100 |
commit | cdce3e8385927bf2cf2a21902d6563ecea37262c (patch) | |
tree | 3b3daf8731b30acddb7783a28e8eb97637dae291 /test/Runtime | |
parent | d2285e097656936c866ae6518e0a496cf4499517 (diff) | |
download | klee-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.c | 9 | ||||
-rw-r--r-- | test/Runtime/POSIX/Isatty.c | 24 |
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; } |