		Search-engine friendly clone of the ACL2 documentation.

Vl-read-file

Vl-read-file-hook

Customizable hook for vl-read-file.

This is generally intended for collecting up statistics on the files that have been read. By default we do nothing.

Definitions and Theorems

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

(defthm state-p1-of-vl-read-file-hook
  (implies
       (force (state-p1 state))
       (state-p1 (vl-read-file-hook filename contents len state))))

Function: vl-read-file-hook-default

(defun vl-read-file-hook-default (filename contents len state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (stringp filename)
                              (vl-echarlist-p contents)
                              (equal len (len contents)))))
  (declare (ignore filename contents len))
  (let ((__function__ 'vl-read-file-hook-default))
    (declare (ignorable __function__))
    state))

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

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