Adrian Herrera

Ah ok, I did not realise this. Does the above commit fix the issue?

Do you have the correct SDK installed?

Hi all, Yes, I have noticed this contradiction also :) As you noted, the implementation is largely taken from the qemu version implemented for the "be sensitive and collaborative" paper....

Yeah what you say makes sense. It could also just be a mistake :) I will contact the authors and see what their reason is, because I am very curious...

This is a greatl idea! Maybe you can check out what S2E and RevGen do and see if there are any useful ideas there. Yeah, shameless plug :)

Not sure if people are still struggling with this, but I've made a PR that does exactly what @hexcoder suggested (https://github.com/AngoraFuzzer/Angora/pull/74). However, this still requires an abilist for libcrypto (because...

No. All of the instrumentation is based on the LLVM IR.

Hey Arie, Thanks for the reply! >Most of our own clients of sea-dsa ensure that functions always terminate by cutting out non-terminating paths. Do you mean like what CLAM does...

Thanks @caballa! Given that, does it suffice to generalize `HasReturn` (as used [here](https://github.com/seahorn/sea-dsa/blob/dev12/lib/seadsa/ShadowMem.cc#L914)) to also allow for `UnreachableInst`s and then only mark a cell with a `mem.out` marker [here](https://github.com/seahorn/sea-dsa/blob/dev12/lib/seadsa/ShadowMem.cc#L952) if...

Hey @agurfinkel and @caballa, Just wondering if you had any thoughts on https://github.com/seahorn/sea-dsa/pull/139?