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