(vl-make-udp-with-parse-error name minloc maxloc err tokens) → udp
Function:
(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-wire-type* :loc minloc) :minloc minloc :maxloc maxloc :warnings (list err warn2)))))
Theorem:
(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)