CompCertGSA This is the version of CompCertSSA with support for Gated-SSA. GSA is implemented in the following files: ./midend/GSA*.v: Contains the main syntax definition, specification and proofs. ./midend/SSA/ExternGSAgen.ml: Contains some unverified translations used in the GSA generation. The following files were take from an existing development doing WCET analysis. ./midend/SSA/bourdoncleAux.ml: Used to detect loop headers. ./midend/SSA/bourdoncleIterator.ml: Underlying implementation of Bourdoncle. ./midend/Bourdoncle.v: Coq interface to Bourdoncle. In addition to that, it requires the following dependencies to compile: OCaml 4.10.2 Coq 8.13.2 Z3 4.8.12 MenhirLib 20211012 The following should set up the correct environment (the z3 command line program may also need to be installed in case link errors are encountered during the final compilation steps): opam switch create 4.10.2 # Use OCaml version 4.10.2 (for example) eval $(opam env --switch=4.10.2) opam install coq=8.13.2 # Use Coq version 8.13.2 (for example) opam install menhir z3 It should then be possible to compile CompCertGSA using the provided makefile (more information can be found in the CompCert manual): ./configure x86_64-linux make all The compiler with GSA enabled can then be run using: ./ccomp -stdlib ./runtime -ssa gsa -dgsa main.c This will create a binary that can be executed, as well as a main.gsa.0, which contains the GSA version of the program. To run the simple test suite included in CompCert, the following command can be run: make -C test/c SSA_MODE="-ssa gsa -dgsa"