|
|
|---|
|
|
|
|---|
A C-to-C transformation to split a function in two.
This transformation splits out the second half of a function. The function body of the original function is truncated at the split point, at which point it calls the new function containing the remainder of the statements. Necessary values are passed by pointer to the split-out function.
(split-fn const-old const-new :target ... ; required :new-fn ... ; required :split-point ... ; required )
Specifies the code to be transformed.
This must be a symbol that names an existing ACL2 constant that contains a translation unit ensemble, i.e. a value of type transunit-ensemble. This constant could result from c$::input-files, or from some other transformation.
Specifies the name of the constant for the transformed code.
This must be a symbol that is valid name for a new ACL2 constant.
A string denoting the identifier of the function which should be split.
Note: There is currently no way to specify the translation unit to allow for disambiguation of functions of the same name with internal linkage. Eventually, a :target-filepath keyword argument will be introduced to accommodate this case. Until then, the transformation will apply to all functions of the specified name.
A string denoting the identifier which shall be used as the name of the new function introduced by the transformation.
Note: This identifier should be free to avoid name conflict, but this condition is not current checked.
A natural number indicating the position in the function body at which to split. This is the number of top-levelblock itemsin the function body before the split point. Splits within nested statement blocks are not yet supported.