Hello, I have an additional question on this comment: https://github.com/klee/klee/issues/1254 <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 following code fragment: ``` int *o1 = (int*)malloc(4); free(o1); int *o2 = (int*)malloc(4); *o1 = 10; /* use-after-free */ ``` The code uses the memory block allocated to the object 'o1' after it is freed (at line 2). ASan simply detects and reports it as 'use-after-free'. But, KLEE does not report an alarm when the second `malloc` allocates the same memory block as allocated by the first `malloc`. Since KLEE simply relies on the standard malloc semantics, the same memory block can be allocated. And, when there is a memory access, KLEE only checks whether the dereferenced memory block is *currently* valid. So, the last line `*o1 = 10` is valid because `o2 == o1`. Do you support any other mechanism to catch such an issue? Thank you. Best regards, Yoonseok
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
