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.
(defthm state-p1-of-vl-read-file-hook (implies (force (state-p1 state)) (state-p1 (vl-read-file-hook filename contents len state))))
(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))