		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Section-names

Get all names from sections in section-info-list

Signature
(section-names section-info-list) → sec-names
Arguments: section-info-list — Guard (section-info-list-p section-info-list).
Returns: sec-names — Type (string-listp sec-names), given the guard.

Definitions and Theorems

Function: section-names

(defun section-names (section-info-list)
  (declare (xargs :guard (section-info-list-p section-info-list)))
  (let ((__function__ 'section-names))
    (declare (ignorable __function__))
    (b* (((when (atom section-info-list)) nil)
         ((section-info section-info)
          (car section-info-list))
         ((elf-section-header section-info.header)))
      (cons section-info.header.name-str
            (section-names (cdr section-info-list))))))

Theorem: string-listp-of-section-names

(defthm string-listp-of-section-names
  (implies (and (section-info-list-p section-info-list))
           (b* ((sec-names (section-names section-info-list)))
             (string-listp sec-names)))
  :rule-classes :rewrite)

Theorem: cdr-section-names

(defthm cdr-section-names
  (equal (section-names (cdr sec-info-list))
         (cdr (section-names sec-info-list))))