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 <norli...@xlfutureleaders.com<mailto:norli...@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 <norli...@xlfutureleaders.com<mailto:norli...@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@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@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@d376710b7e96:~$ _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk<mailto:klee-dev@imperial.ac.uk> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
