AbsInt
Add explicit tail calls to Clight and C#minor
By popular demand.
The tail call optimization pass performed later in CompCert will not turn a call into a tail call if the function has stack-allocated data, because this might change the semantics.
Having an explicit Stailcall form in Clight makes it possible to force a call in tail position to be a tail call, deallocating stack-allocated data before the call. This is the same reason why we have an Stailcall form in Cminor already.
Cc: @andrew-appel
I would have thought that ExportClight.ml would also need to be edited, but I don't see that in the list of "files changed."
Yes, I'm pretty sure it does. I don't have time to test it this month. I recommend merge the P.R. Thank you.