		Search-engine friendly clone of the ACL2 documentation.

Program-execution

Init-zero-page

Signature
(init-zero-page zero-page-ptr command-line-ptr disk-image-ptr disk-image-size kernel-ptr kernel-image x86) → x86
Arguments: zero-page-ptr — Guard (canonical-address-p zero-page-ptr).; command-line-ptr — Guard (canonical-address-p command-line-ptr).; disk-image-ptr — Guard (canonical-address-p disk-image-ptr).; disk-image-size — Guard (natp disk-image-size).; kernel-ptr — Guard (n32p kernel-ptr).; kernel-image — Guard (byte-listp kernel-image).

Definitions and Theorems

Function: init-zero-page

(defun init-zero-page (zero-page-ptr command-line-ptr
                                     disk-image-ptr disk-image-size
                                     kernel-ptr kernel-image x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (and (canonical-address-p zero-page-ptr)
                             (canonical-address-p command-line-ptr)
                             (canonical-address-p disk-image-ptr)
                             (natp disk-image-size)
                             (n32p kernel-ptr)
                             (byte-listp kernel-image))))
 (declare
  (xargs :guard (and (canonical-address-p (+ zero-page-ptr 4095)))))
 (let ((__function__ 'init-zero-page))
   (declare (ignorable __function__))
   (b*
    (((unless (> (len kernel-image) 529))
      x86)
     ((unless (> (len kernel-image) (+ 620 497)))
      x86)
     (setup-header (take 620 (nthcdr 497 kernel-image)))
     ((mv & x86)
      (write-bytes-to-memory (+ zero-page-ptr 497)
                             setup-header x86))
     ((mv & x86)
      (write-bytes-to-memory (+ zero-page-ptr 506)
                             '(255 255)
                             x86))
     ((mv & x86)
      (write-bytes-to-memory (+ zero-page-ptr 528)
                             '(255)
                             x86))
     (loadflags (logand (nth 529 kernel-image) 95))
     ((mv & x86)
      (write-bytes-to-memory (+ zero-page-ptr 529)
                             (list loadflags)
                             x86))
     ((mv & x86)
      (write-bytes-to-memory (+ zero-page-ptr 532)
                             (pack-u32 kernel-ptr)
                             x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 536)
           (pack-u32 (logand 4294967295 disk-image-ptr))
           x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 540)
           (pack-u32 (logand 4294967295 disk-image-size))
           x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 552)
           (pack-u32 (logand 4294967295 command-line-ptr))
           x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 192)
           (pack-u32 (logand 4294967295 (ash disk-image-ptr -32)))
           x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 196)
           (pack-u32 (logand 4294967295 (ash disk-image-size -32)))
           x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 200)
           (pack-u32 (logand 4294967295 (ash command-line-ptr -32)))
           x86)))
    x86)))