		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Set-elf-stobj-fields

Populate ELF stobj with bytes corresponding to each section

Signature
(set-elf-stobj-fields sec-headers file-bytes elf) → new-elf
Arguments: sec-headers — Guard (elf-section-headers-p sec-headers).; file-bytes — Guard (byte-listp file-bytes).
Returns: new-elf — Type (good-elf-p new-elf), given (good-elf-p elf).

Definitions and Theorems

Function: set-elf-stobj-fields

(defun set-elf-stobj-fields (sec-headers file-bytes elf)
 (declare (xargs :stobjs (elf)))
 (declare (xargs :guard (and (elf-section-headers-p sec-headers)
                             (byte-listp file-bytes))))
 (let ((__function__ 'set-elf-stobj-fields))
  (declare (ignorable __function__))
  (if (atom sec-headers)
      elf
   (b*
    ((sec-header (car sec-headers))
     ((elf-section-header sec-header))
     (bytes (take sec-header.size
                  (nthcdr sec-header.offset file-bytes)))
     (elf
      (if (byte-listp bytes)
          (b* ((section (make-section-info :header sec-header
                                           :bytes bytes)))
            (!sections (cons section (@sections elf))
                       elf))
       (prog2$
        (cw
         "~% Insufficient number of bytes in the file to grab section ~s0!~% ~
  This could be a problem later, but we're moving on anyway..."
         sec-header.name-str)
        elf))))
    (set-elf-stobj-fields (cdr sec-headers)
                          file-bytes elf)))))

Theorem: good-elf-p-of-set-elf-stobj-fields

(defthm good-elf-p-of-set-elf-stobj-fields
 (implies
   (good-elf-p elf)
   (b* ((new-elf (set-elf-stobj-fields sec-headers file-bytes elf)))
     (good-elf-p new-elf)))
 :rule-classes :rewrite)