		Search-engine friendly clone of the ACL2 documentation.

Elf64_sym-info

Make-elf64_sym-info

Basic constructor macro for elf64_sym-info structures.

Syntax

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

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-elf64_sym-info

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

Function: elf64_sym-info

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