		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Get-section-info1

Signature
(get-section-info1 name section-info-list section-names) → section-info
Arguments: name — Name of a section header; e.g., ".symtab".
Guard (stringp name).; section-info-list — Guard (section-info-list-p section-info-list).; section-names — Guard (string-listp section-names).
Returns: section-info — Type (section-info-p section-info), given (section-info-list-p section-info-list).

Definitions and Theorems

Function: get-section-info1

(defun get-section-info1 (name section-info-list section-names)
 (declare (xargs :guard (and (stringp name)
                             (section-info-list-p section-info-list)
                             (string-listp section-names))))
 (declare
      (xargs :guard (subsetp-equal (section-names section-info-list)
                                   section-names)))
 (let ((__function__ 'get-section-info1))
  (declare (ignorable __function__))
  (b*
   (((when (atom section-info-list))
     (prog2$
        (raise "Section ~s0 not found! List of sections found: ~x1."
               name section-names)
        (make-section-info)))
    ((section-info section-info)
     (car section-info-list))
    ((elf-section-header section-info.header))
    ((when (equal (str::trim section-info.header.name-str)
                  (str::trim name)))
     section-info))
   (get-section-info1 name (cdr section-info-list)
                      section-names))))

Theorem: section-info-p-of-get-section-info1

(defthm section-info-p-of-get-section-info1
 (implies
   (section-info-list-p section-info-list)
   (b*
    ((section-info
          (get-section-info1 name section-info-list section-names)))
    (section-info-p section-info)))
 :rule-classes :rewrite)