		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-vardecl-svbad-warnings

Signature
(vl-vardecl-svbad-warnings x warnings) → warnings
Arguments: x — Guard (vl-vardecl-p x).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-vardecl-svbad-warnings

(defun vl-vardecl-svbad-warnings (x warnings)
 (declare (xargs :guard (and (vl-vardecl-p x)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-vardecl-svbad-warnings))
  (declare (ignorable __function__))
  (b* (((vl-vardecl x))
       ((unless (vl-datatype-svbad-p x.type))
        (ok)))
   (fatal
      :type :vl-warn-svbad-p
      :msg "~a0: type ~a1 looks like it will cause problems for SV."
      :args (list x x.type)))))

Theorem: vl-warninglist-p-of-vl-vardecl-svbad-warnings

(defthm vl-warninglist-p-of-vl-vardecl-svbad-warnings
  (b* ((warnings (vl-vardecl-svbad-warnings x warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)