• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
      • Execloader
        • Elf-reader
        • Mach-o-reader
          • Read-load_commands
          • Read-section_data_sz_structures
          • Mach-o-section-header
            • Mach-o-section-header-fix
            • Make-mach-o-section-header
            • Mach-o-section-header-equiv
            • Mach-o-section-header-p
            • Change-mach-o-section-header
            • Mach-o-section-header->sectname
            • Mach-o-section-header->reserved3
            • Mach-o-section-header->reserved2
            • Mach-o-section-header->reserved1
            • Mach-o-section-header->segname
            • Mach-o-section-header->reloff
            • Mach-o-section-header->offset
            • Mach-o-section-header->nreloc
            • Mach-o-section-header->flags
            • Mach-o-section-header->align
            • Mach-o-section-header->size
            • Mach-o-section-header->addr
          • Mach-o-header
          • Populate-mach-o-contents
          • Good-mach-o-p
          • Fill-data-segment-bytes
          • Fill-text-segment-bytes
          • Fill-text-text-section-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
        • Charlist->bytes
        • Take-till-zero
        • Merge-bytes
        • Bytes->charlist
        • Bytes->string
        • String->bytes
      • Axe
    • Testing-utilities
    • Math
  • Mach-o-reader

Mach-o-section-header

This is a product type introduced by defprod.

Fields
sectname — stringp
segname — stringp
addr — natp
size — natp
offset — natp
align — natp
reloff — natp
nreloc — natp
flags — natp
reserved1 — natp
reserved2 — natp
reserved3 — natp

Subtopics

Mach-o-section-header-fix
Fixing function for mach-o-section-header structures.
Make-mach-o-section-header
Basic constructor macro for mach-o-section-header structures.
Mach-o-section-header-equiv
Basic equivalence relation for mach-o-section-header structures.
Mach-o-section-header-p
Recognizer for mach-o-section-header structures.
Change-mach-o-section-header
Modifying constructor for mach-o-section-header structures.
Mach-o-section-header->sectname
Get the sectname field from a mach-o-section-header.
Mach-o-section-header->reserved3
Get the reserved3 field from a mach-o-section-header.
Mach-o-section-header->reserved2
Get the reserved2 field from a mach-o-section-header.
Mach-o-section-header->reserved1
Get the reserved1 field from a mach-o-section-header.
Mach-o-section-header->segname
Get the segname field from a mach-o-section-header.
Mach-o-section-header->reloff
Get the reloff field from a mach-o-section-header.
Mach-o-section-header->offset
Get the offset field from a mach-o-section-header.
Mach-o-section-header->nreloc
Get the nreloc field from a mach-o-section-header.
Mach-o-section-header->flags
Get the flags field from a mach-o-section-header.
Mach-o-section-header->align
Get the align field from a mach-o-section-header.
Mach-o-section-header->size
Get the size field from a mach-o-section-header.
Mach-o-section-header->addr
Get the addr field from a mach-o-section-header.