Save-x86
- Signature
(save-x86 filename memsize x86 state) → state
- Arguments
- filename — The name of the file to write the
non-memory state out to. The memory will be written
out to <filename>.mem.
Guard (stringp filename).
- memsize — The number of bytes of memory to save.
Guard (natp memsize).
Definitions and Theorems
Function: save-x86
(defun save-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__ 'save-x86))
(declare (ignorable __function__))
(b* ((serialized-x86 (serialize-x86 x86))
(state (serialize-write filename serialized-x86))
(memfilename (concatenate 'string filename ".mem"))
((mv memchannel state)
(open-output-channel memfilename
:byte state))
((unless memchannel) state)
(state (write-mem-to-channel memsize memchannel x86 state))
(state (close-output-channel memchannel state)))
state)))
