		Search-engine friendly clone of the ACL2 documentation.

Ppst

Vl-ppst-fatal

Add a fatal warning to the ppst.

Signature
(vl-ppst-fatal &key (type ':vl-preprocessor-error) 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 also print the warning since this is a fatal error, and the user may be interested in seeing it sooner rather than later.

Definitions and Theorems

Function: vl-ppst-fatal-fn

(defun vl-ppst-fatal-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-fatal))
   (declare (ignorable __function__))
   (b*
     ((w (make-vl-warning :type type
                          :fatalp t
                          :msg msg
                          :args args
                          :fn fn))
      (warnings (vl-ppst->warnings))
      (ppst (vl-ppst-update-warnings (cons w warnings)))
      (wstr (with-local-ps (vl-print-warning w)))
      (padded (str::prefix-lines wstr (cat (vl-ppst-pad) " *** "))))
     (cw-unformatted padded)
     ppst)))