923e4770_The_CompCertTSO_compiler__Pass
[Source & target] Linear to Mach [Compiler code] Bounds Stacking [Correctness proof] Stackingproof [Pass] 
Laying out the activation records
The CompCertTSO compiler
Pass