Compcert for CertiKOS

This repository contains changes to Compcert that are used for the CertiKOS project.

The branch master is the unchanged master branch from the AbsInt repository. Additionally, we maintain a series of patches to Compcert 2.7 as individual (but cumulative) branches:

• param-memory-model parametrizes the implementation of the memory model and the semantics of external functions.
  • param-memory-model-coq85 is based on Compcert 2.7.1 and builds with Coq 8.5
• strong-unchanged-on adds a boolean field to the massert structure of Separation.v which indicates whether (what turns out in CertiKOS to be) the abstract data should be considered as part of the footprint. The field is used to choose between the old Mem.unchanged_on and a new Mem.strong_unchanged_on which are identical in the canonical implementation of the memory model, but may be different in alternative implementations.
• disable-unusedglob disables the Unusedglob pass, so that the structure of source and target global environments remain identical.
• compcert-certikos is the version of Compcert used as a submodule in our CertiKOS repository, which includes some more changes needed for CertiKOS.

While we hope that some version of param-memory-model will eventually be integrated upstream, the other patches are not necessarily intended as clean, general-purpose, long-term modifications to Compcert.