		Search-engine friendly clone of the ACL2 documentation.

Problem-modules

Vl-warn-problem-module

Add a fatal warning if this is a problem module.

Signature
(vl-warn-problem-module x problems) → new-x
Arguments: x — A module, perhaps a problem module.
Guard (vl-module-p x).; problems — A list of problem module names, supplied by the user.
Guard (string-listp problems).
Returns: new-x — Type (vl-module-p new-x), given (force (vl-module-p x)).

Definitions and Theorems

Function: vl-warn-problem-module

(defun
 vl-warn-problem-module (x problems)
 (declare (xargs :guard (and (vl-module-p x)
                             (string-listp problems))))
 (let
  ((__function__ 'vl-warn-problem-module))
  (declare (ignorable __function__))
  (b*
   (((unless (member-equal (vl-module->name x)
                           problems))
     x)
    (warnings (vl-module->warnings x))
    (warnings
     (fatal
         :type :vl-problem-module
         :msg "~m0 was listed as a \"problem module\" by the VL user."
         :args (list (vl-module->name x)))))
   (change-vl-module x
                     :warnings warnings))))

Theorem: vl-module-p-of-vl-warn-problem-module

(defthm vl-module-p-of-vl-warn-problem-module
        (implies (force (vl-module-p x))
                 (b* ((new-x (vl-warn-problem-module x problems)))
                     (vl-module-p new-x)))
        :rule-classes :rewrite)