		Search-engine friendly clone of the ACL2 documentation.

Elf64-segment-header

Make-elf64-segment-header

Basic constructor macro for elf64-segment-header structures.

Syntax

(make-elf64-segment-header [:type <type>] 
                           [:flags <flags>] 
                           [:offset <offset>] 
                           [:vaddr <vaddr>] 
                           [:paddr <paddr>] 
                           [:filesz <filesz>] 
                           [:memsz <memsz>] 
                           [:align <align>])

This is the usual way to construct elf64-segment-header structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-elf64-segment-header

(defmacro make-elf64-segment-header (&rest args)
  (std::make-aggregate 'elf64-segment-header
                       args
                       '((:type . 0)
                         (:flags . 0)
                         (:offset . 0)
                         (:vaddr . 0)
                         (:paddr . 0)
                         (:filesz . 0)
                         (:memsz . 0)
                         (:align . 0))
                       'make-elf64-segment-header
                       nil))

Function: elf64-segment-header

(defun elf64-segment-header
       (type flags
             offset vaddr paddr filesz memsz align)
  (declare (xargs :guard (and (natp type)
                              (natp flags)
                              (natp offset)
                              (natp vaddr)
                              (natp paddr)
                              (natp filesz)
                              (natp memsz)
                              (natp align))))
  (declare (xargs :guard t))
  (let ((__function__ 'elf64-segment-header))
    (declare (ignorable __function__))
    (b* ((type (mbe :logic (nfix type) :exec type))
         (flags (mbe :logic (nfix flags) :exec flags))
         (offset (mbe :logic (nfix offset) :exec offset))
         (vaddr (mbe :logic (nfix vaddr) :exec vaddr))
         (paddr (mbe :logic (nfix paddr) :exec paddr))
         (filesz (mbe :logic (nfix filesz) :exec filesz))
         (memsz (mbe :logic (nfix memsz) :exec memsz))
         (align (mbe :logic (nfix align) :exec align)))
      (list (cons 'type type)
            (cons 'flags flags)
            (cons 'offset offset)
            (cons 'vaddr vaddr)
            (cons 'paddr paddr)
            (cons 'filesz filesz)
            (cons 'memsz memsz)
            (cons 'align align)))))