		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Get-named-section-headers

Signature
(get-named-section-headers elf-header file-byte-list) → new-sections
Arguments: elf-header — Guard (elf-header-p elf-header).; file-byte-list — Guard (byte-listp file-byte-list).
Returns: new-sections — Type (elf-section-headers-p new-sections).

Definitions and Theorems

Function: get-named-section-headers

(defun get-named-section-headers (elf-header file-byte-list)
 (declare (xargs :guard (and (elf-header-p elf-header)
                             (byte-listp file-byte-list))))
 (let ((__function__ 'get-named-section-headers))
  (declare (ignorable __function__))
  (b*
   (((elf-header elf-header))
    (section-header-offset elf-header.shoff)
    (section-header-bytes
         (nthcdr section-header-offset file-byte-list))
    ((unless (byte-listp section-header-bytes))
     (prog2$ (raise "Not enough bytes to read ELF section headers!")
             nil))
    (nsections elf-header.shnum)
    (w (if (equal elf-header.class 1) 4 8))
    (string-section-index elf-header.shstrndx)
    ((when (not (or (equal nsections string-section-index)
                    (> nsections string-section-index))))
     (prog2$
      (raise
       "ELF Binary: Mismatch between number of sections and string-section-index. ~
 Strings could not be read. ~%")
      nil))
    (headers
        (read-section-headers nsections w section-header-bytes nil))
    (string-section-data
         (get-string-section-data string-section-index
                                  headers file-byte-list))
    (updated-headers
         (read-section-names headers string-section-data nil)))
   updated-headers)))

Theorem: elf-section-headers-p-of-get-named-section-headers

(defthm elf-section-headers-p-of-get-named-section-headers
  (b* ((new-sections
            (get-named-section-headers elf-header file-byte-list)))
    (elf-section-headers-p new-sections))
  :rule-classes :rewrite)