[klee-dev] Type of bugs that KLEE can find

[Cristian Cadar]

Hi,

The kind of bugs KLEE can find are memory errors (buffer overflows, null 
pointer dereference, etc.),  division/modulo by zero, overshifts, and 
assertion violations.  If I forgot anything, others should feel free to 
add to this list.  KLEE does not report memory leaks, but it could be 
extended to do so.

We should indeed document this better, so if anyone would like to add a 
complete list to the website, that would be great.

Best,
Cristian

On 17/04/2020 11:05, XIE Xuan wrote:
> Dear all,
> 
> I would like to ask what types of bugs can KLEE find?  I only find a 
> simple introduction about the error KLEE report here: 
> http://klee.github.io/tutorials/testing-regex/
> 
> Do you have detailed documentation?
> 
> What’s more, is KLEE able to discover memory leak, i.e. forget to free() 
> after malloc()? From the introduction above, it seems that KLEE is not 
> able to find it.
> 
> Thanks!
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>