• 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-find-file-aux
          • Vl-extend-pathname
        • 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Loader

Vl-find-file

Determine where to load a file from, given its (absolute or relative) name and a list of directories to search.

Signature: (vl-find-file filename searchpath state) returns (mv realname state).

The filename is the name of a file you want to load; it can be either an absolute filename (in which case it will just be returned as realname), or a relative filename (in which case we will look for it in the searchpath).

The searchpath is a list of strings that are the names of directories to search. These order of these directories is important, because we search them in order.

If we find the file in any of the search directories, we essentially return dir/filename as realname. But if we can't find the file anywhere, realname is just nil.

Definitions and Theorems

Function: vl-find-file

(defun vl-find-file (filename searchpath state)
  (declare (xargs :guard (and (stringp filename)
                              (string-listp searchpath)
                              (state-p state))))
  (if (acl2::absolute-pathname-string-p
           filename nil (acl2::os (w state)))
      (mv filename state)
    (vl-find-file-aux filename searchpath state)))

Theorem: state-p1-of-vl-find-file

(defthm state-p1-of-vl-find-file
 (implies
      (and (force (state-p1 state))
           (force (stringp filename)))
      (state-p1 (mv-nth 1
                        (vl-find-file filename searchpath state)))))

Theorem: stringp-of-vl-find-file

(defthm stringp-of-vl-find-file
 (implies
  (force (stringp filename))
  (equal (stringp (mv-nth 0
                          (vl-find-file filename searchpath state)))
         (if (mv-nth 0
                     (vl-find-file filename searchpath state))
             t
           nil)))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (implies
    (force (stringp filename))
    (or (not (mv-nth 0
                     (vl-find-file filename searchpath state)))
        (stringp
             (mv-nth 0
                     (vl-find-file filename searchpath state))))))))

Subtopics

Vl-find-file-aux

Look for a file in a list of search directories.

Vl-extend-pathname

(vl-extend-pathname dir filename) concatenates dir and filename, adding a slash to between them only if dir does not end with a slash.