• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
          • Vl-warninglist->types
          • Vl-warning
          • Propagating-errors
          • Vl-reportcard
          • Vl-warning-sort
            • Vl-warning-<
            • Lint-warning-suppression
            • Clean-warnings
            • Warn
            • Vl-print-warnings-with-header
            • Vl-some-warning-fatalp
            • Vl-print-warnings-with-named-header
            • Flat-warnings
            • Vl-remove-warnings
            • Vl-keep-warnings
            • Vl-print-warnings
            • Vl-some-warning-of-type-p
            • Vl-clean-warnings
            • Vl-warnings-to-string
            • Vl-warninglist
            • Vl-print-warning
            • Ok
            • Vl-trace-warnings
            • Fatal
          • Primitives
          • Use-set
          • Syntax
          • Getting-started
          • Utilities
          • Loader
          • Transforms
          • Lint
          • Mlib
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-warning-sort

    Vl-warning-<

    A basic, rather arbitrary ordering for warnings.

    Signature
    (vl-warning-< x y) → *
    Arguments
    x — Guard (vl-warning-p x).
    y — Guard (vl-warning-p y).

    Definitions and Theorems

    Function: vl-warning-<

    (defun vl-warning-< (x y)
      (declare (xargs :guard (and (vl-warning-p x)
                                  (vl-warning-p y))))
      (let ((__function__ 'vl-warning-<))
        (declare (ignorable __function__))
        (b* (((vl-warning x) x)
             ((vl-warning y) y)
             ((when (symbol< x.type y.type)) t)
             ((unless (eq x.type y.type)) nil)
             ((when (<< x.fn y.fn)) t)
             ((unless (eq x.fn y.fn)) nil)
             ((when (string< x.msg y.msg)) t)
             ((unless (equal x.msg y.msg)) nil)
             ((when (<< x.args y.args)) t)
             ((unless (equal x.args y.args)) nil))
          (<< x.fatalp y.fatalp))))

    Theorem: vl-warning-<-transitive

    (defthm vl-warning-<-transitive
      (implies (and (vl-warning-< x y)
                    (vl-warning-< y z))
               (vl-warning-< x z)))

    Theorem: vl-warning-<-of-vl-warning-fix-x

    (defthm vl-warning-<-of-vl-warning-fix-x
      (equal (vl-warning-< (vl-warning-fix x) y)
             (vl-warning-< x y)))

    Theorem: vl-warning-<-vl-warning-equiv-congruence-on-x

    (defthm vl-warning-<-vl-warning-equiv-congruence-on-x
      (implies (vl-warning-equiv x x-equiv)
               (equal (vl-warning-< x y)
                      (vl-warning-< x-equiv y)))
      :rule-classes :congruence)

    Theorem: vl-warning-<-of-vl-warning-fix-y

    (defthm vl-warning-<-of-vl-warning-fix-y
      (equal (vl-warning-< x (vl-warning-fix y))
             (vl-warning-< x y)))

    Theorem: vl-warning-<-vl-warning-equiv-congruence-on-y

    (defthm vl-warning-<-vl-warning-equiv-congruence-on-y
      (implies (vl-warning-equiv y y-equiv)
               (equal (vl-warning-< x y)
                      (vl-warning-< x y-equiv)))
      :rule-classes :congruence)