		Search-engine friendly clone of the ACL2 documentation.

C

An ACL2 library for C.

This library contains:

A formalization of (a subset of) the C language. This is a deep embedding of C in ACL2.
A representation of (a subset of) the C language constructs in ACL2. This is a shallow embedding of C in ACL2.
A proof-generating C code generator for ACL2. This recognizes, and translates to C, the shallowly embedded ACL2 representation of C constructs, and generates proofs based on the deep embedding.
A tool-oriented syntax of C.

The library is work in progress.

This library is based on the ISO/IEC 9899:2018 specification of C, i.e. the C17 standard. In the documentation of this library, this standard is referenced as `[C]'; sections are referenced by appending their designations separated by colon, e.g. `[C:6.2.6]' references Section 6.2.6; paragraphs are referenced by further appending their numbers separated by slash, e.g. `[C:6.2.5/2]' references Paragraph 2 of Section 6.2.5. These square-bracketed references may be used as nouns or parenthetically.

This library is also based on the documentation of GCC, particularly the extensions to the C language family. Although these are extensions to the standard, they are sufficiently prevalent and import that we need to take them into account when developing practical tools for C. But in the documentation of this ACL2 library, we are always careful to distinguish the C standard from the GCC extensions.

Subtopics

Syntax-for-tools: A syntax of C for use by tools.
Atc: ATC (ACL2 To C), a proof-generating C code generator for ACL2.
Language: A formal model of (a subset of) the C language.
Representation: A representation of C in ACL2.
Transformation-tools: Transformation tools for C.
Pack: Build a symbol in the C package from a list of atoms.