• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
          • Vl-iframe-p
          • Preprocessor-ifdef-minutia
          • Vl-preprocess-loop
          • Vl-read-until-end-of-define
          • Vl-expand-define
          • Vl-read-include
          • Vl-process-ifdef
          • Vl-substitute-into-macro-text
          • Vl-preprocess
          • Vl-define
          • Vl-process-define
          • Vl-process-undef
          • Preprocessor-include-minutia
          • Vl-split-define-text
          • Vl-read-timescale
          • Vl-line-up-define-formals-and-actuals
          • Vl-process-else
          • Vl-process-endif
          • Vl-istack-p
          • Vl-is-compiler-directive-p
          • Vl-check-remaining-formals-all-have-defaults
          • Vl-safe-previous-n
          • Vl-safe-next-n
          • Vl-defines
          • *vl-preprocess-clock*
        • 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-read-files
        • Vl-find-file
        • Extended-characters
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • 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
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Preprocessor

Vl-process-undef

Handler for undef directives.

Signature

(vl-process-undef loc echars defines activep) 
  → 
(mv successp new-defines remainder)

Arguments

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

echars — Guard (vl-echarlist-p echars).

defines — Guard (vl-defines-p defines).

activep — Guard (booleanp activep).

Returns

new-defines — Type (vl-defines-p new-defines).

remainder — Type (vl-echarlist-p remainder), given (force (vl-echarlist-p echars)).

We assume that an `undef has just been read and echars is the text which follows it. We try to read the name we are to undefine, then update the defines table appropriately.

Definitions and Theorems

Function: vl-process-undef

(defun
 vl-process-undef
 (loc echars defines activep)
 (declare (xargs :guard (and (vl-location-p loc)
                             (vl-echarlist-p echars)
                             (vl-defines-p defines)
                             (booleanp activep))))
 (let
  ((__function__ 'vl-process-undef))
  (declare (ignorable __function__))
  (b*
   ((defines (vl-defines-fix defines))
    ((mv & remainder)
     (vl-read-while-whitespace echars))
    ((mv name & remainder)
     (vl-read-identifier remainder))
    ((when (not name))
     (mv
      (cw
       "Preprocessor error (~s0): found an `undef without a name.~%"
       (vl-location-string loc))
      defines echars))
    ((when (vl-is-compiler-directive-p name))
     (mv
      (cw
        "Preprocessor error (~s0): refusing to permit `undef ~s1.~%"
        (vl-location-string loc)
        name)
      defines echars))
    ((when (not activep))
     (mv t defines remainder))
    (lookup (vl-find-define name defines))
    (-
     (if
      (not lookup)
      (cw
       "Preprocessor warning (~s0): found `undef ~s1, but ~s1 is ~
                   not defined.~%"
       (vl-location-string loc)
       name)
      (cw "Undefining ~s0.~%" name)))
    (defines (vl-delete-define name defines)))
   (mv t defines remainder))))

Theorem: vl-defines-p-of-vl-process-undef.new-defines

(defthm vl-defines-p-of-vl-process-undef.new-defines
        (b* (((mv ?successp ?new-defines ?remainder)
              (vl-process-undef loc echars defines activep)))
            (vl-defines-p new-defines))
        :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-process-undef.remainder

(defthm
     vl-echarlist-p-of-vl-process-undef.remainder
     (implies (force (vl-echarlist-p echars))
              (b* (((mv ?successp ?new-defines ?remainder)
                    (vl-process-undef loc echars defines activep)))
                  (vl-echarlist-p remainder)))
     :rule-classes :rewrite)

Theorem: true-listp-of-vl-process-undef-remainder

(defthm
 true-listp-of-vl-process-undef-remainder
 (equal (true-listp
             (mv-nth 2
                     (vl-process-undef loc echars defines activep)))
        (true-listp echars)))

Theorem: acl2-count-of-vl-process-undef

(defthm
    acl2-count-of-vl-process-undef
    (<= (acl2-count
             (mv-nth 2
                     (vl-process-undef loc echars defines activep)))
        (acl2-count echars))
    :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-process-undef-strong

(defthm
 acl2-count-of-vl-process-undef-strong
 (implies
     (mv-nth 0
             (vl-process-undef loc echars defines activep))
     (< (acl2-count
             (mv-nth 2
                     (vl-process-undef loc echars defines activep)))
        (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))