(vl-add-context-to-parser-warning warning &key (tokstream 'tokstream)) → new-warning
Function:
(defun vl-add-context-to-parser-warning-fn (warning tokstream) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-warning-p warning))) (let ((__function__ 'vl-add-context-to-parser-warning)) (declare (ignorable __function__)) (b* ((tokens (vl-tokstream->tokens)) (context (cat " Near: \"" (vl-tokenlist->string-with-spaces (take (min 4 (len tokens)) (list-fix tokens))) (if (> (len tokens) 4) "..." "") "\"")) (new-msg (cat (vl-warning->msg warning) (str::strsubst "~" "~~" context)))) (change-vl-warning warning :msg new-msg))))
Theorem:
(defthm vl-warning-p-of-vl-add-context-to-parser-warning (b* ((new-warning (vl-add-context-to-parser-warning-fn warning tokstream))) (vl-warning-p new-warning)) :rule-classes :rewrite)