		Search-engine friendly clone of the ACL2 documentation.

Input-files

Input-files-implementation

Implementation of input-files.

This also implements the programmatic interface input-files-prog. The flag progp, passed to some of the implementation functions below, says whether the programmatic interface has been called.

Subtopics

Input-files-process-inputs: Process the inputs.
Input-files-gen-events: Generate the events.
Input-files-process-preprocess-args: Process the :preprocess-args input.
Input-files-process-inputs-and-gen-events: Process the inputs and generate the events.
Input-files-complete-preprocess-extra-args: Extend the preprocessing arguments with a -std= flag.
Input-files-process-ienv: Process the :std, :gcc, :short-bytes, :int-bytes, :long-bytes, :long-long-bytes, :plain-char-signed inputs.
Input-files-fn: Event expansion of input-files from the inputs.
Input-files-read-files: Read a file set from a given set of paths.
Input-files-process-const: Process the :const inputs.
String-stringlist-map-map-cons-values: Cons a string to the value of each entry in an omap from strings to string lists.
Input-files-process-path: Process the :path input.
Input-files-process-files: Process the :files input.
Input-files-process-process: Process the :process input.
Input-files-preprocess-arg-std: Return the -std= flag reflecting the implementation environment.
Input-files-process-preprocess: Process the :preprocess input.
Input-files-process-keep-going: Process the :keep-going input.
Input-files-process-inputp: Recognize valid values of the :process input.
Input-files-preprocess-inputp: Recognize valid values of the :preprocess input.
*input-files-allowed-options*: Keyword options accepted by input-files.
Input-files-definition: Definition of the input-files macro.