		Search-engine friendly clone of the ACL2 documentation.

Simpadd0

Simpadd0-implementation

Implementation of simpadd0.

This transformation is implemented as a collection of ACL2 functions that operate on the abstract syntax, following the recursive structure of the abstract syntax. This is a typical pattern for C-to-C transformations, which we may want to partially automate, via things like generalized `folds' over the abstract syntax.

Subtopics

Simpadd0-exprs/decls/stmts: Transform expressions, declarations, statements, and related entities.
Simpadd0-gen-proofs-for-transunit-ensemble: Generate equivalence theorems for all functions in a translation unit ensemble.
Simpadd0-filepath: Transform a file path.
Simpadd0-gen-proofs-for-transunit: Generate equivalence theorems for all the functions in a translation unit.
Simpadd0-gen-proof-for-fun: Generate equivalence theorem for a function.
Simpadd0-transunit-ensemble: Transform a translation unit ensemble.
Simpadd0-filepath-transunit-map: Transform a map from file paths to translation units.
Simpadd0-extdecl-list: Transform a list of external declarations.
Simpadd0-fn: Event expansion of the transformation.
Simpadd0-transunit: Transform a translation unit.
Simpadd0-fundef: Transform a function definition.
Simpadd0-extdecl: Transform an external declaration.
Simpadd0-macro-definition: Definition of the simpadd0 macro.