blob: cea7c3b8a101f9f8fedbe36968e0a55ed5466c7a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
+++
title = "CompCert Internals"
date = "2020-12-10"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a"]
forwardlinks = ["3a2", "3a1a"]
zettelid = "3a1"
+++
CompCert has 11 intermediate languages, that are used to prove different
properties at each stage, as the higher level programming language is
translated to assembly. The main two parts are the front end and the
back end of the compiler.
|
