blob: e59edd1d541dde691d0336a1c69e8664b6310ed2 (
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
32
33
34
35
36
37
38
39
40
41
42
43
|
// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee -max-static-fork-pct=0.2 -max-static-pct-check-delay=1 --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck --check-prefix=CHECK-pt2 %s
// RUN: rm -rf %t.klee-out
// RUN: %klee -max-static-fork-pct=0.5 -max-static-pct-check-delay=1 --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck --check-prefix=CHECK-pt5 %s
// RUN: rm -rf %t.klee-out
// RUN: %klee -max-static-fork-pct=0.8 -max-static-pct-check-delay=1 --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck --check-prefix=CHECK-pt8 %s
// RUN: rm -rf %t.klee-out
// RUN: %klee -max-static-cpfork-pct=0.5 -max-static-pct-check-delay=1 --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck --check-prefix=CHECK-cppt5 %s
#include "klee/klee.h"
#include <stdio.h>
int main() {
#define N 4
int x[10], i;
klee_make_symbolic(&x, sizeof(x), "x");
if (x[0])
printf("x[0] ");
else printf("NOT x[0] ");
if (x[1])
// CHECK-pt2: skipping fork and concretizing condition (MaxStatic*Pct limit reached)
// CHECK-cppt5: skipping fork and concretizing condition (MaxStatic*Pct limit reached)
printf("x[1] ");
else printf("NOT x[1] ");
for (i = 2; i < 10; i++) {
if (x[i])
// CHECK-pt5: skipping fork and concretizing condition (MaxStatic*Pct limit reached)
// CHECK-pt8: skipping fork and concretizing condition (MaxStatic*Pct limit reached)
printf("x[%d] ", i);
else printf("NOT x[%d] ", i);
}
// CHECK-pt2: completed paths = 4
// CHECK-pt5: completed paths = 8
// CHECK-pt8: completed paths = 17
// CHECK-cppt5: completed paths = 2
return 0;
}
|
