		Search-engine friendly clone of the ACL2 documentation.

Elf32-segment-header

Elf32-segment-header-p

Recognizer for elf32-segment-header structures.

Signature
(elf32-segment-header-p x) → *

Definitions and Theorems

Function: elf32-segment-header-p

(defun elf32-segment-header-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'elf32-segment-header-p))
  (declare (ignorable __function__))
  (and
    (mbe :logic
         (and (alistp x)
              (equal (strip-cars x)
                     '(type flags
                            offset vaddr paddr filesz memsz align)))
         :exec (fty::alist-with-carsp
                    x
                    '(type flags
                           offset vaddr paddr filesz memsz align)))
    (b* ((type (cdr (std::da-nth 0 x)))
         (flags (cdr (std::da-nth 1 x)))
         (offset (cdr (std::da-nth 2 x)))
         (vaddr (cdr (std::da-nth 3 x)))
         (paddr (cdr (std::da-nth 4 x)))
         (filesz (cdr (std::da-nth 5 x)))
         (memsz (cdr (std::da-nth 6 x)))
         (align (cdr (std::da-nth 7 x))))
      (and (natp type)
           (natp flags)
           (natp offset)
           (natp vaddr)
           (natp paddr)
           (natp filesz)
           (natp memsz)
           (natp align))))))

Theorem: consp-when-elf32-segment-header-p

(defthm consp-when-elf32-segment-header-p
  (implies (elf32-segment-header-p x)
           (consp x))
  :rule-classes :compound-recognizer)