(restore-x86 filename memsize x86 state) → (mv x86 state)
Function:
(defun restore-x86 (filename memsize x86 state) (declare (xargs :stobjs (x86 state))) (declare (xargs :guard (and (stringp filename) (natp memsize)))) (declare (xargs :guard (<= memsize *mem-size-in-bytes*))) (let ((__function__ 'restore-x86)) (declare (ignorable __function__)) (b* (((mv read-in-x86 state) (serialize-read filename)) (x86 (deserialize-x86 read-in-x86 x86)) (memfilename (concatenate 'string filename ".mem")) ((mv memchannel state) (open-input-channel memfilename :byte state)) ((unless memchannel) (mv x86 state)) ((mv x86 state) (read-mem-from-channel memsize memchannel x86 state)) (state (close-input-channel memchannel state))) (mv x86 state))))