Hi Cristian, Thanks for pointing me in the right direction. It has helped me a lot.
-- Thanks and Regards, Sumit On 19 May 2016 at 21:50, Cristian Cadar <c.ca...@imperial.ac.uk> wrote: > 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 >
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
