Cristian Cadar

> Edit: Although presumably -O1 is just hiding some underlying KLEE bug? Is there a fundamental reason why this can't be detected in unoptimized code? @moyix Yes, this is a...

@251 looks like our messages crossed, or at least I only noticed yours after submitting mine. Now we only need to integrate the solution I mentioned into the mainline ;)

Indeed, one would have to be careful with the integration, as UAF detection techniques are likely to directly interfere with KLEE's memory model.

Indeed, I think this would be a nice extension to KLEE. I would guard all these calls with the same option.

@251 I believe this PR is now outdated and we can close it? (#1348 was merged)

Added `blockaddress` and `indirectbr`, reported in #615

@jyn514 Thanks, I added it to the list. We need to understand why these are not eliminated like other vectorized intrinsics. @MartinNowack any thoughts?

@operasfantom thanks, I added them to the list.

@hhs4240 this requires adding some documentation, would you be willing to write some? These two message threads are a good starting point (and they could be referenced on the website...

@kren1 do you have a small test? Can you open a new issue?