• 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
          • Elf64_sym
          • Elf32_sym
          • Elf-header
          • 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
      • Math
      • Testing-utilities
    • Elf-reader

    Good-elf-p

    The preferred recognizer for the elf stobj

    Definitions and Theorems

    Function: good-elf-p

    (defun good-elf-p (elf)
      (declare (xargs :stobjs elf)
               (ignore elf))
      t)