• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Lexer
        • Vl-loadstate
        • Parser
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-find-file
        • Vl-read-files
        • Extended-characters
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
          • Vl-filter-warnings-by-loc
          • Vl-descriptionlist-inject-warnings
          • Vl-description-inject-warnings
          • Vl-description-add-warnings
          • Vl-warning->loc
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Inject-warnings

Vl-filter-warnings-by-loc

Extract warnings that are between certain bounds.

Signature

(vl-filter-warnings-by-loc min max warnings between beyond) 
  → 
(mv between beyond)

Arguments

min — Guard (vl-location-p min).

max — Guard (vl-location-p max).

warnings — Warnings to filter.
    Guard (vl-warninglist-p warnings).

between — Accumulator for warnings between min/max.
    Guard (vl-warninglist-p between).

beyond — Accumulator for warnings not between min/max.
    Guard (vl-warninglist-p beyond).

Returns

between — Type (vl-warninglist-p between).

beyond — Type (vl-warninglist-p beyond).

Definitions and Theorems

Function: vl-filter-warnings-by-loc

(defun vl-filter-warnings-by-loc (min max warnings between beyond)
  (declare (xargs :guard (and (vl-location-p min)
                              (vl-location-p max)
                              (vl-warninglist-p warnings)
                              (vl-warninglist-p between)
                              (vl-warninglist-p beyond))))
  (let ((__function__ 'vl-filter-warnings-by-loc))
    (declare (ignorable __function__))
    (b* ((warnings (vl-warninglist-fix warnings))
         (between (vl-warninglist-fix between))
         (beyond (vl-warninglist-fix beyond))
         ((when (atom warnings))
          (mv between beyond))
         (warn1 (car warnings))
         (loc1 (vl-warning->loc warn1))
         ((when (and loc1
                     (vl-location-between-p loc1 min max)))
          (vl-filter-warnings-by-loc min max (cdr warnings)
                                     (cons warn1 between)
                                     beyond)))
      (vl-filter-warnings-by-loc min max (cdr warnings)
                                 between (cons warn1 beyond)))))

Theorem: vl-warninglist-p-of-vl-filter-warnings-by-loc.between

(defthm vl-warninglist-p-of-vl-filter-warnings-by-loc.between
 (b* (((mv ?between ?beyond)
       (vl-filter-warnings-by-loc min max warnings between beyond)))
   (vl-warninglist-p between))
 :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-filter-warnings-by-loc.beyond

(defthm vl-warninglist-p-of-vl-filter-warnings-by-loc.beyond
 (b* (((mv ?between ?beyond)
       (vl-filter-warnings-by-loc min max warnings between beyond)))
   (vl-warninglist-p beyond))
 :rule-classes :rewrite)

Theorem: vl-filter-warnings-by-loc-of-vl-location-fix-min

(defthm vl-filter-warnings-by-loc-of-vl-location-fix-min
  (equal
       (vl-filter-warnings-by-loc (vl-location-fix min)
                                  max warnings between beyond)
       (vl-filter-warnings-by-loc min max warnings between beyond)))

Theorem: vl-filter-warnings-by-loc-vl-location-equiv-congruence-on-min

(defthm
      vl-filter-warnings-by-loc-vl-location-equiv-congruence-on-min
 (implies
  (vl-location-equiv min min-equiv)
  (equal (vl-filter-warnings-by-loc min max warnings between beyond)
         (vl-filter-warnings-by-loc
              min-equiv max warnings between beyond)))
 :rule-classes :congruence)

Theorem: vl-filter-warnings-by-loc-of-vl-location-fix-max

(defthm vl-filter-warnings-by-loc-of-vl-location-fix-max
  (equal
       (vl-filter-warnings-by-loc min (vl-location-fix max)
                                  warnings between beyond)
       (vl-filter-warnings-by-loc min max warnings between beyond)))

Theorem: vl-filter-warnings-by-loc-vl-location-equiv-congruence-on-max

(defthm
      vl-filter-warnings-by-loc-vl-location-equiv-congruence-on-max
 (implies
  (vl-location-equiv max max-equiv)
  (equal (vl-filter-warnings-by-loc min max warnings between beyond)
         (vl-filter-warnings-by-loc
              min max-equiv warnings between beyond)))
 :rule-classes :congruence)

Theorem: vl-filter-warnings-by-loc-of-vl-warninglist-fix-warnings

(defthm vl-filter-warnings-by-loc-of-vl-warninglist-fix-warnings
 (equal
    (vl-filter-warnings-by-loc min max (vl-warninglist-fix warnings)
                               between beyond)
    (vl-filter-warnings-by-loc min max warnings between beyond)))

Theorem: vl-filter-warnings-by-loc-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-filter-warnings-by-loc-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal (vl-filter-warnings-by-loc min max warnings between beyond)
         (vl-filter-warnings-by-loc
              min max warnings-equiv between beyond)))
 :rule-classes :congruence)

Theorem: vl-filter-warnings-by-loc-of-vl-warninglist-fix-between

(defthm vl-filter-warnings-by-loc-of-vl-warninglist-fix-between
 (equal
    (vl-filter-warnings-by-loc min max
                               warnings (vl-warninglist-fix between)
                               beyond)
    (vl-filter-warnings-by-loc min max warnings between beyond)))

Theorem: vl-filter-warnings-by-loc-vl-warninglist-equiv-congruence-on-between

(defthm
 vl-filter-warnings-by-loc-vl-warninglist-equiv-congruence-on-between
 (implies
  (vl-warninglist-equiv between between-equiv)
  (equal (vl-filter-warnings-by-loc min max warnings between beyond)
         (vl-filter-warnings-by-loc
              min max warnings between-equiv beyond)))
 :rule-classes :congruence)

Theorem: vl-filter-warnings-by-loc-of-vl-warninglist-fix-beyond

(defthm vl-filter-warnings-by-loc-of-vl-warninglist-fix-beyond
 (equal
     (vl-filter-warnings-by-loc min max warnings
                                between (vl-warninglist-fix beyond))
     (vl-filter-warnings-by-loc min max warnings between beyond)))

Theorem: vl-filter-warnings-by-loc-vl-warninglist-equiv-congruence-on-beyond

(defthm
 vl-filter-warnings-by-loc-vl-warninglist-equiv-congruence-on-beyond
 (implies
  (vl-warninglist-equiv beyond beyond-equiv)
  (equal (vl-filter-warnings-by-loc min max warnings between beyond)
         (vl-filter-warnings-by-loc
              min max warnings between beyond-equiv)))
 :rule-classes :congruence)