• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • 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
            • Elf32_sym-info-fix
            • Elf32_sym-info-equiv
            • Make-elf32_sym-info
              • Elf32_sym-info->name-str
              • Elf32_sym-info->entry
              • Change-elf32_sym-info
              • Elf32_sym-info-p
            • 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
    • Elf32_sym-info

    Make-elf32_sym-info

    Basic constructor macro for elf32_sym-info structures.

    Syntax
    (make-elf32_sym-info [:name-str <name-str>] 
                         [:entry <entry>]) 
    

    This is the usual way to construct elf32_sym-info structures. It simply conses together a structure with the specified fields.

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

    Definition

    This is an ordinary make- macro introduced by defprod.

    Macro: make-elf32_sym-info

    (defmacro make-elf32_sym-info (&rest args)
      (std::make-aggregate 'elf32_sym-info
                           args '((:name-str . "") (:entry . 0))
                           'make-elf32_sym-info
                           nil))

    Function: elf32_sym-info

    (defun elf32_sym-info (name-str entry)
      (declare (xargs :guard (and (stringp name-str)
                                  (elf32_sym-p entry))))
      (declare (xargs :guard t))
      (let ((__function__ 'elf32_sym-info))
        (declare (ignorable __function__))
        (b* ((name-str (mbe :logic (acl2::str-fix name-str)
                            :exec name-str))
             (entry (mbe :logic (elf32_sym-fix entry)
                         :exec entry)))
          (list (cons 'name-str name-str)
                (cons 'entry entry)))))