		Search-engine friendly clone of the ACL2 documentation.

Server

Vls-get-warnings

Signature
(vls-get-warnings origname data) → ans
Arguments: origname — Guard (stringp origname).; data — Guard (vls-data-p data).
Returns: ans — Type (stringp ans).

Definitions and Theorems

Function: vls-get-warnings

(defun vls-get-warnings (origname data)
  (declare (xargs :guard (and (stringp origname)
                              (vls-data-p data))))
  (let ((__function__ 'vls-get-warnings))
    (declare (ignorable __function__))
    (b* (((vls-data data))
         (look (hons-assoc-equal origname data.orig-descalist))
         ((unless look)
          (vls-fail "No such description: ~s0~%" origname))
         (reportcard (vls-data-origname-reportcard data))
         (warnings (cdr (hons-assoc-equal origname reportcard)))
         (json (with-local-ps (vl-jp-warninglist warnings))))
      (vls-success :json json))))

Theorem: stringp-of-vls-get-warnings

(defthm stringp-of-vls-get-warnings
  (b* ((ans (vls-get-warnings origname data)))
    (stringp ans))
  :rule-classes :type-prescription)