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

Sumit Kumar sumit686215 at gmail.com
Thu May 19 16:24:29 BST 2016


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> 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> 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
> > 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
> ----------------------------------------------------
>
>
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list