		Search-engine friendly clone of the ACL2 documentation.

Server

Vl-description->warnings

Get the warnings from most descriptions, or nil if this description doesn't have any warnings (e.g., an import statement, function declaration, ...).

Signature
(vl-description->warnings x) → warnings
Arguments: x — Guard (vl-description-p x).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-description->warnings

(defun vl-description->warnings (x)
  (declare (xargs :guard (vl-description-p x)))
  (let ((__function__ 'vl-description->warnings))
    (declare (ignorable __function__))
    (b* ((x (vl-description-fix x)))
      (case (tag x)
            (:vl-module (vl-module->warnings x))
            (:vl-udp (vl-udp->warnings x))
            (:vl-interface (vl-interface->warnings x))
            (:vl-package (vl-package->warnings x))
            (:vl-program (vl-program->warnings x))
            (:vl-config (vl-config->warnings x))
            (:vl-taskdecl nil)
            (:vl-fundecl nil)
            (:vl-paramdecl nil)
            (:vl-import nil)
            (:vl-fwdtypedef nil)
            (:vl-typedef nil)
            (otherwise (impossible))))))

Theorem: vl-warninglist-p-of-vl-description->warnings

(defthm vl-warninglist-p-of-vl-description->warnings
  (b* ((warnings (vl-description->warnings x)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)