		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Get-label-address

Return the address of label, if present, by searching in the sym/str table information

Signature
(get-label-address label elf) → addr
Arguments: label — Guard (stringp label).
Returns: addr — Type (acl2::maybe-natp addr), given the guard.

Definitions and Theorems

Function: get-label-address

(defun get-label-address (label elf)
 (declare (xargs :stobjs (elf)))
 (declare (xargs :guard (stringp label)))
 (let ((__function__ 'get-label-address))
  (declare (ignorable __function__))
  (b*
   ((entries (get-symtab-entries elf))
    (elf64 (equal (elf-header->class (@elf-header elf))
                  2))
    (addr
     (find-label-address-from-elf-symtab-info elf64 label entries)))
   addr)))

Theorem: maybe-natp-of-get-label-address

(defthm maybe-natp-of-get-label-address
  (implies (and (elfp elf) (stringp label))
           (b* ((addr (get-label-address label elf)))
             (acl2::maybe-natp addr)))
  :rule-classes :rewrite)