		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-process-endif

Handler for endif directives.

Signature
(vl-process-endif loc echars ppst) → (mv successp ppst)
Arguments: loc — Guard (vl-location-p loc).; echars — Characters that come after the `endif, which are used only for multiple-include optimization.
Guard (vl-echarlist-p echars).
Returns: successp — Type (booleanp successp).

Definitions and Theorems

Function: vl-process-endif

(defun vl-process-endif (loc echars ppst)
 (declare (xargs :stobjs (ppst)))
 (declare (xargs :guard (and (vl-location-p loc)
                             (vl-echarlist-p echars))))
 (let ((__function__ 'vl-process-endif))
  (declare (ignorable __function__))
  (b*
   ((istack (vl-ppst->istack))
    ((when (atom istack))
     (let
       ((ppst (vl-ppst-fatal
                   :msg "~a0: found `endif, but no `ifdef is open."
                   :args (list loc))))
       (mv nil ppst)))
    ((vl-iframe iframe) (car istack))
    (new-istack (cdr istack))
    (new-activep iframe.initially-activep)
    (ppst (vl-ppst-update-istack new-istack))
    (ppst (vl-ppst-update-activep new-activep))
    ((unless iframe.mi-controller)
     (mv t ppst))
    ((unless iframe.mi-filename)
     (raise
      "Programming error: iframe has mi controller but no filename? ~x0"
      iframe)
     (mv t ppst))
    ((unless (equal iframe.mi-filename
                    (vl-location->filename loc)))
     (let
      ((ppst
        (vl-ppst-warn
         :type :vl-warn-include-guard
         :msg
         "~a0: disabling multiple-include optimization ~
                           because the corresponding include guard was found ~
                           in a different file, ~s1.  If this isn't expected, ~
                           there may be a problem with your `ifdef tree."
         :args (list loc iframe.mi-filename))))
      (mv t ppst)))
    (post-ws (vl-skip-whitespace/comments echars))
    ((unless (atom post-ws))
     (let
      ((ppst
        (vl-ppst-warn
         :type :vl-warn-include-guard
         :msg
         "~a0: disabling multiple-include optimization ~
                           because there's content after the `else for ~
                           ~s1."
         :args (list loc iframe.mi-controller))))
      (mv t ppst)))
    (- (cw-unformatted (cat (vl-ppst-pad)
                            " (multi-include confirmed)" *nls*)))
    (iskips (vl-includeskips-install-controller
                 iframe.mi-filename
                 iframe.mi-controller (vl-ppst->iskips)))
    (ppst (vl-ppst-update-iskips iskips)))
   (mv t ppst))))

Theorem: booleanp-of-vl-process-endif.successp

(defthm booleanp-of-vl-process-endif.successp
  (b* (((mv ?successp ?ppst)
        (vl-process-endif loc echars ppst)))
    (booleanp successp))
  :rule-classes :type-prescription)