		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Read-section-names

Get the names of the section headers from the string section table, located at the offset indicated by the sh_offset value of the shstrndxth section

Signature
(read-section-names sec-headers string-section-data acc) → new-sec-headers
Arguments: sec-headers — Guard (elf-section-headers-p sec-headers).; string-section-data — Guard (byte-listp string-section-data).; acc — Guard (elf-section-headers-p acc).
Returns: new-sec-headers — Type (elf-section-headers-p new-sec-headers), given (elf-section-headers-p acc).

Definitions and Theorems

Function: read-section-names

(defun read-section-names (sec-headers string-section-data acc)
 (declare (xargs :guard (and (elf-section-headers-p sec-headers)
                             (byte-listp string-section-data)
                             (elf-section-headers-p acc))))
 (let ((__function__ 'read-section-names))
  (declare (ignorable __function__))
  (if (atom sec-headers)
      acc
   (b*
    ((section-header (car sec-headers))
     ((elf-section-header section-header))
     (name-str-offset section-header.name)
     ((unless (<= name-str-offset
                  (len string-section-data)))
      (prog2$
       (raise
        "String-section-data's length should be at least ~x0, but it is ~x1 instead!"
        name-str-offset
        (len string-section-data))
       acc))
     (name-str (elf-read-string-null-term
                    string-section-data name-str-offset))
     (new-section-header
          (change-elf-section-header section-header
                                     :name-str name-str)))
    (read-section-names (cdr sec-headers)
                        string-section-data
                        (cons new-section-header acc))))))

Theorem: elf-section-headers-p-of-read-section-names

(defthm elf-section-headers-p-of-read-section-names
 (implies
   (elf-section-headers-p acc)
   (b*
    ((new-sec-headers
          (read-section-names sec-headers string-section-data acc)))
    (elf-section-headers-p new-sec-headers)))
 :rule-classes :rewrite)