		Search-engine friendly clone of the ACL2 documentation.

Preprocess-files

Preprocess a set of files.

Signature
(preprocess-files files &key (path '".") (out-dir 'nil) (save ':auto) (preprocessor '"cpp") (extra-args ''("-P")) (state 'state)) → (mv erp map state)
Arguments: files — The file path list specifying C file to preprocess.
Guard (string-listp files).; path — The base path to which files are relative. By default, the value is "." (the current working directory).
Guard (stringp path).; out-dir — This specifies the directory that preprocessed output files are saved to with posfix ".i". If nil, temporary files will be created (see oslib::tempfile).
Guard (or (not out-dir) (stringp out-dir)).; save — If t, the output files are saved. If nil, the files are removed after reading them in. If :auto, the default value, files will be saved only if an explicit out-dir value is provided.; preprocessor — The preprocessor executable to use. The default is "cpp". Other reasonable values might be "gcc", "clang", "cc", etc.
Guard (stringp preprocessor).; extra-args — Arguments to pass to the C preprocessor, in addition to "-E". The default value is (list "-P") (the flag "-P" suppresses the generation of linemarkers).
Guard (string-listp extra-args).
Returns: erp — nil if successful, or the first error msgp otherwise.; map — The map from filepaths to preprocessed filedata.
Type (filesetp map).

This function preprocesses a filepath-setp. See preprocess-file for a similar utility which operates on individuals files.

Definitions and Theorems

Function: preprocess-files-fn

(defun preprocess-files-fn
       (files path out-dir
              save preprocessor extra-args state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (string-listp files)
                             (stringp path)
                             (or (not out-dir) (stringp out-dir))
                             (stringp preprocessor)
                             (string-listp extra-args))))
 (let ((__function__ 'preprocess-files))
   (declare (ignorable __function__))
   (b* (((reterr) (irr-fileset) state)
        ((when (endp files))
         (retok (fileset nil) state))
        (out (and out-dir
                  (b* ((filename (first files)))
                    (and (stringp filename)
                         (concatenate 'string
                                      out-dir "/" filename ".i")))))
        (filename (concatenate 'string
                               path "/" (first files)))
        ((erp - filedata state)
         (preprocess-file filename
                          :out out
                          :save save
                          :preprocessor preprocessor
                          :extra-args extra-args
                          :state state))
        ((erp (fileset fileset) state)
         (preprocess-files (rest files)
                           :path path
                           :out-dir out-dir
                           :save save
                           :preprocessor preprocessor
                           :extra-args extra-args
                           :state state)))
     (retok (fileset (omap::update (filepath (first files))
                                   filedata fileset.unwrap))
            state))))

Theorem: filesetp-of-preprocess-files.map

(defthm filesetp-of-preprocess-files.map
  (b* (((mv acl2::?erp ?map acl2::?state)
        (preprocess-files-fn files path out-dir
                             save preprocessor extra-args state)))
    (filesetp map))
  :rule-classes :rewrite)