For each module M in DEPS, additionally blame BAD.
(vl-blame-alist-aux1 bad deps alist) → new-alist
Function:
(defun vl-blame-alist-aux1 (bad deps alist) (declare (xargs :guard (and (stringp bad) (string-listp deps) (vl-blamealist-p alist)))) (let ((__function__ 'vl-blame-alist-aux1)) (declare (ignorable __function__)) (b* ((bad (string-fix bad)) (deps (string-list-fix deps)) (alist (vl-blamealist-fix alist)) ((when (atom deps)) alist) (m (car deps)) (old-blamed (cdr (hons-get m alist))) (new-blamed (cons bad old-blamed)) (new-alist (hons-acons m new-blamed alist))) (vl-blame-alist-aux1 bad (cdr deps) new-alist))))
Theorem:
(defthm vl-blamealist-p-of-vl-blame-alist-aux1 (b* ((new-alist (vl-blame-alist-aux1 bad deps alist))) (vl-blamealist-p new-alist)) :rule-classes :rewrite)
Theorem:
(defthm vl-blame-alist-aux1-of-str-fix-bad (equal (vl-blame-alist-aux1 (str-fix bad) deps alist) (vl-blame-alist-aux1 bad deps alist)))
Theorem:
(defthm vl-blame-alist-aux1-streqv-congruence-on-bad (implies (streqv bad bad-equiv) (equal (vl-blame-alist-aux1 bad deps alist) (vl-blame-alist-aux1 bad-equiv deps alist))) :rule-classes :congruence)
Theorem:
(defthm vl-blame-alist-aux1-of-string-list-fix-deps (equal (vl-blame-alist-aux1 bad (string-list-fix deps) alist) (vl-blame-alist-aux1 bad deps alist)))
Theorem:
(defthm vl-blame-alist-aux1-string-list-equiv-congruence-on-deps (implies (str::string-list-equiv deps deps-equiv) (equal (vl-blame-alist-aux1 bad deps alist) (vl-blame-alist-aux1 bad deps-equiv alist))) :rule-classes :congruence)
Theorem:
(defthm vl-blame-alist-aux1-of-vl-blamealist-fix-alist (equal (vl-blame-alist-aux1 bad deps (vl-blamealist-fix alist)) (vl-blame-alist-aux1 bad deps alist)))
Theorem:
(defthm vl-blame-alist-aux1-vl-blamealist-equiv-congruence-on-alist (implies (vl-blamealist-equiv alist alist-equiv) (equal (vl-blame-alist-aux1 bad deps alist) (vl-blame-alist-aux1 bad deps alist-equiv))) :rule-classes :congruence)