about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
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;
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-11 07:21:07 +0000