		Search-engine friendly clone of the ACL2 documentation.

Vl-includeskips

Vl-multiple-include-begin

Check a file for a proper include-guard header; if so, install a special iframe and skip past the initial ifndef part, otherwise leave the file alone.

Signature
(vl-multiple-include-begin realfile contents ppst) → (mv new-contents ppst)
Arguments: realfile — File name being loaded.
Guard (stringp realfile).; contents — Contents of that file.
Guard (vl-echarlist-p contents).
Returns: new-contents — On failure, the unmodified contents. On success, the remainder of the file just past the include guard.
Type (vl-echarlist-p new-contents).; ppst — Possibly updated with a special iframe for the include guard.

Definitions and Theorems

Function: vl-multiple-include-begin

(defun vl-multiple-include-begin (realfile contents ppst)
 (declare (xargs :stobjs (ppst)))
 (declare (xargs :guard (and (stringp realfile)
                             (vl-echarlist-p contents))))
 (let ((__function__ 'vl-multiple-include-begin))
  (declare (ignorable __function__))
  (b*
   ((contents (vl-echarlist-fix contents))
    ((mv controller1 controller1-loc post-ifndef)
     (vl-match-proper-header-file-start-1 contents))
    ((mv controller2 controller2-loc post-else)
     (if controller1 (mv nil nil nil)
       (vl-match-proper-header-file-start-2 contents)))
    (controller (or controller1 controller2))
    (resume-point (if controller1 post-ifndef post-else))
    (controller-loc (if controller1 controller1-loc
                      controller2-loc))
    ((unless controller)
     (let
      ((ppst
        (vl-ppst-warn
         :type :vl-warn-include-guard
         :msg
         "~s0: included file has no include-guard.  (This is ~
                           fine but may reduce performance if the file is ~
                           included multiple times.)"
         :args (list realfile))))
      (mv contents ppst)))
    (prev-def (vl-find-define controller (vl-ppst->defines)))
    ((when prev-def)
     (let
      ((ppst
        (vl-ppst-warn
         :type :vl-warn-include-guard
         :msg
         "~s0: potential include guard controller, ~s1, is ~
                           already defined when reading the file; previous ~
                           definition from ~a2.  This is unusual and will ~
                           defeat multiple-include optimization for this file."
         :args (list realfile
                     controller (vl-define->loc prev-def)))))
      (mv contents ppst)))
    (- (cw-unformatted (cat (vl-ppst-pad)
                            " (multi-include candidate)" *nls*)))
    (iframe (make-vl-iframe :initially-activep t
                            :some-thing-satisfiedp t
                            :already-saw-elsep (not controller1)
                            :mi-controller controller
                            :mi-filename realfile))
    (ppst (vl-ppst-record-ifdef-use
               controller
               (make-vl-ifdef-context :loc controller-loc)))
    (istack (vl-ppst->istack))
    (ppst (vl-ppst-update-istack (cons iframe istack))))
   (mv resume-point ppst))))

Theorem: vl-echarlist-p-of-vl-multiple-include-begin.new-contents

(defthm vl-echarlist-p-of-vl-multiple-include-begin.new-contents
  (b* (((mv ?new-contents ?ppst)
        (vl-multiple-include-begin realfile contents ppst)))
    (vl-echarlist-p new-contents))
  :rule-classes :rewrite)