|
|
|---|
|
|
|
|---|
An ACL2 library for C.
This library contains:
The library is work in progress.
This library is based on:
In the documentation of this library,
these source are referenced as `[C23]', `[C17]', `[GCCM]', and `[GCCL]';
sections are referenced
by appending their designations separated by colon,
e.g. `[C17:6.2.6]' references Section 6.2.6 of [C17];
paragraphs are referenced
by further appending their numbers separated by slash,
e.g. `[C17:6.2.5/2]' references Paragraph 2 of Section 6.2.5 of [C17].
These square-bracketed references may be used
as nouns or parenthetically.
In the case of [GCCM] and [GCCL], we also give URL links,
which, given the characters that form them, may be useful to locate
documentation that has moved or otherwise changed,
given that [GCCM] and [GCCL] are live documents;
an example is [GCCM:6], which currently refers to Section 6 of [GCCM],
titled `Extensions to the C Language Family',
and whose URL includes
The GCC extensions to the ISO/IEC standard are sufficiently prevalent and important that we need to take them into account for our library of C to be of practical use. But in the documentation of this ACL2 library, we always clearly distinguish between standard C and GCC extensions.
When referencing concepts that are the same in [C23] and [C17], we prefer to just reference [C23]. However, since we started developing this library before [C23], there are still many references to [C17]. When there is some difference between [C17] and [C23], we take care to reference both.