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

Martin Nowack martin_nowack at tu-dresden.de
Thu May 19 14:01:58 BST 2016


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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20160519/3805759b/attachment.sig>


More information about the klee-dev mailing list