The C programming language is notionally defined by an ISO standard, however over time the “de facto” usage of the language has diverged from that standard semantics. The main point of disagreement concerns the memory object model, and in particular the semantics of pointers. While system programmers often rely on a very concrete view of pointers (sometimes even more concrete than what the ISO standard describes), compiler implementers take a more abstract view. Some compiler optimisations, in particular those based on alias-analysis, reason about the provenance of pointers: how pointer values are constructed during the program execution, instead of only considering their representations and types.

In this talk, we present Cerberus: an executable semantics for a substantial fragment of C capturing that ISO specification, while reconciling the concrete and abstract views of the C memory model with a notion of pointer provenance that admits many systems-programming idioms and compiler optimisations, and which has been approved in principle by the WG14 and WG21 C/C++ ISO standards committees. The model is defined by elaboration into a intermediate language, Core, while retaining some level of implementation agnosticism. Being executable, Cerberus can be used as an oracle for exploring the range of behaviours that one should expect for reasonably sized programs, including all the C undefined behaviours. Web interfaces support interactive exploration and bounded model-checking: https://cerberus.cl.cam.ac.uk/cerberus and https://cerberus.cl.cam.ac.uk/bmc.html.