Restore-x86
- Signature
(restore-x86 filename memsize x86 state) → (mv x86 state)
- Arguments
- filename — The name of the file to read the
non-memory state from. The memory will be read
from <filename>.mem.
Guard (stringp filename).
- memsize — The number of bytes to read out of the memory file and into the memory.
Guard (natp memsize).
Definitions and Theorems
Function: restore-x86
(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))))
