(vl-parse-for-initialization &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Function:
(defun vl-parse-for-initialization-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-for-initialization)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-semi) (return '(nil))) (return-raw (b* ((backup (vl-tokstream-save)) ((mv erp1 vardecls tokstream) (vl-parse-1+-for-variable-declarations)) ((unless erp1) (mv nil (cons vardecls nil) tokstream)) (tokstream (vl-tokstream-restore backup)) ((mv erp2 assigns tokstream) (vl-parse-1+-for-init-assignments)) ((unless erp2) (mv nil (cons nil assigns) tokstream)) (tokstream (vl-tokstream-restore backup))) (vl-parse-error "Failed to parse for loop initialization as either declarations or assignments."))))))
Theorem:
(defthm vl-parse-for-initialization-fails-gracefully (implies (mv-nth 0 (vl-parse-for-initialization)) (not (mv-nth 1 (vl-parse-for-initialization)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-for-initialization (iff (vl-warning-p (mv-nth 0 (vl-parse-for-initialization))) (mv-nth 0 (vl-parse-for-initialization))))
Theorem:
(defthm vl-parse-for-initialization-result (implies (and (not (mv-nth 0 (vl-parse-for-initialization))) (and t)) (and (consp (mv-nth 1 (vl-parse-for-initialization))) (vl-vardecllist-p (car (mv-nth 1 (vl-parse-for-initialization)))) (vl-stmtlist-p (cdr (mv-nth 1 (vl-parse-for-initialization)))))))
Theorem:
(defthm vl-parse-for-initialization-count-weak (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-for-initialization))) (vl-tokstream-measure)) :rule-classes ((:rewrite) (:linear)))