Record that a file is being successfully skipped due to multiple include optimization.
(vl-includeskips-record-hit realfile loc iskips) → new-iskips
Function:
(defun vl-includeskips-record-hit (realfile loc iskips) (declare (xargs :guard (and (stringp realfile) (vl-location-p loc) (vl-includeskips-p iskips)))) (let ((__function__ 'vl-includeskips-record-hit)) (declare (ignorable __function__)) (b* ((realfile (string-fix realfile)) (loc (vl-location-fix loc)) (iskips (vl-includeskips-fix iskips)) (entry (cdr (hons-get realfile iskips))) ((unless entry) (raise "Programming error: skipping include without entry for ~f0???" realfile) iskips) (entry (change-vl-iskipinfo entry :hits (cons loc (vl-iskipinfo->hits entry))))) (hons-acons realfile entry iskips))))
Theorem:
(defthm vl-includeskips-p-of-vl-includeskips-record-hit (b* ((new-iskips (vl-includeskips-record-hit realfile loc iskips))) (vl-includeskips-p new-iskips)) :rule-classes :rewrite)