[klee-dev] Sample STP problems

Is it possible to get hold of some sample STP problems generated by Klee in the course of analyzing some code? (Or problems generated for input to some other solver such as Z3 would be fine, too.) I haven't been able to find any in the links from the website.

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

Hello, I have an additional question on this comment: https://github.com/klee/klee/issues/1254 @ccadar mentioned that KLEE already finds the kind of bugs that AddressSanitizer detects, but I don't clearly understand. For example, consider the

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

You are right, KLEE doesn't catch this use-after-free bug currently, as it doesn't implement a quarantine. It wouldn't it be too hard to add this though (you might want to refer to the ASan paper for details). Best, Cristian On 02/01/2021 18:16, Yoonseok Ko wrote: Hello,  I have an

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

Hi, On Sat, 2 Jan 2021 19:31:02 + Cristian Cadar 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