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 the file indicated by
;; PATH-TO-FILE. If PATH-TO-FILE is a relative path, it is interpreted
;; relative to the CBD.
(defund read-file-into-byte-list (path-to-file state)
(declare (xargs :guard (stringp path-to-file)
:stobjs state))
(mv-let (channel state)
(open-input-channel path-to-file :byte state)
(if (not channel)
;; Error:
(mv `(:could-not-open-channel ,path-to-file) nil state)
(mv-let (bytes state)
(read-bytes-from-channel channel nil state)
(let ((state (close-input-channel channel state)))
(mv nil ; no error
bytes
state))))))
