blob: ebe0dcb54307e0e61ca3fc6054fdb258c47c019c (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
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: 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;
volatile unsigned int d1;
volatile unsigned int d2;
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;
}
|
