		Search-engine friendly clone of the ACL2 documentation.

Syntax-for-tools

Input-files

Read C files from the file system into an ACL2 representation.

Introduction

In the name of this macro, input is best read as a verb: the macro inputs files into ACL2.

This macro takes as input a list of file paths (which must contain C code), reads those files from the file system, and performs a user-specified level of processing on them, yielding a representation in ACL2 of that C code. This representation can be further processed, e.g. to perform code transformations, after which the macro output-files can be used to write the transformed code to the file system.

The (non-event) macro input-files-prog provides a programmatic interface to the functionality of input-files.

General Form

(input-files :files             ...  ; no default
             :preprocess        ...  ; default nil
             :preprocess-args   ...  ; no default
             :process           ...  ; default :validate
             :const             ...  ; no default
             :gcc               ...  ; default nil
             :short-bytes       ...  ; default 2
             :int-bytes         ...  ; default 4
             :long-bytes        ...  ; default 8
             :long-long-bytes   ...  ; default 8
             :plain-char-signed ...  ; default nil
  )

Inputs

:files

List of zero or more file paths that specify the files to be read.
This must be a list of strings that are valid path names in the system. Non-absolute paths are relative to the connected book directory (see cbd).
This input to this macro is not evaluated.

:preprocess — default nil

Specifies the preprocessor to use, if any, on the files specified by the :files input.
This input must be one of the following:
nil (the default), in which case no preprocessing is done. In this case, the files must be already in preprocessed form, unless the :process input (see below) is nil.
A string, which names the preprocessor to use, which must be in the current path.
:auto, which implicitly names the preprocessor "cpp" (a common default), which must be in the current path.
The preprocessing (if this input is not nil), is performed via the preprocess-file tool.

:preprocess-args — no default

Specifies arguments to pass to the preprocessor.
This must either absent or a list of zero or more strings, each of which is an argument to pass, e.g. -I.
If :preprocess is nil, the :preprocess-args input must be absent.
If :preprocess is not nil, and the :preprocess-args input is absent, the arguments -E and -P are passed to the preprocessor, in that order.
If :preprocess is not nil, and :preprocess-args input is present, the argument -E is passed to the preprocessor, followed by the arguments in the list, in that order.
See the preprocessor documentation for information about the arguments mentioned above.

:process — default :validate

Specifies the processing to perform on the files specified by the :files input (if :preprocess is nil) or on the result of preprocessing those files (if :preprocess is not nil).
This input must be one of the following:
:parse, to parse the files into an abstract syntax representation, which may contain ambiguous constructs.
:disambiguate, to parse the files, and then to disambiguate the possibly ambiguous abstract syntax representation obtained from the parser into a non-ambiguous abstract syntax representation.
:validate (the default), to parse and disambiguate the files, and then to validate the disambiguated abstract syntax representation obtained from the disambiguator, which annotated the abstract syntax with validation information. Validation depends on the :short-bytes, :int-bytes, :long-bytes, :long-long-bytes, and :plain-char-signed inputs, which determine an implementation environment.
These levels of processing are ordered as
:parse < :disambiguate < :validate
where a larger level includes and extends the processing of smaller levels. These processing levels are orthogonal to the preprocessing specified by :preprocess, since they apply equally to either the original or the preprocessed files.

:const

Name of the generated ACL2 constant whose value is the final result of processing (and preprocessing) the files specified in the :files input.
If :process is :parse, the value of the constant named by :const is a translation unit ensemble (i.e. a value of type transunit-ensemble), containing the abstract syntax representation of the code resulting from the parser. Since the parser captures ambiguous constructs without resolving them, this representation may include ambiguous constructs.
If :process is :disambiguate, the value of the constant named by :const is a translation unit ensemble (i.e. a value of type transunit-ensemble), containing the abstract syntax representation of the code obtained by disambiguating the one resulting from the parser.
If :process is :validate, the value of the constant named by :const is a translation unit ensemble (i.e. a value of type transunit-ensemble), containing the abstract syntax representation of the code obtained by disambiguating the one resulting from the parser, and such that the abstract syntax representation passed validation; this abstract syntax is annotated with validation information.
In the rest of this documentation page, let *const* be the name of this constant.

:gcc — default nil

Boolean flag saying whether certain GCC extensions should be accepted or not.

:short-bytes — default 2

Positive integer saying how many bytes are used to represent signed short int and unsigned short int.
This must be at least 2.

:int-bytes — default 4

Positive integer saying how many bytes are used to represent signed int and unsigned int.
This must be at least 4, and not less than :short-bytes.

:long-bytes — default 8

Positive integer saying how many bytes are used to represent signed long int and unsigned long int.
This must be at least 8, and not less than :int-bytes.

:long-long-bytes — default 8

Positive integer saying how many bytes are used to represent signed long long int and unsigned long long int.
This must be at least 8, and not less than :long-bytes.

:plain-char-signed — default nil

Boolean saying whether the plain char type consists of the same value as the signed char or unsigned char type.

Generated Events

*const*

The named constant containing the result of processing, as specified by :process, the files specified by :files (if :preprocess is nil) or the files resulting from preprocessing those (if :preprocess is not nil).

Subtopics

Input-files-implementation: Implementation of input-files.
Input-files-prog: Programmatic interface to input-files.