		Search-engine friendly clone of the ACL2 documentation.

Parse-udps

Vl-make-udp-with-parse-error

Signature
(vl-make-udp-with-parse-error name minloc maxloc err tokens) → udp
Arguments: name — Guard (stringp name).; minloc — Guard (vl-location-p minloc).; maxloc — Guard (vl-location-p maxloc).; err — Guard (vl-warning-p err).; tokens — Guard (vl-tokenlist-p tokens).
Returns: udp — Type (vl-udp-p udp).

Definitions and Theorems

Function: vl-make-udp-with-parse-error

(defun vl-make-udp-with-parse-error (name minloc maxloc err tokens)
 (declare (xargs :guard (and (stringp name)
                             (vl-location-p minloc)
                             (vl-location-p maxloc)
                             (vl-warning-p err)
                             (vl-tokenlist-p tokens))))
 (let ((__function__ 'vl-make-udp-with-parse-error))
  (declare (ignorable __function__))
  (b*
   ((warn2
     (make-vl-warning
      :type :vl-parse-error
      :msg "[[ Remaining ]]: ~s0 ~s1.~%"
      :args
      (list
        (vl-tokenlist->string-with-spaces (take (min 4 (len tokens))
                                                (list-fix tokens)))
        (if (> (len tokens) 4) "..." ""))
      :fatalp t
      :fn __function__)))
   (make-vl-udp
        :name name
        :output
        (make-vl-portdecl :name "FAKE_PORT_FOR_UDP_WITH_PARSE_ERROR"
                          :dir :vl-output
                          :type *vl-plain-old-logic-type*
                          :loc minloc)
        :minloc minloc
        :maxloc maxloc
        :warnings (list err warn2)))))

Theorem: vl-udp-p-of-vl-make-udp-with-parse-error

(defthm vl-udp-p-of-vl-make-udp-with-parse-error
 (b*
  ((udp
      (vl-make-udp-with-parse-error name minloc maxloc err tokens)))
  (vl-udp-p udp))
 :rule-classes :rewrite)