		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)