🦞🌯 Lobster Roll

Also, see [Firm's comparison with LLVM](https://pp.ipd.kit.edu/firm/LLVM.html)

Abstract: > LLVM miscompiles certain programs in C, C++, and Rust that use low-level language features such as raw pointers in Rust or conversion between integers and pointers in C or C++. The problem is that it is difficult for the compiler to implement aggressive, high-level memory optimizations...

Abstract: "A key ingredient contributing to the success of CompCert, the state-of-the-art verified compiler for C, is its block-based memory model, which is used uniformly for all of its languages and their verified compilation. However, CompCert’s memory model lacks an explicit notion of stack. I...