Read-file-into-byte-list
Read a file into a list of bytes.
;; Returns (mv erp bytes state) where either ERP is non-nil (meaning an error
;; occurred) or else BYTES is the contents of FILENAME.
(defund read-file-into-byte-list (filename state)
(declare (xargs :guard (stringp filename)
:stobjs state))
(mv-let (channel state)
(open-input-channel filename :byte state)
(if (not channel)
;; Error:
(mv `(:could-not-open-channel ,filename) nil state)
(mv-let (bytes state)
(read-file-into-byte-list-aux channel nil state)
(let ((state (close-input-channel channel state)))
(mv nil ; no error
bytes
state))))))
