		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Get-label-addresses

Return the addresses of each valid label in labels by searching in the sym/str table information

Signature
(get-label-addresses labels elf) → addrs
Arguments: labels — Guard (string-listp labels).
Returns: addrs — Type (true-listp addrs), given the guard.

Definitions and Theorems

Function: get-label-addresses

(defun get-label-addresses (labels elf)
  (declare (xargs :stobjs (elf)))
  (declare (xargs :guard (string-listp labels)))
  (let ((__function__ 'get-label-addresses))
    (declare (ignorable __function__))
    (if (atom labels)
        nil
      (cons (get-label-address (car labels) elf)
            (get-label-addresses (cdr labels)
                                 elf)))))

Theorem: true-listp-of-get-label-addresses

(defthm true-listp-of-get-label-addresses
  (implies (and (elfp elf) (string-listp labels))
           (b* ((addrs (get-label-addresses labels elf)))
             (true-listp addrs)))
  :rule-classes :rewrite)