CompCert only exposes global pointers in trace. How difficult would be to change the overall development to expose the local pointers in trace? I understand preservation of the trace would be the major concern, but want to know from CompCert experts if it is even feasible.