You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: doc/ccomp.1
+1-1
Original file line number
Diff line number
Diff line change
@@ -9,7 +9,7 @@ ccomp \- the CompCert C compiler
9
9
\fBCompCertC\fP is a compiler for the C programming language.
10
10
Its intended use is the compilation of life-critical and mission-critical software written in C and meeting high levels of assurance.
11
11
It accepts most of the ISO C 99 language, with some exceptions and a few extensions.
12
-
It produces machine code for the PowerPC (32bit), ARM (32bit), x86 (32bit and 64bit), and RISC-V (32bit and 64bit) architectures.
12
+
It produces machine code for the PowerPC (32bit), ARM (32bit), AArch64 (ARM 64bit), x86 (32bit and 64bit), and RISC-V (32bit and 64bit) architectures.
13
13
.PP
14
14
What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues.
15
15
In other words, the executable code it produces is proved to behave exactly as specified by the semantics of the source C program.
0 commit comments