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_now...@tu-dresden.de
<mailto:martin_now...@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 <sumit686...@gmail.com
    <mailto:sumit686...@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@imperial.ac.uk <mailto:klee-dev@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_now...@tu-dresden.de <mailto:martin_now...@tu-dresden.de>
    ----------------------------------------------------




_______________________________________________
klee-dev mailing list
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

Reply via email to