• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
        • Elf-reader
          • Elf64_sym
          • Elf32_sym
          • Elf-header
            • Elf-header-fix
            • Make-elf-header
            • Elf-header-p
            • Change-elf-header
            • Elf-header-equiv
            • Elf-header->version
            • Elf-header->shstrndx
            • Elf-header->shentsize
            • Elf-header->phentsize
            • Elf-header->padding
            • Elf-header->magic
            • Elf-header->machine
            • Elf-header->identver
            • Elf-header->ehsize
            • Elf-header->dataenc
            • Elf-header->abiver
            • Elf-header->type
            • Elf-header->shoff
            • Elf-header->shnum
            • Elf-header->phoff
            • Elf-header->phnum
            • Elf-header->osabi
            • Elf-header->flags
            • Elf-header->entry
            • Elf-header->class
          • Elf-section-header
          • Elf64-segment-header
          • Elf32-segment-header
          • Elf_bits32
          • Elf_bits8
          • Elf_bits64
          • Elf_bits16
          • Section-info
          • Read-section-headers
          • Read-segment-headers-64
          • Read-segment-headers-32
          • Read-section-names
          • Elf64_sym-info
          • Elf32_sym-info
          • Read-elf-header
          • Parse-symtab-entries
          • Populate-elf-contents
          • Is-elf-content-p
          • Get-string-section-data
          • Get-section-info1
          • Set-elf-stobj-fields
          • Get-named-section-headers
          • Elf-read-mem-null-term
          • Get-section-info
          • Get-symtab-entries
          • Find-label-address-from-elf-symtab-info
          • Section-names
          • Populate-elf
          • Get-label-addresses
          • Elf-read-string-null-term
          • Get-label-address
          • Good-elf-p
          • Elf64_sym-equiv-under-mask
          • Elf64-segment-headers
          • Elf32_sym-equiv-under-mask
          • Elf32-segment-headers
          • Section-info-list
          • Elf64_sym-info-list
          • Elf32_sym-info-list
          • Elf-section-headers
          • Elf64_sym-debug
          • Elf32_sym-debug
        • Mach-o-reader
        • Merge-first-split-bytes
        • Split-bytes
        • Take-till-zero
        • Charlist->bytes
        • Merge-bytes
        • Bytes->charlist
        • String->bytes
        • Bytes->string
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Elf-reader

Elf-header

This is a product type introduced by defprod.

Fields
magic — ACL2::byte-list
class — natp
dataenc — natp
identver — natp
osabi — natp
abiver — natp
padding — ACL2::byte-list
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 — natp

Subtopics

Elf-header-fix
Fixing function for elf-header structures.
Make-elf-header
Basic constructor macro for elf-header structures.
Elf-header-p
Recognizer for elf-header structures.
Change-elf-header
Modifying constructor for elf-header structures.
Elf-header-equiv
Basic equivalence relation for elf-header structures.
Elf-header->version
Get the version field from a elf-header.
Elf-header->shstrndx
Get the shstrndx field from a elf-header.
Elf-header->shentsize
Get the shentsize field from a elf-header.
Elf-header->phentsize
Get the phentsize field from a elf-header.
Elf-header->padding
Get the padding field from a elf-header.
Elf-header->magic
Get the magic field from a elf-header.
Elf-header->machine
Get the machine field from a elf-header.
Elf-header->identver
Get the identver field from a elf-header.
Elf-header->ehsize
Get the ehsize field from a elf-header.
Elf-header->dataenc
Get the dataenc field from a elf-header.
Elf-header->abiver
Get the abiver field from a elf-header.
Elf-header->type
Get the type field from a elf-header.
Elf-header->shoff
Get the shoff field from a elf-header.
Elf-header->shnum
Get the shnum field from a elf-header.
Elf-header->phoff
Get the phoff field from a elf-header.
Elf-header->phnum
Get the phnum field from a elf-header.
Elf-header->osabi
Get the osabi field from a elf-header.
Elf-header->flags
Get the flags field from a elf-header.
Elf-header->entry
Get the entry field from a elf-header.
Elf-header->class
Get the class field from a elf-header.