		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Preprocess

Preprocess a file set [C17:5.1.1.2/4].

Signature
(preprocess fileset) → tunit
Arguments: fileset — Guard (filesetp fileset).
Returns: tunit — Type (transunit-resultp tunit).

This is a very simplified model of C preprocessing [C17:6.10]. If there is no header, this is essentially a no-op: the external declarations are unwrapped from the source file and re-wrapped into a translation unit. If there is a header, as explained in fileset, it is implicitly included in the source file (without an explicit representation of the #include directive): we concatenate the external declarations from the header and the external declarations from the source file, and wrap the concatenation into a translation unit. This amounts to replacing the (implicit) #include with the included header, which is assumed to be at the beginning of the source file. The path without extension component of the file set is currently ignored, because the #include is implicit.

Definitions and Theorems

Function: preprocess

(defun preprocess (fileset)
  (declare (xargs :guard (filesetp fileset)))
  (let ((__function__ 'preprocess))
    (declare (ignorable __function__))
    (b* ((h-extdecls (and (fileset->dot-h fileset)
                          (file->declons (fileset->dot-h fileset))))
         (c-extdecls (file->declons (fileset->dot-c fileset))))
      (make-transunit :declons (append h-extdecls c-extdecls)))))

Theorem: transunit-resultp-of-preprocess

(defthm transunit-resultp-of-preprocess
  (b* ((tunit (preprocess fileset)))
    (transunit-resultp tunit))
  :rule-classes :rewrite)

Theorem: preprocess-of-fileset-fix-fileset

(defthm preprocess-of-fileset-fix-fileset
  (equal (preprocess (fileset-fix fileset))
         (preprocess fileset)))

Theorem: preprocess-fileset-equiv-congruence-on-fileset

(defthm preprocess-fileset-equiv-congruence-on-fileset
  (implies (fileset-equiv fileset fileset-equiv)
           (equal (preprocess fileset)
                  (preprocess fileset-equiv)))
  :rule-classes :congruence)