about summary refs log tree commit diff homepage
path: root/test
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
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')
-rw-r--r--test/CXX/StaticConstructor.cpp2
-rw-r--r--test/CXX/StaticDestructor.cpp11
-rw-r--r--test/Feature/InAndOutOfBounds.c8
-rw-r--r--test/Feature/KleeReportError.c14
-rw-r--r--test/Feature/MultipleFreeResolution.c20
-rw-r--r--test/Feature/OneFreeError.c3
-rw-r--r--test/Feature/OneOutOfBounds.c3
-rw-r--r--test/Feature/OvershiftCheck.c16
-rw-r--r--test/Feature/SourceMapping.c32
-rw-r--r--test/Feature/consecutive_divide_by_zero.c20
-rw-r--r--test/Feature/ubsan_signed_overflow.c9
-rw-r--r--test/Feature/ubsan_unsigned_overflow.c9
-rw-r--r--test/Runtime/POSIX/FreeArgv.c9
-rw-r--r--test/Runtime/POSIX/Isatty.c24
-rw-r--r--test/regression/2014-07-04-unflushed-error-report.c11
15 files changed, 84 insertions, 107 deletions
diff --git a/test/CXX/StaticConstructor.cpp b/test/CXX/StaticConstructor.cpp
index 56fcb97b..c184526e 100644
--- a/test/CXX/StaticConstructor.cpp
+++ b/test/CXX/StaticConstructor.cpp
@@ -20,7 +20,7 @@ public:
 Test t;
 
 int main() {
-  assert(t.getX()==22);
+  assert(t.getX() == 22);
 
   return 0;
 }
diff --git a/test/CXX/StaticDestructor.cpp b/test/CXX/StaticDestructor.cpp
index adc449a5..2cf01e3b 100644
--- a/test/CXX/StaticDestructor.cpp
+++ b/test/CXX/StaticDestructor.cpp
@@ -3,7 +3,7 @@
 // RUN: %llvmgxx %s -emit-llvm -g -O0 -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --optimize=false --libc=klee --no-output %t1.bc 2> %t1.log
-// RUN: grep ":17: memory error" %t1.log
+// RUN: FileCheck --input-file %t1.log %s
 
 #include <cassert>
 
@@ -12,14 +12,13 @@ class Test {
 
 public:
   Test() : p(0) {}
-  ~Test() { 
-    assert(!p); 
+  ~Test() {
+    assert(!p);
+    // CHECK: :[[@LINE+1]]: memory error
     assert(*p == 10); // crash here
   }
 };
 
 Test t;
 
-int main(int argc, char** argv) {
-  return 0;
-}
+int main(int argc, char **argv) { return 0; }
diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c
index 6eb8784a..9b913609 100644
--- a/test/Feature/InAndOutOfBounds.c
+++ b/test/Feature/InAndOutOfBounds.c
@@ -8,15 +8,15 @@
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
   klee_make_symbolic(&x, sizeof x, "x");
-  if (x-start>=end-start) klee_silent_exit(0);
+  if (x - start >= end - start)
+    klee_silent_exit(0);
   return x;
 }
 
 int main() {
   int *x = malloc(sizeof(int));
-  // FIXME: Use newer FileCheck syntax to support relative line numbers
-  // CHECK: InAndOutOfBounds.c:19: memory error: out of bound pointer
-  x[klee_urange(0,2)] = 1;
+  // CHECK: InAndOutOfBounds.c:[[@LINE+1]]: memory error: out of bound pointer
+  x[klee_urange(0, 2)] = 1;
   free(x);
   return 0;
 }
diff --git a/test/Feature/KleeReportError.c b/test/Feature/KleeReportError.c
index 4e21df18..96879a55 100644
--- a/test/Feature/KleeReportError.c
+++ b/test/Feature/KleeReportError.c
@@ -2,24 +2,24 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s
 // RUN: ls %t.klee-out/ | grep .my.err | wc -l | grep 2
-#include <stdio.h>
 #include <assert.h>
+#include <stdio.h>
 
