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

Re: [klee-dev] KLEE Slow execution while executing natively

2020-04-17 Thread Cristian Cadar
Improving the interpretation speed of KLEE is on our todo list. But KLEE's speed should be comparable to that of lli in interpreter mode (lli --force-interpreter=true). If you have examples where it's slower, I'd be curious to take a look, please open an issue on GitHub. Best, Cristian On