Special error recovery for parse errors encountered during primitives.
(vl-skip-through-endprimitive udpname &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Function:
(defun vl-skip-through-endprimitive-fn (udpname tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (declare (xargs :guard (stringp udpname))) (let ((__function__ 'vl-skip-through-endprimitive)) (declare (ignorable __function__)) (seq tokstream (unless (vl-is-token? :vl-kwd-endprimitive) (:s= (vl-match-any)) (endkwd := (vl-skip-through-endprimitive udpname)) (return endkwd)) (endkwd := (vl-match)) (:= (vl-parse-endblock-name udpname "primitive/endprimitive")) (return endkwd))))
Theorem:
(defthm vl-skip-through-endprimitive-fails-gracefully (implies (mv-nth 0 (vl-skip-through-endprimitive udpname)) (not (mv-nth 1 (vl-skip-through-endprimitive udpname)))))
Theorem:
(defthm vl-warning-p-of-vl-skip-through-endprimitive (iff (vl-warning-p (mv-nth 0 (vl-skip-through-endprimitive udpname))) (mv-nth 0 (vl-skip-through-endprimitive udpname))))
Theorem:
(defthm vl-skip-through-endprimitive-result (implies (and (force (stringp udpname))) (equal (vl-token-p (mv-nth 1 (vl-skip-through-endprimitive udpname))) (not (mv-nth 0 (vl-skip-through-endprimitive udpname))))))
Theorem:
(defthm vl-skip-through-endprimitive-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-skip-through-endprimitive udpname))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-skip-through-endprimitive udpname))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-skip-through-endprimitive udpname))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))