		Search-engine friendly clone of the ACL2 documentation.

Check-case

Vl-module-check-case

Signature
(vl-module-check-case x) → new-x
Arguments: x — Guard (vl-module-p x).
Returns: new-x — Maybe with new warnings.
Type (vl-module-p new-x), given the guard.

Definitions and Theorems

Function: vl-module-check-case

(defun vl-module-check-case (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-module-check-case))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) x)
    (names (append (vl-portdecllist->names x.portdecls)
                   (vl-module->modnamespace x)))
    (names (cwtime (mergesort names)
                   :name check-case-gather-names
                   :mintime 1/2))
    (equiv-names (cwtime (vl-find-case-equivalent-strings names)
                         :name check-case-find-equiv-strs
                         :mintime 1/2))
    ((unless equiv-names) x)
    (w
     (make-vl-warning
      :type :vl-warn-case-sensitive-names
      :msg
      "In ~a0, found names that differ only by case.  This might ~
                 indicate a typo, and otherwise it might cause problems for ~
                 some Verilog tools.  Details: ~%~s1"
      :args
      (list x.name
            (with-local-ps (vl-equiv-strings-to-lines equiv-names)))
      :fatalp nil
      :fn __function__)))
   (change-vl-module x
                     :warnings (cons w x.warnings)))))

Theorem: vl-module-p-of-vl-module-check-case

(defthm vl-module-p-of-vl-module-check-case
  (implies (and (force (vl-module-p x)))
           (b* ((new-x (vl-module-check-case x)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)