[klee-dev] Question on use-after-free detection.

[Frank Busse]

Hi,

On Sat, 2 Jan 2021 19:31:02 +0000
Cristian Cadar <c.cadar at imperial.ac.uk> wrote:

> You are right, KLEE doesn't catch this use-after-free bug currently,
> as it doesn't implement a quarantine.

Just a remark: KLEE's deterministic allocation mode (--allocate-determ)
implements an el cheapo arena allocator and just increments addresses.
Hence, in that mode it finds the bug.


Kind regards,

Frank