		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))))))