A convenient shorthand for calling vl-warninglist-fix.
This is often useful as a base case in functions that sometimes create warnings. The name of the warnings accumulator to fix can also be specified, e.g.,:
(ok acc) == (vl-warninglist-fix acc)
(defthm ok-correct (and (equal (ok x) (vl-warninglist-fix x)) (equal (ok) (vl-warninglist-fix warnings))) :rule-classes nil)