[klee-dev] KLEE coverage

[Nowack, Martin]

Hi,

There are a couple of options to drive KLEE. First, use `-only-output-states-covering-new`, this only generates test cases which are covering new instructions.
Otherwise every path through an application found by KLEE will have a test case generated even though it doesn’t cover new instructions.
Second, vary the input `—sym-arg 3` reflecting the input needed by the application. Have a closer look here: https://klee.github.io/docs/options/#symbolic-environment
This helps to cover more code.

Best,
Martin

On 25. Jun 2018, at 03:35, Norlina Pasaribu <norlinap at xlfutureleaders.com<mailto:norlinap at xlfutureleaders.com>> wrote:

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<mailto: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:~$


_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed