		Search-engine friendly clone of the ACL2 documentation.

Mach-o-header

Mach-o-header-p

Recognizer for mach-o-header structures.

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

Definitions and Theorems

Function: mach-o-header-p

(defun mach-o-header-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'mach-o-header-p))
  (declare (ignorable __function__))
  (and
   (mbe
       :logic (and (alistp x)
                   (equal (strip-cars x)
                          '(magic cputype cpusubtype filetype
                                  ncmds sizeofcmds flags reserved)))
       :exec (fty::alist-with-carsp
                  x
                  '(magic cputype cpusubtype filetype
                          ncmds sizeofcmds flags reserved)))
   (b* ((magic (cdr (std::da-nth 0 x)))
        (cputype (cdr (std::da-nth 1 x)))
        (cpusubtype (cdr (std::da-nth 2 x)))
        (filetype (cdr (std::da-nth 3 x)))
        (ncmds (cdr (std::da-nth 4 x)))
        (sizeofcmds (cdr (std::da-nth 5 x)))
        (flags (cdr (std::da-nth 6 x)))
        (reserved (cdr (std::da-nth 7 x))))
     (and (natp magic)
          (natp cputype)
          (natp cpusubtype)
          (natp filetype)
          (natp ncmds)
          (natp sizeofcmds)
          (natp flags)
          (acl2::maybe-natp reserved))))))

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

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