Read-file-into-byte-array-stobj
Read the bytes from a file into a stobj array.
;; Returns (mv erp byte-array-stobj state) where either ERP is non-nil (meaning an error
;; occurred) or else the bytes field of BYTE-ARRAY-STOBJ contains the contents of FILENAME.
(defund read-file-into-byte-array-stobj (filename byte-array-stobj state)
(declare (xargs :guard (stringp filename)
:stobjs (byte-array-stobj state)))
(mv-let (file-length state)
(file-length$ filename state)
(if (not file-length)
(mv `(:failed-to-get-file-length ,filename) byte-array-stobj state)
(mv-let (channel state)
(open-input-channel filename :byte state)
(if (not channel)
;; Error:
(mv `(:could-not-open-channel ,filename) byte-array-stobj state)
(let ( ;; make the array the right size:
(byte-array-stobj (resize-bytes file-length byte-array-stobj)))
(mv-let (byte-array-stobj state)
(read-file-into-byte-array-stobj-aux channel 0 byte-array-stobj state)
(let ((state (close-input-channel channel state)))
(mv nil ; no error
byte-array-stobj
state)))))))))
