		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Parse-symtab-entries

Signature
(parse-symtab-entries elf64 entrysize symbytes strbytes) → elf-entries
Arguments: elf64 — Guard (booleanp elf64).; entrysize — Guard (natp entrysize).; symbytes — Guard (byte-listp symbytes).; strbytes — Guard (byte-listp strbytes).

Definitions and Theorems

Function: parse-symtab-entries

(defun parse-symtab-entries (elf64 entrysize symbytes strbytes)
 (declare (xargs :guard (and (booleanp elf64)
                             (natp entrysize)
                             (byte-listp symbytes)
                             (byte-listp strbytes))))
 (let ((__function__ 'parse-symtab-entries))
  (declare (ignorable __function__))
  (b*
   (((unless (and (< 0 (len symbytes))
                  (< 0 (nfix entrysize))))
     nil)
    ((mv entry rest-symbytes)
     (merge-first-split-bytes entrysize symbytes))
    ((unless (if elf64 (elf64_sym-p entry)
               (elf32_sym-p entry)))
     (prog2$ (raise "Inconsistency with entrysize and symbytes?")
             nil))
    (entry-name (if elf64 (elf64_sym->name entry)
                  (elf32_sym->name entry)))
    (name-str
     (bytes->string (take-till-zero (nthcdr entry-name strbytes)))))
   (cons (if elf64 (make-elf64_sym-info :name-str name-str
                                        :entry entry)
           (make-elf32_sym-info :name-str name-str
                                :entry entry))
         (parse-symtab-entries elf64
                               entrysize rest-symbytes strbytes)))))

Theorem: elf64_sym-info-list-p-of-parse-symtab-entries

(defthm elf64_sym-info-list-p-of-parse-symtab-entries
  (b*
    ((?elf-entries
          (parse-symtab-entries elf64 entrysize symbytes strbytes)))
    (implies elf64
             (elf64_sym-info-list-p elf-entries))))

Theorem: elf32_sym-info-list-p-of-parse-symtab-entries

(defthm elf32_sym-info-list-p-of-parse-symtab-entries
  (b*
    ((?elf-entries
          (parse-symtab-entries elf64 entrysize symbytes strbytes)))
    (implies (not elf64)
             (elf32_sym-info-list-p elf-entries))))