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

[Sumit Kumar]

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.cadar at 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_nowack at tu-dresden.de
>> <mailto: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
>>     <mailto: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 <mailto: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 <mailto:
>> martin_nowack at tu-dresden.de>
>>     ----------------------------------------------------
>>
>>
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed