		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Read-segment-headers-32

Read 64-bit ELF segment headers

Signature
(read-segment-headers-32 nsegments rest-of-the-file acc) → 32-bit-segments
Arguments: nsegments — Guard (natp nsegments).; rest-of-the-file — Guard (byte-listp rest-of-the-file).; acc — Guard (elf32-segment-headers-p acc).
Returns: 32-bit-segments — Type (elf32-segment-headers-p 32-bit-segments), given (elf32-segment-headers-p acc).

Definitions and Theorems

Function: read-segment-headers-32

(defun read-segment-headers-32 (nsegments rest-of-the-file acc)
  (declare (xargs :guard (and (natp nsegments)
                              (byte-listp rest-of-the-file)
                              (elf32-segment-headers-p acc))))
  (let ((__function__ 'read-segment-headers-32))
    (declare (ignorable __function__))
    (if (zp nsegments)
        (reverse acc)
      (b* (((mv p_type rest-of-the-file)
            (merge-first-split-bytes 4 rest-of-the-file))
           ((mv p_offset rest-of-the-file)
            (merge-first-split-bytes 4 rest-of-the-file))
           ((mv p_vaddr rest-of-the-file)
            (merge-first-split-bytes 4 rest-of-the-file))
           ((mv p_paddr rest-of-the-file)
            (merge-first-split-bytes 4 rest-of-the-file))
           ((mv p_filesz rest-of-the-file)
            (merge-first-split-bytes 4 rest-of-the-file))
           ((mv p_memsz rest-of-the-file)
            (merge-first-split-bytes 4 rest-of-the-file))
           ((mv p_flags rest-of-the-file)
            (merge-first-split-bytes 4 rest-of-the-file))
           ((mv p_align rest-of-the-file)
            (merge-first-split-bytes 4 rest-of-the-file))
           (segment (make-elf32-segment-header :type p_type
                                               :flags p_flags
                                               :offset p_offset
                                               :vaddr p_vaddr
                                               :paddr p_paddr
                                               :filesz p_filesz
                                               :memsz p_memsz
                                               :align p_align)))
        (read-segment-headers-32
             (1- nsegments)
             rest-of-the-file (cons segment acc))))))

Theorem: elf32-segment-headers-p-of-read-segment-headers-32

(defthm elf32-segment-headers-p-of-read-segment-headers-32
 (implies
   (elf32-segment-headers-p acc)
   (b*
    ((32-bit-segments
          (read-segment-headers-32 nsegments rest-of-the-file acc)))
    (elf32-segment-headers-p 32-bit-segments)))
 :rule-classes :rewrite)