[klee-dev] KLEE coverage

[Norlina Pasaribu]

Hallo all,

Some papers tell that KLEE having good coverage, but I am still confuce
about my implementation for Space program C from http://sir.unl.edu/,
because I just only find 9% branch coverage for that program. Any one would
tell me How KLEE run test case ? thank you.

Here is the result of the KLEE's execution on Space program

klee at d376710b7e96:~$ klee --optimize --libc=uclibc --posix-runtime
./space.bc --sym-arg 3

KLEE: NOTE: Using klee-uclibc :
/home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca

KLEE: NOTE: Using model:
/home/klee/klee_build/klee/Release+Debug+Asserts/lib/libkleeRuntimePOSIX.bca

KLEE: WARNING: cannot create klee-last symlink: Is a directory

KLEE: output directory is "/home/klee/./klee-out-1"

KLEE: Using STP solver backend

KLEE: WARNING: undefined reference to function: __ctype_b_loc

KLEE: WARNING: undefined reference to function: acos

KLEE: WARNING: undefined reference to function: asin

KLEE: WARNING: undefined reference to function: atan

KLEE: WARNING: undefined reference to function: cos

KLEE: WARNING: undefined reference to function: pow

KLEE: WARNING: undefined reference to function: puts

KLEE: WARNING: undefined reference to function: sin

KLEE: WARNING: undefined reference to function: sqrt

KLEE: WARNING: executable has module level assembly (ignoring)

KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 45833072) at
/home/klee/klee_src/runtime/POSIX/fd.c:1044

KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled.
Using alignment of 8.

KLEE: WARNING ONCE: calling external: puts(42350896) at
/home/klee/space.c:2879

*******************************************************************************

KLEE: WARNING ONCE: calling external: printf(51242496, 4607182418800017408)
at /home/klee/space.c:2880

                         ARRAY PREPROCESSOR ver. 1.0

*******************************************************************************

*******************************************************************************

                         ARRAY PREPROCESSOR ver. 1.0

*******************************************************************************

*******************************************************************************

                         ARRAY PREPROCESSOR ver. 1.0

*******************************************************************************

*******************************************************************************

                         ARRAY PREPROCESSOR ver. 1.0

*******************************************************************************

** ERROR 21: Can not open input file: ** ERROR 21: Can not open input file:
#** ERROR 23: Empty input file: /** ERROR 21: Can not open input file: /#**
ERROR 21: Can not open input file: #/** ERROR 21: Can not open input file:
##** ERROR 21: Can not open input file: //#** ERROR 21: Can not open input
file: #/#** ERROR 21: Can not open input file: /#/** ERROR 23: Empty input
file: //

KLEE: done: total instructions = 151474

KLEE: done: completed paths = 13

KLEE: done: generated tests = 13

** ERROR 21: Can not open input file: ###** ERROR 21: Can not open input
file: /klee at d376710b7e96:~$ klee-stats klee-last

------------------------------------------------------------------------

|  Path   |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|

------------------------------------------------------------------------

|klee-last| 4391343|    59.51|    12.42|     9.05|   21068|       27.99|

------------------------------------------------------------------------

klee at d376710b7e96:~$
-------------- next part --------------
HTML attachment scrubbed and removed