		Search-engine friendly clone of the ACL2 documentation.

Segmentation

Eas-to-las

Translate a sequence of contiguous effective addresses to linear addresses.

Signature
(eas-to-las proc-mode n eff-addr seg-reg x86) → (mv flg lin-addrs)
Arguments: n — Guard (natp n).
Returns: lin-addrs — A nil-terminated list of i64ps.

The contiguous effective addresses are eff-addr through eff-addr + n - 1. These effective addresses are translated in increasing order. When the translation of an effective address fails, the recursion stops and the error flag is returned.

Definitions and Theorems

Function: eas-to-las

(defun eas-to-las
       (proc-mode n eff-addr seg-reg x86)
       (declare (xargs :stobjs (x86)))
       (declare (type (integer 0 4) proc-mode)
                (type (signed-byte 64) eff-addr)
                (type (integer 0 5) seg-reg))
       (declare (xargs :guard (natp n)))
       (let ((__function__ 'eas-to-las))
            (declare (ignorable __function__))
            (if (zp n)
                (mv nil nil)
                (b* (((mv flg lin-addr)
                      (ea-to-la proc-mode eff-addr seg-reg 1 x86))
                     ((when flg) (mv flg nil))
                     (eff-addr+1 (i64 (1+ eff-addr)))
                     ((mv flg lin-addrs)
                      (eas-to-las proc-mode (1- n)
                                  eff-addr+1 seg-reg x86))
                     ((when flg) (mv flg nil)))
                    (mv nil (cons lin-addr lin-addrs))))))