		Search-engine friendly clone of the ACL2 documentation.

Vl-reportcard

Vl-apply-reportcard

Update a design to include any warnings from a vl-reportcard-p.

Signature
(vl-apply-reportcard x reportcard) → new-x
Arguments: x — Guard (vl-design-p x).; reportcard — Guard (vl-reportcard-p reportcard).
Returns: new-x — Type (vl-design-p new-x).

This is typically the last step in using a reportcard. We change the design x by adding the warnings from throughout the report card to the appropriate design elements. For instance, if there is a module named foo in the design that currently has two warnings, and the report card lists three warnings about foo, then in the new design these warnings will have been merged so that foo will now have 5 warnings.

One subtlety is that the reportcard may mention modules that aren't in the design. This typically shouldn't happen. If it does, these warnings will be associated with the top-level design, instead.

Definitions and Theorems

Function: vl-apply-reportcard

(defun vl-apply-reportcard (x reportcard)
 (declare (xargs :guard (and (vl-design-p x)
                             (vl-reportcard-p reportcard))))
 (let ((__function__ 'vl-apply-reportcard))
  (declare (ignorable __function__))
  (b*
   (((vl-design x) (vl-design-fix x))
    (reportcard (vl-reportcard-fix reportcard))
    ((when (atom reportcard)) x)
    (reportcard (vl-clean-reportcard reportcard))
    (valid-keys (vl-design-reportcard-keys x))
    (valid-fal (make-lookup-alist valid-keys))
    (revived
       (vl-reportcard-revive-invalid-warnings reportcard valid-fal))
    (- (fast-alist-free valid-fal))
    (new-toplevel
         (append-without-guard (cdr (hons-get :design reportcard))
                               revived x.warnings))
    (new-x
     (change-vl-design
      x
      :mods (vl-modulelist-apply-reportcard x.mods reportcard)
      :udps (vl-udplist-apply-reportcard x.udps reportcard)
      :interfaces
      (vl-interfacelist-apply-reportcard x.interfaces reportcard)
      :programs
      (vl-programlist-apply-reportcard x.programs reportcard)
      :classes (vl-classlist-apply-reportcard x.classes reportcard)
      :packages
      (vl-packagelist-apply-reportcard x.packages reportcard)
      :configs (vl-configlist-apply-reportcard x.configs reportcard)
      :typedefs
      (vl-typedeflist-apply-reportcard x.typedefs reportcard)
      :warnings new-toplevel))
    (- (fast-alist-free reportcard)))
   new-x)))

Theorem: vl-design-p-of-vl-apply-reportcard

(defthm vl-design-p-of-vl-apply-reportcard
  (b* ((new-x (vl-apply-reportcard x reportcard)))
    (vl-design-p new-x))
  :rule-classes :rewrite)

Theorem: vl-apply-reportcard-of-vl-design-fix-x

(defthm vl-apply-reportcard-of-vl-design-fix-x
  (equal (vl-apply-reportcard (vl-design-fix x)
                              reportcard)
         (vl-apply-reportcard x reportcard)))

Theorem: vl-apply-reportcard-vl-design-equiv-congruence-on-x

(defthm vl-apply-reportcard-vl-design-equiv-congruence-on-x
  (implies (vl-design-equiv x x-equiv)
           (equal (vl-apply-reportcard x reportcard)
                  (vl-apply-reportcard x-equiv reportcard)))
  :rule-classes :congruence)

Theorem: vl-apply-reportcard-of-vl-reportcard-fix-reportcard

(defthm vl-apply-reportcard-of-vl-reportcard-fix-reportcard
  (equal (vl-apply-reportcard x (vl-reportcard-fix reportcard))
         (vl-apply-reportcard x reportcard)))

Theorem: vl-apply-reportcard-vl-reportcard-equiv-congruence-on-reportcard

(defthm
   vl-apply-reportcard-vl-reportcard-equiv-congruence-on-reportcard
  (implies (vl-reportcard-equiv reportcard reportcard-equiv)
           (equal (vl-apply-reportcard x reportcard)
                  (vl-apply-reportcard x reportcard-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-udplist-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-udplist-p.
Vl-typedeflist-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-typedeflist-p.
Vl-programlist-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-programlist-p.
Vl-packagelist-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-packagelist-p.
Vl-modulelist-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-modulelist-p.
Vl-interfacelist-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-interfacelist-p.
Vl-configlist-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-configlist-p.
Vl-classlist-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-classlist-p.
Vl-interface-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-interface-p.
Vl-typedef-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-typedef-p.
Vl-program-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-program-p.
Vl-package-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-package-p.
Vl-module-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-module-p.
Vl-config-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-config-p.
Vl-class-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-class-p.
Vl-udp-apply-reportcard: Add any warnings from a vl-reportcard-p to a vl-udp-p.
Vl-design-reportcard-keys: Gather a list of all valid vl-reportcard keys for a design.