		Search-engine friendly clone of the ACL2 documentation.

Bigmem

Get-mem

Get the entire contents of the memory in the form of a linear list

Signature
(get-mem mem) → memlist
Arguments: mem — Guard (memp mem).
Returns: memlist — Type (acl2::unsigned-byte-listp 8 memlist), given (memp mem).

Definitions and Theorems

Function: get-mem

(defun
     get-mem (mem)
     (declare (xargs :stobjs (mem)))
     (declare (xargs :guard (memp mem)))
     (declare (xargs :non-executable t))
     (prog2$ (acl2::throw-nonexec-error 'get-mem
                                        (list mem))
             (let ((__function__ 'get-mem))
                  (declare (ignorable __function__))
                  (acl2::rev (get-mem-aux (1- (expt 2 64)) mem)))))

Theorem: return-type-of-get-mem

(defthm return-type-of-get-mem
        (implies (memp mem)
                 (b* ((memlist (get-mem mem)))
                     (acl2::unsigned-byte-listp 8 memlist)))
        :rule-classes :rewrite)

Theorem: rewrite-read-mem-to-nth-of-get-mem

(defthm rewrite-read-mem-to-nth-of-get-mem
        (implies (and (unsigned-byte-p 64 i) (memp mem))
                 (equal (read-mem i mem)
                        (nth i (get-mem mem)))))

Theorem: get-mem-after-write-mem

(defthm get-mem-after-write-mem
        (implies (unsigned-byte-p 64 i)
                 (equal (get-mem (write-mem i v mem))
                        (update-nth i (loghead 8 v)
                                    (get-mem mem)))))