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/Feature | |
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/Feature')
-rw-r--r-- | test/Feature/InAndOutOfBounds.c | 8 | ||||
-rw-r--r-- | test/Feature/KleeReportError.c | 14 | ||||
-rw-r--r-- | test/Feature/MultipleFreeResolution.c | 20 | ||||
-rw-r--r-- | test/Feature/OneFreeError.c | 3 | ||||
-rw-r--r-- | test/Feature/OneOutOfBounds.c | 3 | ||||
-rw-r--r-- | test/Feature/OvershiftCheck.c | 16 | ||||
-rw-r--r-- | test/Feature/SourceMapping.c | 32 | ||||
-rw-r--r-- | test/Feature/consecutive_divide_by_zero.c | 20 | ||||
-rw-r--r-- | test/Feature/ubsan_signed_overflow.c | 9 | ||||
-rw-r--r-- | test/Feature/ubsan_unsigned_overflow.c | 9 |
10 files changed, 59 insertions, 75 deletions
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; |