[klee-dev] KLEE coverage

[Norlina Pasaribu]

Anyone tell me how KLEE generate test case ? We tried to generate testcase
several times on the max time 60,  we got different number of test case
that generated for every generating about 1600 - 3000 test cases. We run
hat test cases and having some coverage.

on other condition we change max time different being 3600 and we got
56.000 test cases then run the test case and having coverage same with 1600
test cases.

I hope, I can get information 1600 test cases having same coverage with
56.000 test cases.

Thank you for attention



On Mon, Jun 25, 2018 at 9:14 AM, Norlina Pasaribu <
norlinap at xlfutureleaders.com> wrote:

> 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