-int main(int argc, char** argv) {
+int main(int argc, char **argv) {
   int x, y, *p = 0;
-  
+
   klee_make_symbolic(&x, sizeof x, "x");
   klee_make_symbolic(&y, sizeof y, "y");
 
   if (x)
     fprintf(stderr, "x\n");
-  else fprintf(stderr, "!x\n");
+  else
+    fprintf(stderr, "!x\n");
 
   if (y) {
     fprintf(stderr, "My error\n");
-    // CHECK: KleeReportError.c:23: My error
-    // CHECK: KleeReportError.c:23: My error
-    // FIXME: Use FileCheck's relative line number syntax
+    // CHECK: KleeReportError.c:[[@LINE+2]]: My error
+    // CHECK: KleeReportError.c:[[@LINE+1]]: My error
     klee_report_error(__FILE__, __LINE__, "My error", "my.err");
   }
 
diff --git a/test/Feature/MultipleFreeResolution.c b/test/Feature/MultipleFreeResolution.c
index 704057f9..5c7dfdd8 100644
--- a/test/Feature/MultipleFreeResolution.c
+++ b/test/Feature/MultipleFreeResolution.c
@@ -4,13 +4,14 @@
 // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 4
 // RUN: ls %t.klee-out/ | grep .err | wc -l | grep 3
 
-#include <stdlib.h>
 #include <stdio.h>
+#include <stdlib.h>
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
   klee_make_symbolic(&x, sizeof x, "x");
-  if (x-start>=end-start) klee_silent_exit(0);
+  if (x - start >= end - start)
+    klee_silent_exit(0);
   return x;
 }
 
@@ -22,21 +23,20 @@ int *make_int(int i) {
 
 int main() {
   int *buf[4];
-  int i,s;
+  int i, s;
 
-  for (i=0; i<3; i++)
+  for (i = 0; i < 3; i++)
     buf[i] = make_int(i);
   buf[3] = 0;
 
-  s = klee_urange(0,4);
+  s = klee_urange(0, 4);
 
   free(buf[s]);
 
-  // CHECK: MultipleFreeResolution.c:40: memory error: out of bound pointer
-  // CHECK: MultipleFreeResolution.c:40: memory error: out of bound pointer
-  // CHECK: MultipleFreeResolution.c:40: memory error: out of bound pointer
-  // FIXME: Use FileCheck's relative line numbers
-  for (i=0; i<3; i++) {
+  for (i = 0; i < 3; i++) {
+    // CHECK: MultipleFreeResolution.c:[[@LINE+3]]: memory error: out of bound pointer
+    // CHECK: MultipleFreeResolution.c:[[@LINE+2]]: memory error: out of bound pointer
+    // CHECK: MultipleFreeResolution.c:[[@LINE+1]]: memory error: out of bound pointer
     printf("*buf[%d] = %d\n", i, *buf[i]);
   }
 
diff --git a/test/Feature/OneFreeError.c b/test/Feature/OneFreeError.c
index 4f5a8c8c..64a0425d 100644
--- a/test/Feature/OneFreeError.c
+++ b/test/Feature/OneFreeError.c
@@ -6,8 +6,7 @@
 int main() {
   int *x = malloc(4);
   free(x);
-  // CHECK: OneFreeError.c:11: memory error: out of bound pointer
-  // FIXME: Use FileCheck's relative line numbers
+  // CHECK: OneFreeError.c:[[@LINE+1]]: memory error: out of bound pointer
   x[0] = 1;
   return 0;
 }
diff --git a/test/Feature/OneOutOfBounds.c b/test/Feature/OneOutOfBounds.c
index 85fb2a79..88a2ae43 100644
--- a/test/Feature/OneOutOfBounds.c
+++ b/test/Feature/OneOutOfBounds.c
@@ -5,8 +5,7 @@
 
 int main() {
   int *x = malloc(sizeof(int));
-  // CHECK: OneOutOfBounds.c:10: memory error: out of bound pointer
-  // FIXME: Use FileCheck's relative line numbers
+  // CHECK: OneOutOfBounds.c:[[@LINE+1]]: memory error: out of bound pointer
   x[1] = 1;
   free(x);
   return 0;
diff --git a/test/Feature/OvershiftCheck.c b/test/Feature/OvershiftCheck.c
index 09cbf8ba..ace54cee 100644
--- a/test/Feature/OvershiftCheck.c
+++ b/test/Feature/OvershiftCheck.c
@@ -1,26 +1,26 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out -check-overshift %t.bc 2> %t.log
-// RUN: grep -c "overshift error" %t.log
-// RUN: grep -c "OvershiftCheck.c:20: overshift error" %t.log
-// RUN: grep -c "OvershiftCheck.c:24: overshift error" %t.log
+// RUN: FileCheck --input-file %t.log %s
 
 /* This test checks that two consecutive potential overshifts
  * are reported as errors.
  */
-int main()
-{
-  unsigned int x=15;
+#include "klee/klee.h"
+int main() {
+  unsigned int x = 15;
   unsigned int y;
   unsigned int z;
   volatile unsigned int result;
 
   /* Overshift if y>= sizeof(x) */
-  klee_make_symbolic(&y,sizeof(y),"shift_amount1");
+  klee_make_symbolic(&y, sizeof(y), "shift_amount1");
+  // CHECK: OvershiftCheck.c:[[@LINE+1]]: overshift error
   result = x << y;
 
   /* Overshift is z>= sizeof(x) */
-  klee_make_symbolic(&z,sizeof(z),"shift_amount2");
+  klee_make_symbolic(&z, sizeof(z), "shift_amount2");
+  // CHECK: OvershiftCheck.c:[[@LINE+1]]: overshift error
   result = x >> z;
 
   return 0;
diff --git a/test/Feature/SourceMapping.c b/test/Feature/SourceMapping.c
index 9835d701..bc13652d 100644
--- a/test/Feature/SourceMapping.c
+++ b/test/Feature/SourceMapping.c
@@ -19,37 +19,25 @@
 
 // CHECK-NEXT: {{[1-9][0-9]*}} {{[1-9][0-9]*}}
 
-
-// Ensure we have the right line number (and check called function markers).
-// CHECK: fn=f1
-// CHECK: cfn=f0
-// CHECK-NEXT: calls=1 {{[1-9][0-9]*}}
-// CHECK-NEXT: {{[1-9][0-9]*}} 48 {{.*}}
-
-// This check just brackets the checks above, to make sure they fall in the
-// appropriate region of the run.istats file.
-//
-// CHECK: fn=main
-
-
-
-
-
-
-
-// KEEP THIS AS LINE 40
-
 int f0(int a, int b) {
   return a + b;
 }
 
 int f1(int a, int b) {
-  // f0 is called on line 48
+  // Ensure we have the right line number (and check called function markers).
+  // CHECK: fn=f1
+  // CHECK: cfn=f0
+  // CHECK-NEXT: calls=1 {{[1-9][0-9]*}}
+  // CHECK-NEXT: {{[1-9][0-9]*}} [[@LINE+1]] {{.*}}
   return f0(a, b);
 }
 
+// This check just brackets the checks above, to make sure they fall in the
+// appropriate region of the run.istats file.
+//
+// CHECK: fn=main
 int main() {
   int x = f1(1, 2);
-  
+
   return x;
 }
diff --git a/test/Feature/consecutive_divide_by_zero.c b/test/Feature/consecutive_divide_by_zero.c
index 31124ea4..ebe0dcb5 100644
--- a/test/Feature/consecutive_divide_by_zero.c
+++ b/test/Feature/consecutive_divide_by_zero.c
@@ -1,31 +1,31 @@
 // RUN: %llvmgcc -emit-llvm -c -g -O0 %s -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out -check-div-zero -emit-all-errors=0 %t.bc 2> %t.log
-// RUN: grep "completed paths = 3" %t.log
-// RUN: grep "generated tests = 3" %t.log
-// RUN: grep "consecutive_divide_by_zero.c:25: divide by zero" %t.log
-// RUN: grep "consecutive_divide_by_zero.c:28: divide by zero" %t.log
+// RUN: FileCheck --input-file=%t.log %s
 
 /* This test case captures a bug where two distinct division
 *  by zero errors are treated as the same error and so
 *  only one test case is generated EVEN IF THERE ARE MULTIPLE 
 *  DISTINCT ERRORS!
 */
-int main()
-{
-  unsigned int a=15;
-  unsigned int b=15;
+int main() {
+  unsigned int a = 15;
+  unsigned int b = 15;
   volatile unsigned int d1;
   volatile unsigned int d2;
 
-  klee_make_symbolic(&d1, sizeof(d1),"divisor1");
-  klee_make_symbolic(&d2, sizeof(d2),"divisor2");
+  klee_make_symbolic(&d1, sizeof(d1), "divisor1");
+  klee_make_symbolic(&d2, sizeof(d2), "divisor2");
 
   // deliberate division by zero possible
+  // CHECK: consecutive_divide_by_zero.c:[[@LINE+1]]: divide by zero
   unsigned int result1 = a / d1;
 
   // another deliberate division by zero possible
+  // CHECK: consecutive_divide_by_zero.c:[[@LINE+1]]: divide by zero
   unsigned int result2 = b / d2;
 
+  // CHECK: completed paths = 3
+  // CHECK: generated tests = 3
   return 0;
 }
diff --git a/test/Feature/ubsan_signed_overflow.c b/test/Feature/ubsan_signed_overflow.c
index c89065eb..8d01f7d3 100644
--- a/test/Feature/ubsan_signed_overflow.c
+++ b/test/Feature/ubsan_signed_overflow.c
@@ -4,8 +4,7 @@
 
 #include "klee/klee.h"
 
-int main()
-{
+int main() {
   signed int x;
   signed int y;
   volatile signed int result;
@@ -13,13 +12,13 @@ int main()
   klee_make_symbolic(&x, sizeof(x), "x");
   klee_make_symbolic(&y, sizeof(y), "y");
 
-  // CHECK: ubsan_signed_overflow.c:17: overflow on addition
+  // CHECK: ubsan_signed_overflow.c:[[@LINE+1]]: overflow on addition
   result = x + y;
 
-  // CHECK: ubsan_signed_overflow.c:20: overflow on subtraction
+  // CHECK: ubsan_signed_overflow.c:[[@LINE+1]]: overflow on subtraction
   result = x - y;
 
-  // CHECK: ubsan_signed_overflow.c:23: overflow on multiplication
+  // CHECK: ubsan_signed_overflow.c:[[@LINE+1]]: overflow on multiplication
   result = x * y;
 
   return 0;
diff --git a/test/Feature/ubsan_unsigned_overflow.c b/test/Feature/ubsan_unsigned_overflow.c
index 1300ffcc..e2d9592c 100644
--- a/test/Feature/ubsan_unsigned_overflow.c
+++ b/test/Feature/ubsan_unsigned_overflow.c
@@ -4,8 +4,7 @@
 
 #include "klee/klee.h"
 
-int main()
-{
+int main() {
   unsigned int x;
   unsigned int y;
   volatile unsigned int result;
@@ -13,13 +12,13 @@ int main()
   klee_make_symbolic(&x, sizeof(x), "x");
   klee_make_symbolic(&y, sizeof(y), "y");
 
-  // CHECK: ubsan_unsigned_overflow.c:17: overflow on addition
+  // CHECK: ubsan_unsigned_overflow.c:[[@LINE+1]]: overflow on addition
   result = x + y;
 
-  // CHECK: ubsan_unsigned_overflow.c:20: overflow on subtraction
+  // CHECK: ubsan_unsigned_overflow.c:[[@LINE+1]]: overflow on subtraction
   result = x - y;
 
-  // CHECK: ubsan_unsigned_overflow.c:23: overflow on multiplication
+  // CHECK: ubsan_unsigned_overflow.c:[[@LINE+1]]: overflow on multiplication
   result = x * y;
 
   return 0;
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;
 }
diff --git a/test/regression/2014-07-04-unflushed-error-report.c b/test/regression/2014-07-04-unflushed-error-report.c
index 0518fb4d..0b98944a 100644
--- a/test/regression/2014-07-04-unflushed-error-report.c
+++ b/test/regression/2014-07-04-unflushed-error-report.c
@@ -6,20 +6,17 @@
 /* This test checks that the error file isn't empty and contains the
  * right content.
  */
-int main()
-{
-  unsigned int x=15;
+int main() {
+  unsigned int x = 15;
   unsigned int y;
   unsigned int z;
   volatile unsigned int result;
 
   /* Overshift if y>= sizeof(x) */
-  klee_make_symbolic(&y,sizeof(y),"shift_amount1");
+  klee_make_symbolic(&y, sizeof(y), "shift_amount1");
   // CHECK: Error: overshift error
   // CHECK-NEXT: 2014-07-04-unflushed-error-report.c
-  // FIXME: Need newer FileCheck for to do ``Line: [[@LINE+1]]``
-  // Just hardcode line number for now
-  // CHECK-NEXT: Line: 23
+  // CHECK-NEXT: Line: [[@LINE+1]]
   result = x << y;
 
   return 0;