		Search-engine friendly clone of the ACL2 documentation.

Loader

Vl-load-read-file-hook

Signature
(vl-load-read-file-hook filename contents len state) → state
Arguments: filename — Guard (stringp filename).; contents — Guard (vl-echarlist-p contents).; len — Guard (equal len (len contents)).
Returns: state — Type (state-p1 state), given (state-p1 state).

Definitions and Theorems

Function: vl-load-read-file-hook

(defun
 vl-load-read-file-hook
 (filename contents len state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (stringp filename)
                             (vl-echarlist-p contents)
                             (equal len (len contents)))))
 (declare (ignorable contents))
 (let
  ((__function__ 'vl-load-read-file-hook))
  (declare (ignorable __function__))
  (b*
   ((file-alist (and (boundp-global 'vl-read-file-alist
                                    state)
                     (f-get-global 'vl-read-file-alist
                                   state)))
    (entry (cdr (hons-get filename file-alist)))
    ((cons num-reads len)
     (if
      entry
      (if
       (and (consp entry)
            (natp (car entry))
            (natp (cdr entry)))
       entry
       (progn$
         (raise "Unexpected vl-read-file-alist entry for ~x0: ~x1~%"
                filename entry)
         '(0 . 0)))
      (cons 0 len)))
    (new-entry (cons (+ 1 num-reads) len))
    (new-alist (hons-acons filename new-entry file-alist))
    (state (f-put-global 'vl-read-file-alist
                         new-alist state)))
   state)))

Theorem: state-p1-of-vl-load-read-file-hook

(defthm
 state-p1-of-vl-load-read-file-hook
 (implies
  (state-p1 state)
  (b* ((state (vl-load-read-file-hook filename contents len state)))
      (state-p1 state)))
 :rule-classes :rewrite)