		Search-engine friendly clone of the ACL2 documentation.

Mach-o-section-header

Make-mach-o-section-header

Basic constructor macro for mach-o-section-header structures.

Syntax

(make-mach-o-section-header [:sectname <sectname>] 
                            [:segname <segname>] 
                            [:addr <addr>] 
                            [:size <size>] 
                            [:offset <offset>] 
                            [:align <align>] 
                            [:reloff <reloff>] 
                            [:nreloc <nreloc>] 
                            [:flags <flags>] 
                            [:reserved1 <reserved1>] 
                            [:reserved2 <reserved2>] 
                            [:reserved3 <reserved3>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-mach-o-section-header

(defmacro make-mach-o-section-header (&rest args)
  (std::make-aggregate 'mach-o-section-header
                       args
                       '((:sectname . "")
                         (:segname . "")
                         (:addr . 0)
                         (:size . 0)
                         (:offset . 0)
                         (:align . 0)
                         (:reloff . 0)
                         (:nreloc . 0)
                         (:flags . 0)
                         (:reserved1 . 0)
                         (:reserved2 . 0)
                         (:reserved3 . 0))
                       'make-mach-o-section-header
                       nil))

Function: mach-o-section-header

(defun mach-o-section-header
       (sectname segname
                 addr size offset align reloff nreloc
                 flags reserved1 reserved2 reserved3)
  (declare (xargs :guard (and (stringp sectname)
                              (stringp segname)
                              (natp addr)
                              (natp size)
                              (natp offset)
                              (natp align)
                              (natp reloff)
                              (natp nreloc)
                              (natp flags)
                              (natp reserved1)
                              (natp reserved2)
                              (natp reserved3))))
  (declare (xargs :guard t))
  (let ((__function__ 'mach-o-section-header))
    (declare (ignorable __function__))
    (b* ((sectname (mbe :logic (acl2::str-fix sectname)
                        :exec sectname))
         (segname (mbe :logic (acl2::str-fix segname)
                       :exec segname))
         (addr (mbe :logic (nfix addr) :exec addr))
         (size (mbe :logic (nfix size) :exec size))
         (offset (mbe :logic (nfix offset) :exec offset))
         (align (mbe :logic (nfix align) :exec align))
         (reloff (mbe :logic (nfix reloff) :exec reloff))
         (nreloc (mbe :logic (nfix nreloc) :exec nreloc))
         (flags (mbe :logic (nfix flags) :exec flags))
         (reserved1 (mbe :logic (nfix reserved1)
                         :exec reserved1))
         (reserved2 (mbe :logic (nfix reserved2)
                         :exec reserved2))
         (reserved3 (mbe :logic (nfix reserved3)
                         :exec reserved3)))
      (list (cons 'sectname sectname)
            (cons 'segname segname)
            (cons 'addr addr)
            (cons 'size size)
            (cons 'offset offset)
            (cons 'align align)
            (cons 'reloff reloff)
            (cons 'nreloc nreloc)
            (cons 'flags flags)
            (cons 'reserved1 reserved1)
            (cons 'reserved2 reserved2)
            (cons 'reserved3 reserved3)))))