		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

!seg-visiblei-from-alist

Update visible portion of segment registers as dictated by seg-visible-alist, which is required to be a seg-visiblei-alistp.

Signature
(!seg-visiblei-from-alist seg-visible-alist x86) → x86

Definitions and Theorems

Function: !seg-visiblei-from-alist

(defun !seg-visiblei-from-alist (seg-visible-alist x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (seg-visiblei-alistp seg-visible-alist)))
  (let ((__function__ '!seg-visiblei-from-alist))
    (declare (ignorable __function__))
    (cond ((endp seg-visible-alist) x86)
          (t (let ((x86 (!seg-visiblei (caar seg-visible-alist)
                                       (cdar seg-visible-alist)
                                       x86)))
               (!seg-visiblei-from-alist (cdr seg-visible-alist)
                                         x86))))))

Theorem: x86p-!seg-visiblei-from-alist

(defthm x86p-!seg-visiblei-from-alist
  (implies (and (seg-visiblei-alistp alist)
                (x86p x86))
           (x86p (!seg-visiblei-from-alist alist x86))))