		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Populate-elf

Initialize the ELF stobj with contents of ELF binary filename

Signature
(populate-elf filename elf state) → (mv new-elf state)
Arguments: filename — Guard (stringp filename).
Returns: new-elf — Type (good-elf-p new-elf), given (good-elf-p elf).

Definitions and Theorems

Function: populate-elf

(defun populate-elf (filename elf state)
  (declare (xargs :stobjs (elf state)))
  (declare (xargs :guard (stringp filename)))
  (let ((__function__ 'populate-elf))
    (declare (ignorable __function__))
    (b* (((mv contents state)
          (acl2::read-file-bytes filename state))
         ((unless (byte-listp contents))
          (prog2$ (raise "Error reading file ~s0!" filename)
                  (mv elf state))))
      (populate-elf-contents contents elf state))))

Theorem: good-elf-p-of-populate-elf.new-elf

(defthm good-elf-p-of-populate-elf.new-elf
  (implies (good-elf-p elf)
           (b* (((mv ?new-elf acl2::?state)
                 (populate-elf filename elf state)))
             (good-elf-p new-elf)))
  :rule-classes :rewrite)