[klee-dev] why do I get a very low value of BCov / branch coverage

[Cristian Cadar]

Hi Sumit, the coverage reported is for the LLVM bitcode.  If you look in 
klee-last/assembly.ll, you'll see that there is additional code being 
linked by KLEE, which is unreachable from main().  If you want to obtain 
coverage at the source code level, you need to replay the generated test 
cases and use gcov, as explained in the tutorials.

Best,
Cristian

On 19/05/2016 16:24, Sumit Kumar wrote:
> Hi Martin,
>
> Thanks for replying :)
>
> I invoked KLEE in the following way:
>     klee  -solver-backend=z3 -max-depth=5 -search=dfs example.bc
>
> Then to get the BCov value I used the following command:
>     klee-stats klee-last/
>
> BCov value is shown as 22.22 %.
>
> --
> Thanks and Regards,
> Sumit
>
> On 19 May 2016 at 18:31, Martin Nowack <martin_nowack at tu-dresden.de
> <mailto:martin_nowack at tu-dresden.de>> wrote:
>
>     Hi Sumit,
>
>     How did you execute KLEE? What are the parameters?
>
>     Cheers,
>     Martin
>     > On 17 May 2016, at 20:44, Sumit Kumar <sumit686215 at gmail.com
>     <mailto:sumit686215 at gmail.com>> wrote:
>     >
>     > Hi Everyone,
>     >
>     > I am getting a BCov value of 22 % for the bitcode input
>     corresponding to the following program although all the branches
>     seem to have been taken:
>     >
>     >     int x;
>     >     int y;
>     >     int z;
>     >     klee_make_symbolic(&x, sizeof(x), "x");
>     >     klee_make_symbolic(&y, sizeof(y), "y");
>     >     klee_make_symbolic(&z, sizeof(z), "z");
>     >     if(x < 1){
>     >         if(y < 0)
>     >         y = 0;
>     >     }
>     >     else{
>     >         y = 1;
>     >     }
>     >
>     > Can anyone please explain why the branch coverage is so low ? I am
>     using llvm 2.9.
>     >
>     > --
>     > Thanks and Regards,
>     > Sumit
>     > _______________________________________________
>     > 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
>
>     ---------------------------------------------------
>     Martin Nowack
>     Research Assistant
>
>     Technische Universität Dresden
>     Computer Science
>     Institute of Systems Architecture
>     Systems Engineering
>     01062 Dresden
>
>     Phone: +49 351 463 39608
>     Email: martin_nowack at tu-dresden.de <mailto:martin_nowack at tu-dresden.de>
>     ----------------------------------------------------
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>