aboutsummaryrefslogtreecommitdiffstats
path: root/doc/ccomp.1
diff options
context:
space:
mode:
Diffstat (limited to 'doc/ccomp.1')
-rw-r--r--doc/ccomp.17
1 files changed, 1 insertions, 6 deletions
diff --git a/doc/ccomp.1 b/doc/ccomp.1
index 89e8c823..edae57e1 100644
--- a/doc/ccomp.1
+++ b/doc/ccomp.1
@@ -9,7 +9,7 @@ ccomp \- the CompCert C compiler
\fBCompCert C\fP is a compiler for the C programming language.
Its intended use is the compilation of life-critical and mission-critical software written in C and meeting high levels of assurance.
It accepts most of the ISO C 99 language, with some exceptions and a few extensions.
-It produces machine code for the PowerPC (32bit), ARM (32bit), x86 (32bit and 64bit), and RISC-V (32bit and 64bit) architectures.
+It produces machine code for the PowerPC (32bit), ARM (32bit), AArch64 (ARM 64bit), x86 (32bit and 64bit), and RISC-V (32bit and 64bit) architectures.
.PP
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.
In other words, the executable code it produces is proved to behave exactly as specified by the semantics of the source C program.
@@ -327,11 +327,6 @@ Language Support Options
.INDENT 0.0
.
.TP
-.BR \-fbitfields ", " \-fno\-bitfields
-Turn on/off support for emulation bit fields in structs.
-Disabled by default.
-.
-.TP
.BR \-flongdouble ", " \-fno\-longdouble
Turn on/off support for emulation of \fBlong double\fP as \fBdouble\fP.
Disabled by default.