		Search-engine friendly clone of the ACL2 documentation.

Translate-off

Vl-commentmap-translate-off-warnings

Signature
(vl-commentmap-translate-off-warnings x warnings) → warnings
Arguments: x — Guard (vl-commentmap-p x).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-commentmap-translate-off-warnings

(defun vl-commentmap-translate-off-warnings (x warnings)
 (declare (xargs :guard (and (vl-commentmap-p x)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-commentmap-translate-off-warnings))
  (declare (ignorable __function__))
  (b*
   ((x (vl-commentmap-fix x))
    ((when (atom x)) (ok))
    ((cons loc comment) (car x))
    (warnings
     (if
      (vl-scary-translate-comment-p comment)
      (warn
       :type :vl-warn-scary-translate-comment
       :msg
       "~a0: ignoring a comment that may be a ~
                                  translate_on or translate_off directive.  ~
                                  Using a preprocessor directive like `ifdef ~
                                  ASSERT_ON is preferred.  Comment: ~s1"
       :args (list loc comment))
      (ok))))
   (vl-commentmap-translate-off-warnings (cdr x)
                                         warnings))))

Theorem: vl-warninglist-p-of-vl-commentmap-translate-off-warnings

(defthm vl-warninglist-p-of-vl-commentmap-translate-off-warnings
  (b* ((warnings (vl-commentmap-translate-off-warnings x warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)