• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
    • Axe
    • Execloader
      • Elf-reader
      • Mach-o-reader
        • Read-load_commands
        • Read-section_data_sz_structures
        • Mach-o-section-header
        • Mach-o-header
          • Mach-o-header-fix
          • Make-mach-o-header
          • Mach-o-header-equiv
          • Mach-o-header-p
          • Change-mach-o-header
          • Mach-o-header->reserved
          • Mach-o-header->sizeofcmds
          • Mach-o-header->filetype
          • Mach-o-header->cputype
          • Mach-o-header->cpusubtype
          • Mach-o-header->ncmds
          • Mach-o-header->magic
          • Mach-o-header->flags
        • Populate-mach-o-contents
        • Good-mach-o-p
        • Fill-data-segment-bytes
        • Fill-text-text-section-bytes
        • Fill-text-segment-bytes
        • Fill-text-cstring-section-bytes
        • Fill-text-const-section-bytes
        • Fill-data-dyld-section-bytes
        • Fill-data-data-section-bytes
        • Fill-data-const-section-bytes
        • Fill-data-common-section-bytes
        • Fill-data-bss-section-bytes
        • Read-mach_header
        • Populate-mach-o
        • Mach-o-section-headers
      • Merge-first-split-bytes
      • Split-bytes
      • Take-till-zero
      • Charlist->bytes
      • Merge-bytes
      • Bytes->charlist
      • String->bytes
      • Bytes->string
  • Math
  • Testing-utilities

• Mach-o-header

Make-mach-o-header

Basic constructor macro for mach-o-header structures.

Syntax

(make-mach-o-header [:magic <magic>] 
                    [:cputype <cputype>] 
                    [:cpusubtype <cpusubtype>] 
                    [:filetype <filetype>] 
                    [:ncmds <ncmds>] 
                    [:sizeofcmds <sizeofcmds>] 
                    [:flags <flags>] 
                    [:reserved <reserved>]) 

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-mach-o-header

(defmacro make-mach-o-header (&rest args)
  (std::make-aggregate 'mach-o-header
                       args
                       '((:magic . 0)
                         (:cputype . 0)
                         (:cpusubtype . 0)
                         (:filetype . 0)
                         (:ncmds . 0)
                         (:sizeofcmds . 0)
                         (:flags . 0)
                         (:reserved quote nil))
                       'make-mach-o-header
                       nil))

Function: mach-o-header

(defun mach-o-header (magic cputype cpusubtype filetype
                            ncmds sizeofcmds flags reserved)
  (declare (xargs :guard (and (natp magic)
                              (natp cputype)
                              (natp cpusubtype)
                              (natp filetype)
                              (natp ncmds)
                              (natp sizeofcmds)
                              (natp flags)
                              (acl2::maybe-natp reserved))))
  (declare (xargs :guard t))
  (let ((__function__ 'mach-o-header))
    (declare (ignorable __function__))
    (b* ((magic (mbe :logic (nfix magic) :exec magic))
         (cputype (mbe :logic (nfix cputype)
                       :exec cputype))
         (cpusubtype (mbe :logic (nfix cpusubtype)
                          :exec cpusubtype))
         (filetype (mbe :logic (nfix filetype)
                        :exec filetype))
         (ncmds (mbe :logic (nfix ncmds) :exec ncmds))
         (sizeofcmds (mbe :logic (nfix sizeofcmds)
                          :exec sizeofcmds))
         (flags (mbe :logic (nfix flags) :exec flags))
         (reserved (mbe :logic (acl2::maybe-natp-fix reserved)
                        :exec reserved)))
      (list (cons 'magic magic)
            (cons 'cputype cputype)
            (cons 'cpusubtype cpusubtype)
            (cons 'filetype filetype)
            (cons 'ncmds ncmds)
            (cons 'sizeofcmds sizeofcmds)
            (cons 'flags flags)
            (cons 'reserved reserved)))))