This paper addresses the challenges of secure compilation in the face of speculative execution attacks like Spectre. We explore the integration of speculative semantics into CompCert, a formally verified compiler, to counter transient execution leaks. Key challenges include undefined behaviors during transient execution, which arise from transient memory access and function calls/returns. To mitigate these, we propose a protection pass inserting speculation barriers after branch instructions, ensuring constant time conservation. Additionally, a strict calling convention is introduced to decouple speculation analysis between functions, preventing cross-function interference. Our work highlights the necessity of formalizing speculation models in the case of real compiler, where inter-procedural analysis is not possible.