		Search-engine friendly clone of the ACL2 documentation.

Elimalways

Vl-warn-about-bad-always-blocks

Signature
(vl-warn-about-bad-always-blocks x warnings) → warnings
Arguments: x — Guard (vl-alwayslist-p x).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-warn-about-bad-always-blocks

(defun vl-warn-about-bad-always-blocks (x warnings)
  (declare (xargs :guard (and (vl-alwayslist-p x)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-warn-about-bad-always-blocks))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (ok))
         (always1 (vl-always-fix (car x)))
         (warnings (fatal :type :vl-bad-always
                          :msg "~a0: always block is not supported."
                          :args (list always1))))
      (vl-warn-about-bad-always-blocks (cdr x)
                                       warnings))))

Theorem: vl-warninglist-p-of-vl-warn-about-bad-always-blocks

(defthm vl-warninglist-p-of-vl-warn-about-bad-always-blocks
  (b* ((warnings (vl-warn-about-bad-always-blocks x warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-warn-about-bad-always-blocks-of-vl-alwayslist-fix-x

(defthm vl-warn-about-bad-always-blocks-of-vl-alwayslist-fix-x
  (equal (vl-warn-about-bad-always-blocks (vl-alwayslist-fix x)
                                          warnings)
         (vl-warn-about-bad-always-blocks x warnings)))

Theorem: vl-warn-about-bad-always-blocks-vl-alwayslist-equiv-congruence-on-x

(defthm
 vl-warn-about-bad-always-blocks-vl-alwayslist-equiv-congruence-on-x
 (implies
      (vl-alwayslist-equiv x x-equiv)
      (equal (vl-warn-about-bad-always-blocks x warnings)
             (vl-warn-about-bad-always-blocks x-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-warn-about-bad-always-blocks-of-vl-warninglist-fix-warnings

(defthm
     vl-warn-about-bad-always-blocks-of-vl-warninglist-fix-warnings
 (equal
   (vl-warn-about-bad-always-blocks x (vl-warninglist-fix warnings))
   (vl-warn-about-bad-always-blocks x warnings)))

Theorem: vl-warn-about-bad-always-blocks-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-warn-about-bad-always-blocks-vl-warninglist-equiv-congruence-on-warnings
 (implies
      (vl-warninglist-equiv warnings warnings-equiv)
      (equal (vl-warn-about-bad-always-blocks x warnings)
             (vl-warn-about-bad-always-blocks x warnings-equiv)))
 :rule-classes :congruence)