		Search-engine friendly clone of the ACL2 documentation.

Program-execution

Load-elf-sections

Signature
(load-elf-sections sections x86) → (mv flg new-x86)
Arguments: sections — Guard (exld::section-info-list-p sections).
Returns: new-x86 — Type (x86p new-x86), given (x86p x86).

Definitions and Theorems

Function: load-elf-sections

(defun load-elf-sections (sections x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (exld::section-info-list-p sections)))
 (let ((__function__ 'load-elf-sections))
  (declare (ignorable __function__))
  (b* (((when (atom sections)) (mv nil x86))
       ((mv flg x86)
        (load-elf-sections (cdr sections) x86))
       ((exld::section-info section)
        (car sections))
       ((exld::elf-section-header header)
        section.header)
       ((unless section.bytes)
        (prog2$ (cw "~%Empty ~s0 section! Nothing loaded.~%"
                    header.name-str)
                (mv flg x86))))
   (if
    (logbitp 1 header.flags)
    (if
     (and (canonical-address-p header.addr)
          (canonical-address-p (+ (len section.bytes) header.addr)))
     (write-bytes-to-memory header.addr section.bytes x86)
     (mv (cons header.name-str flg) x86))
    (prog2$
     (cw
      "~%Section ~s0 is not marked as SHF_ALLOC in its ELF section header, ~
 so we don't allocate memory for it in the RV model.~%"
      header.name-str)
     (mv nil x86))))))

Theorem: x86p-of-load-elf-sections.new-x86

(defthm x86p-of-load-elf-sections.new-x86
  (implies (x86p x86)
           (b* (((mv ?flg ?new-x86)
                 (load-elf-sections sections x86)))
             (x86p new-x86)))
  :rule-classes :rewrite)