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.

In CompCert, only volatile load produces an event (trace). I would like to also produce some observable event in case of non-volatile load. My question is why this design decision was taken and where difficulty might arise in preserving the trace?