		Search-engine friendly clone of the ACL2 documentation.

Ppst

Vl-ppst-warn

Add a non-fatal warning to the ppst.

Signature
(vl-ppst-warn &key type msg args (fn '__function__) (ppst 'ppst)) → ppst
Arguments: type — Guard (symbolp type).; msg — Guard (stringp msg).; args — Guard (true-listp args).; fn — Guard (symbolp fn).

We don't print anything since it's just a warning.

Definitions and Theorems

Function: vl-ppst-warn-fn

(defun vl-ppst-warn-fn (type msg args fn ppst)
  (declare (xargs :stobjs (ppst)))
  (declare (xargs :guard (and (symbolp type)
                              (stringp msg)
                              (true-listp args)
                              (symbolp fn))))
  (let ((__function__ 'vl-ppst-warn))
    (declare (ignorable __function__))
    (b* ((warnings (vl-ppst->warnings))
         (warnings (warn :type type
                         :msg msg
                         :args args
                         :fn fn)))
      (vl-ppst-update-warnings warnings))))