		Search-engine friendly clone of the ACL2 documentation.

Nameclash

Vl-scope-nameclash-warnings

Top level function for checking a scope for name clashes.

Signature
(vl-scope-nameclash-warnings x design warnings) → warnings
Arguments: x — Guard (vl-scope-p x).; design — Guard (vl-design-p design).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-scope-nameclash-warnings

(defun vl-scope-nameclash-warnings (x design warnings)
 (declare (xargs :guard (and (vl-scope-p x)
                             (vl-design-p design)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-scope-nameclash-warnings))
  (declare (ignorable __function__))
  (b*
   ((x (vl-scope-fix x))
    (design (vl-design-fix design))
    ((vl-scopeinfo info)
     (vl-scope->scopeinfo-aux x design))
    (tricky-generate-stuff (vl-genelementlist->nameclash-scopeitem-alist
                                (vl-scope->raw-generates x)
                                nil))
    (locals (append tricky-generate-stuff info.locals))
    (locally-declared-names (alist-keys locals))
    (directly-imported-names
     (alist-keys
        (mergesort
             (vl-strip-locs-from-importresult-alist info.imports))))
    (dupes (duplicated-members (append locally-declared-names
                                       directly-imported-names)))
    ((unless dupes) (ok)))
   (vl-make-nameclash-warnings
        (vl-scope->id x)
        dupes locals info.imports warnings))))

Theorem: vl-warninglist-p-of-vl-scope-nameclash-warnings

(defthm vl-warninglist-p-of-vl-scope-nameclash-warnings
  (b* ((warnings (vl-scope-nameclash-warnings x design warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-scope-nameclash-warnings-of-vl-scope-fix-x

(defthm vl-scope-nameclash-warnings-of-vl-scope-fix-x
  (equal (vl-scope-nameclash-warnings (vl-scope-fix x)
                                      design warnings)
         (vl-scope-nameclash-warnings x design warnings)))

Theorem: vl-scope-nameclash-warnings-vl-scope-equiv-congruence-on-x

(defthm vl-scope-nameclash-warnings-vl-scope-equiv-congruence-on-x
 (implies
      (vl-scope-equiv x x-equiv)
      (equal (vl-scope-nameclash-warnings x design warnings)
             (vl-scope-nameclash-warnings x-equiv design warnings)))
 :rule-classes :congruence)

Theorem: vl-scope-nameclash-warnings-of-vl-design-fix-design

(defthm vl-scope-nameclash-warnings-of-vl-design-fix-design
  (equal (vl-scope-nameclash-warnings x (vl-design-fix design)
                                      warnings)
         (vl-scope-nameclash-warnings x design warnings)))

Theorem: vl-scope-nameclash-warnings-vl-design-equiv-congruence-on-design

(defthm
   vl-scope-nameclash-warnings-vl-design-equiv-congruence-on-design
 (implies
      (vl-design-equiv design design-equiv)
      (equal (vl-scope-nameclash-warnings x design warnings)
             (vl-scope-nameclash-warnings x design-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-scope-nameclash-warnings-of-vl-warninglist-fix-warnings

(defthm vl-scope-nameclash-warnings-of-vl-warninglist-fix-warnings
  (equal (vl-scope-nameclash-warnings
              x design (vl-warninglist-fix warnings))
         (vl-scope-nameclash-warnings x design warnings)))

Theorem: vl-scope-nameclash-warnings-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-scope-nameclash-warnings-vl-warninglist-equiv-congruence-on-warnings
 (implies
      (vl-warninglist-equiv warnings warnings-equiv)
      (equal (vl-scope-nameclash-warnings x design warnings)
             (vl-scope-nameclash-warnings x design warnings-equiv)))
 :rule-classes :congruence)

Subtopics

Generate-block-nameclash-items: Special detection of name clashes involving generate block names.