diff options
Diffstat (limited to 'test/Feature/consecutive_divide_by_zero.c')
| -rw-r--r-- | test/Feature/consecutive_divide_by_zero.c | 20 |
1 files changed, 10 insertions, 10 deletions
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; } |