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

2020-04-17 Thread 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

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

2020-04-17 Thread XIE Xuan
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