		Search-engine friendly clone of the ACL2 documentation.

Virtualization-for-validation

Write-virtualizable-mem

Write the memory to a channel.

Signature
(write-virtualizable-mem start end channel x86 state) → state
Arguments: channel — Guard (symbolp channel).

Definitions and Theorems

Function: write-virtualizable-mem

(defun write-virtualizable-mem (start end channel x86 state)
  (declare (xargs :stobjs (x86 state)))
  (declare (type (integer 0 4503599627370496)
                 start)
           (type (integer 0 4503599627370496) end))
  (declare (xargs :guard (symbolp channel)))
  (declare (xargs :guard (and (<= start end)
                              (open-output-channel-p channel
                                                     :byte state))))
  (let ((__function__ 'write-virtualizable-mem))
    (declare (ignorable __function__))
    (if (= start end)
        state
      (b* ((state (write-byte$ (memi start x86)
                               channel state)))
        (write-virtualizable-mem (1+ start)
                                 end channel x86 state)))))