		Search-engine friendly clone of the ACL2 documentation.

Transformation-tools

Split-fn

A C-to-C transformation to split a function in two.

This transformation takes the identifier of the function it is to split, the name of the new function to be generated, and the location of the split, represented as a natural number corresponding to the number of block items in the function body before the split.

This transformation is a work in progress, and may fail in certain cases. For instance, it may fail given variables which have been declared but not yet initialized at the split point, or variables which are passed by reference after the split point.

Subtopics

Abstract-fn: Create a new function from the block items following the split-fn split point.
Split-fn-block-item-list: Transform a list of block items.
Decl-to-ident-paramdeclon-map: Convert a regular declaration into an omap of identifiers to parameter declarations.
Split-fn-fundef: Transform a function definition, splitting it if matches the target identifier, or else leaving it untouched.
Split-fn-extdecl: Transform an external declaration.
Split-fn-filepath-transunit-map: Transform a filepath.
Split-fn-extdecl-list: Transform a list of external declarations.
Param-declon-to-ident-paramdeclon-map: Convert a parameter declaration into a singleton omap associating the declared identifier to the declaration.
Split-fn-transunit-ensemble: Transform a translation unit ensemble.
Split-fn-transunit: Transform a translation unit.
Param-declon-list-to-ident-paramdeclon-map: Fold param-declon-to-ident-paramdeclon-map over a list.
Ident-paramdeclon-map-filter
Decl-to-ident-paramdeclon-map0
Decl-list-to-ident-paramdeclon-map: Fold decl-to-ident-paramdeclon-map over a list.
Expr-ident-list: Map c$::expr-list over a list.
Ident-paramdeclon-map: An omap mapping identp to param-declonp.