• 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-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-find-file
        • Vl-read-files
        • 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
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• 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)))