aboutsummaryrefslogtreecommitdiffhomepage
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
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.
-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;