  Current compilers implement security features and optimizations that require
nontrivial semantic reasoning about pointers and memory allocation: the program
after the insertion of the security feature, or after applying the
optimization, must simulate the original program despite a different memory
layout. In this article, we illustrate such reasoning on pointer allocations
through memory extensions and injections, as well as fine points on undefined
values, by explaining how we implemented and proved correct two security
features (stack canaries and pointer authentication) and one optimization (tail
recursion elimination) in the CompCert formally verified compiler.
