Write bytes to a file when not allowed without a trust tag.
;; Writes the BYTES to file FILENAME, overwriting its previous contents. ;; Returns (mv erp state). The ttag is needed because this calls ;; open-output-channel!, but that makes this version usable during make-event ;; expansion, clause-processors, etc. (defun write-bytes-to-file! (bytes filename ctx state) (declare (xargs :stobjs state :guard (and (all-bytep bytes) (stringp filename)))) (mv-let (channel state) (open-output-channel! filename :byte state) (if (not channel) (prog2$ (er hard? ctx "Unable to open file ~s0 for :byte output." filename) (mv t state)) (pprogn (write-bytes-to-channel bytes channel state) (close-output-channel channel state) (mv nil state)))))