• 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
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
          • Vl-remove-unnecessary-elements
          • Vl-necessary-elements-transitive
          • Vl-dependent-elements-transitive
          • Vl-necessary-elements-direct
          • Vl-modulelist-everinstanced
          • Vl-dependent-elements-direct
          • Vl-modulelist-toplevel
          • Vl-design-deporder-modules
          • Vl-design-check-complete
          • Vl-design-upgraph
          • Immdeps
            • Immdeps-main
            • Vl-immdeps
              • Vl-immdeps-p
              • Vl-immdeps-add-error
              • Vl-immdeps-add-item
              • Vl-immdeps-add-definition
              • Vl-immdeps-add-pkgdep
              • Vl-immdeps-fix
              • Vl-immdeps-add-raw-dependency
              • Vl-immdeps-equiv
              • Make-vl-immdeps
              • Vl-immdeps->warnings
              • Vl-immdeps->deps
              • Vl-immdeps->all-okp
              • Change-vl-immdeps
            • Immdeps-top
            • Vl-immdepgraph
            • Vl-depgraph
          • Vl-design-downgraph
          • Vl-collect-dependencies
          • Vl-hierarchy-free
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-immdeps

Vl-immdeps-add-error

Note that there is an error with the dependencies we're collecting.

Signature

(vl-immdeps-add-error ans &key 
                      type msg args fatalp (fn '__function__)) 
 
  → 
new-ans

Arguments

ans — Guard (vl-immdeps-p ans).

type — Guard (symbolp type).

msg — Guard (stringp msg).

args — Guard (true-listp args).

fatalp — Guard (booleanp fatalp).

fn — Guard (symbolp fn).

Returns

new-ans — Type (vl-immdeps-p new-ans).

Definitions and Theorems

Function: vl-immdeps-add-error-fn

(defun vl-immdeps-add-error-fn (ans type msg args fatalp fn)
  (declare (xargs :guard (and (vl-immdeps-p ans)
                              (symbolp type)
                              (stringp msg)
                              (true-listp args)
                              (booleanp fatalp)
                              (symbolp fn))))
  (let ((__function__ 'vl-immdeps-add-error))
    (declare (ignorable __function__))
    (b* ((w (make-vl-warning :type type
                             :msg msg
                             :args args
                             :fn fn
                             :fatalp fatalp)))
      (change-vl-immdeps
           ans
           :all-okp nil
           :warnings (cons w (vl-immdeps->warnings ans))))))

Theorem: vl-immdeps-p-of-vl-immdeps-add-error

(defthm vl-immdeps-p-of-vl-immdeps-add-error
  (b*
   ((new-ans (vl-immdeps-add-error-fn ans type msg args fatalp fn)))
   (vl-immdeps-p new-ans))
  :rule-classes :rewrite)

Theorem: vl-immdeps-add-error-fn-of-vl-immdeps-fix-ans

(defthm vl-immdeps-add-error-fn-of-vl-immdeps-fix-ans
  (equal (vl-immdeps-add-error-fn (vl-immdeps-fix ans)
                                  type msg args fatalp fn)
         (vl-immdeps-add-error-fn ans type msg args fatalp fn)))

Theorem: vl-immdeps-add-error-fn-vl-immdeps-equiv-congruence-on-ans

(defthm vl-immdeps-add-error-fn-vl-immdeps-equiv-congruence-on-ans
 (implies
  (vl-immdeps-equiv ans ans-equiv)
  (equal
       (vl-immdeps-add-error-fn ans type msg args fatalp fn)
       (vl-immdeps-add-error-fn ans-equiv type msg args fatalp fn)))
 :rule-classes :congruence)

Theorem: vl-immdeps-add-error-fn-of-symbol-fix-type

(defthm vl-immdeps-add-error-fn-of-symbol-fix-type
  (equal (vl-immdeps-add-error-fn ans (acl2::symbol-fix type)
                                  msg args fatalp fn)
         (vl-immdeps-add-error-fn ans type msg args fatalp fn)))

Theorem: vl-immdeps-add-error-fn-symbol-equiv-congruence-on-type

(defthm vl-immdeps-add-error-fn-symbol-equiv-congruence-on-type
 (implies
  (acl2::symbol-equiv type type-equiv)
  (equal
       (vl-immdeps-add-error-fn ans type msg args fatalp fn)
       (vl-immdeps-add-error-fn ans type-equiv msg args fatalp fn)))
 :rule-classes :congruence)

Theorem: vl-immdeps-add-error-fn-of-str-fix-msg

(defthm vl-immdeps-add-error-fn-of-str-fix-msg
  (equal (vl-immdeps-add-error-fn ans type (str-fix msg)
                                  args fatalp fn)
         (vl-immdeps-add-error-fn ans type msg args fatalp fn)))

Theorem: vl-immdeps-add-error-fn-streqv-congruence-on-msg

(defthm vl-immdeps-add-error-fn-streqv-congruence-on-msg
 (implies
  (streqv msg msg-equiv)
  (equal
       (vl-immdeps-add-error-fn ans type msg args fatalp fn)
       (vl-immdeps-add-error-fn ans type msg-equiv args fatalp fn)))
 :rule-classes :congruence)

Theorem: vl-immdeps-add-error-fn-of-list-fix-args

(defthm vl-immdeps-add-error-fn-of-list-fix-args
  (equal (vl-immdeps-add-error-fn ans type msg (list-fix args)
                                  fatalp fn)
         (vl-immdeps-add-error-fn ans type msg args fatalp fn)))

Theorem: vl-immdeps-add-error-fn-list-equiv-congruence-on-args

(defthm vl-immdeps-add-error-fn-list-equiv-congruence-on-args
 (implies
  (list-equiv args args-equiv)
  (equal
       (vl-immdeps-add-error-fn ans type msg args fatalp fn)
       (vl-immdeps-add-error-fn ans type msg args-equiv fatalp fn)))
 :rule-classes :congruence)

Theorem: vl-immdeps-add-error-fn-of-bool-fix-fatalp

(defthm vl-immdeps-add-error-fn-of-bool-fix-fatalp
 (equal
      (vl-immdeps-add-error-fn ans
                               type msg args (acl2::bool-fix fatalp)
                               fn)
      (vl-immdeps-add-error-fn ans type msg args fatalp fn)))

Theorem: vl-immdeps-add-error-fn-iff-congruence-on-fatalp

(defthm vl-immdeps-add-error-fn-iff-congruence-on-fatalp
 (implies
  (iff fatalp fatalp-equiv)
  (equal
       (vl-immdeps-add-error-fn ans type msg args fatalp fn)
       (vl-immdeps-add-error-fn ans type msg args fatalp-equiv fn)))
 :rule-classes :congruence)

Theorem: vl-immdeps-add-error-fn-of-symbol-fix-fn

(defthm vl-immdeps-add-error-fn-of-symbol-fix-fn
 (equal
     (vl-immdeps-add-error-fn ans type
                              msg args fatalp (acl2::symbol-fix fn))
     (vl-immdeps-add-error-fn ans type msg args fatalp fn)))

Theorem: vl-immdeps-add-error-fn-symbol-equiv-congruence-on-fn

(defthm vl-immdeps-add-error-fn-symbol-equiv-congruence-on-fn
 (implies
  (acl2::symbol-equiv fn fn-equiv)
  (equal
       (vl-immdeps-add-error-fn ans type msg args fatalp fn)
       (vl-immdeps-add-error-fn ans type msg args fatalp fn-equiv)))
 :rule-classes :congruence)