		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Get-string-section-data

Signature
(get-string-section-data string-section-index sec-headers file-byte-list) → bl
Arguments: string-section-index — Guard (natp string-section-index).; sec-headers — Guard (elf-section-headers-p sec-headers).; file-byte-list — Guard (byte-listp file-byte-list).
Returns: bl — Type (byte-listp bl), given (byte-listp file-byte-list).

Definitions and Theorems

Function: get-string-section-data

(defun get-string-section-data
       (string-section-index sec-headers file-byte-list)
 (declare (xargs :guard (and (natp string-section-index)
                             (elf-section-headers-p sec-headers)
                             (byte-listp file-byte-list))))
 (let ((__function__ 'get-string-section-data))
  (declare (ignorable __function__))
  (b*
   ((sec-headers-from-string-section-index
         (nthcdr string-section-index sec-headers))
    ((unless (and (consp sec-headers-from-string-section-index)
                  (elf-section-headers-p
                       sec-headers-from-string-section-index)))
     (prog2$ (er hard? 'elf-file-read
                 "String-section-index header not found!~%")
             nil))
    (header (car sec-headers-from-string-section-index))
    ((elf-section-header header))
    (string-section-header-bytes
         (take header.size
               (nthcdr header.offset file-byte-list)))
    ((unless (byte-listp string-section-header-bytes))
     (prog2$
         (er hard? 'elf-file-read
             "Not enough bytes to read string-section-header data!")
         nil)))
   string-section-header-bytes)))

Theorem: byte-listp-of-get-string-section-data

(defthm byte-listp-of-get-string-section-data
 (implies
     (byte-listp file-byte-list)
     (b* ((bl (get-string-section-data string-section-index
                                       sec-headers file-byte-list)))
       (byte-listp bl)))
 :rule-classes :rewrite)