Initialize the MACH-O stobj with contents of MACH-O binary
(populate-mach-o filename mach-o state) → (mv alst new-mach-o state)
Function:
(defun populate-mach-o (filename mach-o state) (declare (xargs :stobjs (mach-o state))) (declare (xargs :guard (stringp filename))) (let ((__function__ 'populate-mach-o)) (declare (ignorable __function__)) (b* (((mv contents state) (acl2::read-file-bytes filename state)) ((unless (byte-listp contents)) (prog2$ (raise "Error reading file ~s0!" filename) (mv nil mach-o state)))) (populate-mach-o-contents contents mach-o state))))
Theorem:
(defthm good-mach-o-p-of-populate-mach-o.new-mach-o (implies (good-mach-o-p mach-o) (b* (((mv ?alst ?new-mach-o acl2::?state) (populate-mach-o filename mach-o state))) (good-mach-o-p new-mach-o))) :rule-classes :rewrite)