		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Is-elf-content-p

Check if contents represent a valid ELF binary (in bytes, LSB-first); if so, return the ELF header

Signature
(is-elf-content-p contents state) → (mv is-elf-file header state)
Arguments: contents — Guard (byte-listp contents).
Returns: is-elf-file — Type (booleanp is-elf-file).; header — Type (elf-header-p header).

Definitions and Theorems

Function: is-elf-content-p

(defun is-elf-content-p (contents state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (byte-listp contents)))
 (let ((__function__ 'is-elf-content-p))
   (declare (ignorable __function__))
   (b*
    (((unless (<= 64 (len contents)))
      (prog2$ (raise "Error reading ELF contents!")
              (mv nil (make-elf-header) state)))
     (bytes contents)
     (file-header (take 64 bytes))
     ((elf-header header)
      (read-elf-header file-header))
     (magic (merge-bytes header.magic))
     (class header.class)
     ((when (or (not (equal magic *elfmag*))
                (not (member class '(1 2)))))
      (prog2$ (raise "Error:  Invalid ELF header! ~% Header: ~x0 ~%"
                     header)
              (mv nil (make-elf-header) state))))
    (mv t header state))))

Theorem: booleanp-of-is-elf-content-p.is-elf-file

(defthm booleanp-of-is-elf-content-p.is-elf-file
  (b* (((mv ?is-elf-file acl2::?header acl2::?state)
        (is-elf-content-p contents state)))
    (booleanp is-elf-file))
  :rule-classes :type-prescription)

Theorem: elf-header-p-of-is-elf-content-p.header

(defthm elf-header-p-of-is-elf-content-p.header
  (b* (((mv ?is-elf-file acl2::?header acl2::?state)
        (is-elf-content-p contents state)))
    (elf-header-p header))
  :rule-classes :rewrite)