+++ title = "CompcertSSA " author = "Yann Herklotz" tags = [] categories = [] backlinks = ["3a9", "3a8g", "3a7", "2e1b1b"] forwardlinks = ["3c", "1c6", "3a9", "3a8a"] zettelid = "3a8" +++ CompcertSSA[^1] \[1\] is a version of CompCert that integrates a static single assignment (SSA) form as a middle-end optimisation platform in CompCert. The main workflow is to go from RTL to SSA and then back to RTL, which means that it could be easily added onto Vericert ([\#3c]). This would allow for more optimisations that may benefit from a static single assignment, such as modulo scheduling even ([\#1c6]).