		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

!msri-from-alist

Update model-specific registers as dictated by msr-alist, which is required to be a msri-alistp.

Signature
(!msri-from-alist msr-alist x86) → x86

Definitions and Theorems

Function: !msri-from-alist

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

Theorem: x86p-!msri-from-alist

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