• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
        • Lint-warning-suppression
        • Warning-basics
        • Vl-warning
        • Vl-warninglist-add-ctx
        • Vl-warninglist->types
        • Propagating-errors
          • Vl-design-propagate-errors
          • Vl-blamealist
          • Vl-design-zombies
          • Vl-blame-alist-to-reportcard
          • Vl-blame-alist
            • Vl-blame-alist-aux2
            • Vl-blame-alist-aux1
          • Vl-blamealist-count
        • Vl-reportcard
        • Vl-some-warning-fatalp
        • Clean-warnings
        • Lint-whole-file-suppression
        • Warn
        • Vl-warninglist
        • Vl-remove-warnings
        • Vl-keep-warnings
        • Flat-warnings
        • Vl-some-warning-of-type-p
        • Vl-msg
        • Vl-warning-add-ctx
        • Vl-print-warning
        • Vmsg-binary-concat
        • Ok
        • Vl-trace-warnings
        • Fatal
        • Vmsg
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-blame-alist

Vl-blame-alist-aux1

For each module M in DEPS, additionally blame BAD.

Signature

(vl-blame-alist-aux1 bad deps alist) → new-alist

Arguments

bad — Name of a module we are currently processing.
    Guard (stringp bad).

deps — Modules that (transitively) depend on bad.
    Guard (string-listp deps).

alist — Partially constructed blame list.
    Guard (vl-blamealist-p alist).

Returns

new-alist — Type (vl-blamealist-p new-alist).

Definitions and Theorems

Function: vl-blame-alist-aux1

(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: vl-blamealist-p-of-vl-blame-alist-aux1

(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: vl-blame-alist-aux1-of-str-fix-bad

(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: vl-blame-alist-aux1-streqv-congruence-on-bad

(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: vl-blame-alist-aux1-of-string-list-fix-deps

(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: vl-blame-alist-aux1-string-list-equiv-congruence-on-deps

(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: vl-blame-alist-aux1-of-vl-blamealist-fix-alist

(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: vl-blame-alist-aux1-vl-blamealist-equiv-congruence-on-alist

(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)