| 123456789101112131415 |
- The CompCert C verified compiler is a compiler for a large subset
- of the C programming language that generates code for the PowerPC,
- ARM and x86 processors.
- The distinguishing feature of CompCert is that it has been formally
- verified using the Coq proof assistant: the generated assembly code
- is formally guaranteed to behave as prescribed by the semantics of
- the source C code.
- CompCert is not free software. This non-commercial release can only
- be used for evaluation, research, educational and personal purposes.
- A commercial version of CompCert, without this restriction and with
- professional support, can be purchased from AbsInt. See the file
- LICENSE for more information.
|
