		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 '"gcc") (extra-args 'nil) (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 "gcc". Other reasonable values might be "clang", "cpp", "cc", etc.
Guard (stringp preprocessor).; extra-args — Arguments to pass to the C preprocessor, in addition to "-E". This may be either a string list, representing the list of preprocessing arguments provided for every file, or an omap from strings to string lists, associating a list of preprocessing arguments to each file independently. When the argument is an omap, file names from the files argument are looked up directly in the omap. No sort of path equivalence is considered (e.g., "./foo.c" is not the same as "foo.c"). When an omap is provided, any file without an association under the map is interpreted as if it is associated with an empty list. A value of nil has the same interpretation as both a list and map, and so may be considered either. The default value is nil.
Guard (or (string-listp extra-args) (acl2::string-stringlist-mapp 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)
                   (or (string-listp extra-args)
                       (acl2::string-stringlist-mapp 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 (first files))
    (full-filename (concatenate 'string path "/" filename))
    (extra-args-is-mapp (and (consp extra-args)
                             (consp (first extra-args))))
    (preprocessor-args
      (if extra-args-is-mapp (cdr (omap::assoc filename extra-args))
        extra-args))
    ((erp - filedata state)
     (preprocess-file full-filename
                      :out out
                      :save save
                      :preprocessor preprocessor
                      :extra-args preprocessor-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)