		Search-engine friendly clone of the ACL2 documentation.

Vl-read-file

Vl-read-file-rchars

Optimized alternative to vl-read-file that reads the entire file into nrev.

Signature
(vl-read-file-rchars filename nrev &key (state 'state)) → (mv okp nrev state)
Arguments: filename — The file to read.
Guard (stringp filename).

We implement this mainly for vl-read-files.

Definitions and Theorems

Function: vl-read-file-rchars-fn

(defun vl-read-file-rchars-fn (filename nrev state)
  (declare (xargs :stobjs (nrev state)))
  (declare (xargs :guard (stringp filename)))
  (let ((__function__ 'vl-read-file-rchars))
    (declare (ignorable __function__))
    (mbe :logic
         (non-exec (b* (((mv okp data state)
                         (vl-read-file filename)))
                     (mv okp (append nrev data) state)))
         :exec
         (b* (((mv channel state)
               (open-input-channel filename
                                   :byte state))
              ((unless channel) (mv nil nrev state))
              ((mv nrev state)
               (vl-read-file-loop-aux channel filename 1 0 nrev))
              (state (close-input-channel channel state)))
           (mv t nrev state)))))