diff options
-rw-r--r-- | test/Feature/KleeStatsBranches.c | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/test/Feature/KleeStatsBranches.c b/test/Feature/KleeStatsBranches.c new file mode 100644 index 00000000..a1bf2721 --- /dev/null +++ b/test/Feature/KleeStatsBranches.c @@ -0,0 +1,84 @@ +// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-no-tests --output-dir=%t.klee-out %t.bc 2> %t.log +// RUN: %klee-stats --print-columns 'BrConditional,BrIndirect,BrSwitch,BrCall,BrMemOp,BrResolvePointer,BrAlloc,BrRealloc,BrFree,BrGetVal' --table-format=csv %t.klee-out > %t.stats +// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.stats %s + +#include "klee/klee.h" + +#include <stdlib.h> + + +void foo(void) {} +void bar(void) {} + +int memop(void) { + int *p; + klee_make_symbolic(&p, sizeof(p), "p"); + return *p; +} + + +int main(void) { + // alloc + size_t size0; + klee_make_symbolic(&size0, sizeof(size_t), "size0"); + klee_assume(size0 < 10); + void *p; + + // realloc + size_t size1; + klee_make_symbolic(&size1, sizeof(size_t), "size1"); + klee_assume(size1 < 20); + + // conditional + int cond; + klee_make_symbolic(&cond, sizeof(cond), "cond"); + + // switch + int sw_cond; + klee_make_symbolic(&sw_cond, sizeof(sw_cond), "sw_cond"); + + // call + void (*fptr)(void); + klee_make_symbolic(&fptr, sizeof(fptr), "fptr"); + klee_assume((fptr == &foo) | (fptr == &bar)); + + // indirectbr + void *lptr; + klee_make_symbolic(&lptr, sizeof(lptr), "lptr"); + klee_assume((lptr == &&one) | (lptr == &&two)); + goto *lptr; + + +one: + p = malloc(size0); + if (p) { + p = realloc(p, size1); + if (p) { + // free + klee_make_symbolic(&p, sizeof(p), "p"); + free(p); + } + } + + return 1; + +two: + switch (sw_cond) { + case 8: memop(); break; // memop + case 15: (*fptr)(); break; + default: { + int c = 42; + // conditional + if (cond) c++; + return c; + } + } + + return 2; +} + +// Check that we create branches +// CHECK-STATS: BrConditional,BrIndirect,BrSwitch,BrCall,BrMemOp,BrResolvePointer,BrAlloc,BrRealloc,BrFree,BrGetVal +// CHECK-STATS: 1,1,2,1,{{[1-9][0-9]*}},{{[1-9][0-9]*}},2,1,1,0 |