|
|
|---|
|
|
|
|---|
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]', and `[GCC];
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 [GCC], we also give URL links,
which, given their form, may be useful to locate
documentation that has moved or otherwise changed,
given that [GCC] is a live document;
an example is [GCC:6], which currently refers to Section 6,
titled `Extensions to the C Language Family',
and whose URL includes
Although GCC provides extensions to the ISO/IEC standard, they 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.