		Search-engine friendly clone of the ACL2 documentation.

Elf-section-header

Elf-section-header-p

Recognizer for elf-section-header structures.

Signature
(elf-section-header-p x) → *

Definitions and Theorems

Function: elf-section-header-p

(defun elf-section-header-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'elf-section-header-p))
  (declare (ignorable __function__))
  (and
     (mbe :logic
          (and (alistp x)
               (equal (strip-cars x)
                      '(name-str name type flags addr offset
                                 size link info addralign entsize)))
          :exec (fty::alist-with-carsp
                     x
                     '(name-str name type flags addr offset
                                size link info addralign entsize)))
     (b* ((name-str (cdr (std::da-nth 0 x)))
          (name (cdr (std::da-nth 1 x)))
          (type (cdr (std::da-nth 2 x)))
          (flags (cdr (std::da-nth 3 x)))
          (addr (cdr (std::da-nth 4 x)))
          (offset (cdr (std::da-nth 5 x)))
          (size (cdr (std::da-nth 6 x)))
          (link (cdr (std::da-nth 7 x)))
          (info (cdr (std::da-nth 8 x)))
          (addralign (cdr (std::da-nth 9 x)))
          (entsize (cdr (std::da-nth 10 x))))
       (and (stringp name-str)
            (natp name)
            (natp type)
            (natp flags)
            (natp addr)
            (natp offset)
            (natp size)
            (natp link)
            (natp info)
            (natp addralign)
            (natp entsize))))))

Theorem: consp-when-elf-section-header-p

(defthm consp-when-elf-section-header-p
  (implies (elf-section-header-p x)
           (consp x))
  :rule-classes :compound-recognizer)