		Search-engine friendly clone of the ACL2 documentation.

Elf-section-header

Make-elf-section-header

Basic constructor macro for elf-section-header structures.

Syntax

(make-elf-section-header [:name-str <name-str>] 
                         [:name <name>] 
                         [:type <type>] 
                         [:flags <flags>] 
                         [:addr <addr>] 
                         [:offset <offset>] 
                         [:size <size>] 
                         [:link <link>] 
                         [:info <info>] 
                         [:addralign <addralign>] 
                         [:entsize <entsize>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-elf-section-header

(defmacro make-elf-section-header (&rest args)
  (std::make-aggregate 'elf-section-header
                       args
                       '((:name-str . "")
                         (:name . 0)
                         (:type . 0)
                         (:flags . 0)
                         (:addr . 0)
                         (:offset . 0)
                         (:size . 0)
                         (:link . 0)
                         (:info . 0)
                         (:addralign . 0)
                         (:entsize . 0))
                       'make-elf-section-header
                       nil))

Function: elf-section-header

(defun elf-section-header
       (name-str name type flags addr
                 offset size link info addralign entsize)
  (declare (xargs :guard (and (stringp name-str)
                              (natp name)
                              (natp type)
                              (natp flags)
                              (natp addr)
                              (natp offset)
                              (natp size)
                              (natp link)
                              (natp info)
                              (natp addralign)
                              (natp entsize))))
  (declare (xargs :guard t))
  (let ((__function__ 'elf-section-header))
    (declare (ignorable __function__))
    (b* ((name-str (mbe :logic (acl2::str-fix name-str)
                        :exec name-str))
         (name (mbe :logic (nfix name) :exec name))
         (type (mbe :logic (nfix type) :exec type))
         (flags (mbe :logic (nfix flags) :exec flags))
         (addr (mbe :logic (nfix addr) :exec addr))
         (offset (mbe :logic (nfix offset) :exec offset))
         (size (mbe :logic (nfix size) :exec size))
         (link (mbe :logic (nfix link) :exec link))
         (info (mbe :logic (nfix info) :exec info))
         (addralign (mbe :logic (nfix addralign)
                         :exec addralign))
         (entsize (mbe :logic (nfix entsize)
                       :exec entsize)))
      (list (cons 'name-str name-str)
            (cons 'name name)
            (cons 'type type)
            (cons 'flags flags)
            (cons 'addr addr)
            (cons 'offset offset)
            (cons 'size size)
            (cons 'link link)
            (cons 'info info)
            (cons 'addralign addralign)
            (cons 'entsize entsize)))))