Record that a file is not being skipped due to multiple include optimization.
(vl-includeskips-record-miss realfile loc len iskips) → new-iskips
Function:
(defun vl-includeskips-record-miss (realfile loc len iskips) (declare (xargs :guard (and (stringp realfile) (vl-location-p loc) (natp len) (vl-includeskips-p iskips)))) (let ((__function__ 'vl-includeskips-record-miss)) (declare (ignorable __function__)) (b* ((realfile (string-fix realfile)) (loc (vl-location-fix loc)) (iskips (vl-includeskips-fix iskips)) (entry (or (cdr (hons-get realfile iskips)) (make-vl-iskipinfo :controller nil :misses nil :hits nil :len len))) (entry (change-vl-iskipinfo entry :misses (cons loc (vl-iskipinfo->misses entry))))) (hons-acons realfile entry iskips))))
Theorem:
(defthm vl-includeskips-p-of-vl-includeskips-record-miss (b* ((new-iskips (vl-includeskips-record-miss realfile loc len iskips))) (vl-includeskips-p new-iskips)) :rule-classes :rewrite)