Open jeehoonkang opened 9 years ago
We're discussing the issues with extraction in another thread, and I think we talked about adding the tag checking to stores on Skype. That and the update to malloc I think are correct w.r.t the semantics of LLVM/C, respectively.
The apparent typo in callFree__extcall_properties is troubling. I'm still not sure I understand external_intrinsics.v -- why does a call to malloc/free result in an empty trace?
Nitpicking:
Cd "./otherdir"
in the extraction script.