		Search-engine friendly clone of the ACL2 documentation.

Elf-header

Make-elf-header

Basic constructor macro for elf-header structures.

Syntax

(make-elf-header [:magic <magic>] 
                 [:class <class>] 
                 [:dataenc <dataenc>] 
                 [:identver <identver>] 
                 [:osabi <osabi>] 
                 [:abiver <abiver>] 
                 [:padding <padding>] 
                 [:type <type>] 
                 [:machine <machine>] 
                 [:version <version>] 
                 [:entry <entry>] 
                 [:phoff <phoff>] 
                 [:shoff <shoff>] 
                 [:flags <flags>] 
                 [:ehsize <ehsize>] 
                 [:phentsize <phentsize>] 
                 [:phnum <phnum>] 
                 [:shentsize <shentsize>] 
                 [:shnum <shnum>] 
                 [:shstrndx <shstrndx>])

This is the usual way to construct elf-header structures. It simply conses together a structure with the specified fields.

This macro generates a new elf-header structure from scratch. See also change-elf-header, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-elf-header

(defmacro make-elf-header (&rest args)
  (std::make-aggregate 'elf-header
                       args
                       '((:magic quote nil)
                         (:class . 0)
                         (:dataenc . 0)
                         (:identver . 0)
                         (:osabi . 0)
                         (:abiver . 0)
                         (:padding quote nil)
                         (:type . 0)
                         (:machine . 0)
                         (:version . 0)
                         (:entry . 0)
                         (:phoff . 0)
                         (:shoff . 0)
                         (:flags . 0)
                         (:ehsize . 0)
                         (:phentsize . 0)
                         (:phnum . 0)
                         (:shentsize . 0)
                         (:shnum . 0)
                         (:shstrndx . 0))
                       'make-elf-header
                       nil))

Function: elf-header

(defun elf-header (magic class dataenc identver osabi
                         abiver padding type machine version
                         entry phoff shoff flags ehsize phentsize
                         phnum shentsize shnum shstrndx)
  (declare (xargs :guard (and (byte-listp magic)
                              (natp class)
                              (natp dataenc)
                              (natp identver)
                              (natp osabi)
                              (natp abiver)
                              (byte-listp padding)
                              (natp type)
                              (natp machine)
                              (natp version)
                              (natp entry)
                              (natp phoff)
                              (natp shoff)
                              (natp flags)
                              (natp ehsize)
                              (natp phentsize)
                              (natp phnum)
                              (natp shentsize)
                              (natp shnum)
                              (natp shstrndx))))
  (declare (xargs :guard t))
  (let ((__function__ 'elf-header))
    (declare (ignorable __function__))
    (b* ((magic (mbe :logic (acl2::byte-list-fix magic)
                     :exec magic))
         (class (mbe :logic (nfix class) :exec class))
         (dataenc (mbe :logic (nfix dataenc)
                       :exec dataenc))
         (identver (mbe :logic (nfix identver)
                        :exec identver))
         (osabi (mbe :logic (nfix osabi) :exec osabi))
         (abiver (mbe :logic (nfix abiver) :exec abiver))
         (padding (mbe :logic (acl2::byte-list-fix padding)
                       :exec padding))
         (type (mbe :logic (nfix type) :exec type))
         (machine (mbe :logic (nfix machine)
                       :exec machine))
         (version (mbe :logic (nfix version)
                       :exec version))
         (entry (mbe :logic (nfix entry) :exec entry))
         (phoff (mbe :logic (nfix phoff) :exec phoff))
         (shoff (mbe :logic (nfix shoff) :exec shoff))
         (flags (mbe :logic (nfix flags) :exec flags))
         (ehsize (mbe :logic (nfix ehsize) :exec ehsize))
         (phentsize (mbe :logic (nfix phentsize)
                         :exec phentsize))
         (phnum (mbe :logic (nfix phnum) :exec phnum))
         (shentsize (mbe :logic (nfix shentsize)
                         :exec shentsize))
         (shnum (mbe :logic (nfix shnum) :exec shnum))
         (shstrndx (mbe :logic (nfix shstrndx)
                        :exec shstrndx)))
      (list (cons 'magic magic)
            (cons 'class class)
            (cons 'dataenc dataenc)
            (cons 'identver identver)
            (cons 'osabi osabi)
            (cons 'abiver abiver)
            (cons 'padding padding)
            (cons 'type type)
            (cons 'machine machine)
            (cons 'version version)
            (cons 'entry entry)
            (cons 'phoff phoff)
            (cons 'shoff shoff)
            (cons 'flags flags)
            (cons 'ehsize ehsize)
            (cons 'phentsize phentsize)
            (cons 'phnum phnum)
            (cons 'shentsize shentsize)
            (cons 'shnum shnum)
            (cons 'shstrndx shstrndx)))))