		Search-engine friendly clone of the ACL2 documentation.

Mach-o-section-header

Mach-o-section-header-p

Recognizer for mach-o-section-header structures.

Signature
(mach-o-section-header-p x) → *

Definitions and Theorems

Function: mach-o-section-header-p

(defun mach-o-section-header-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'mach-o-section-header-p))
  (declare (ignorable __function__))
  (and
   (mbe
       :logic
       (and (alistp x)
            (equal (strip-cars x)
                   '(sectname segname
                              addr size offset align reloff nreloc
                              flags reserved1 reserved2 reserved3)))
       :exec (fty::alist-with-carsp
                  x
                  '(sectname segname
                             addr size offset align reloff nreloc
                             flags reserved1 reserved2 reserved3)))
   (b* ((sectname (cdr (std::da-nth 0 x)))
        (segname (cdr (std::da-nth 1 x)))
        (addr (cdr (std::da-nth 2 x)))
        (size (cdr (std::da-nth 3 x)))
        (offset (cdr (std::da-nth 4 x)))
        (align (cdr (std::da-nth 5 x)))
        (reloff (cdr (std::da-nth 6 x)))
        (nreloc (cdr (std::da-nth 7 x)))
        (flags (cdr (std::da-nth 8 x)))
        (reserved1 (cdr (std::da-nth 9 x)))
        (reserved2 (cdr (std::da-nth 10 x)))
        (reserved3 (cdr (std::da-nth 11 x))))
     (and (stringp sectname)
          (stringp segname)
          (natp addr)
          (natp size)
          (natp offset)
          (natp align)
          (natp reloff)
          (natp nreloc)
          (natp flags)
          (natp reserved1)
          (natp reserved2)
          (natp reserved3))))))

Theorem: consp-when-mach-o-section-header-p

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