		Search-engine friendly clone of the ACL2 documentation.

States64

Read64-pc

Read the program counter.

Signature
(read64-pc stat) → pc
Arguments: stat — Guard (state64p stat).
Returns: pc — Type (ubyte64p pc).

The result is an unsigned 64-bit integer, read directly from the register.

Definitions and Theorems

Function: read64-pc

(defun read64-pc (stat)
  (declare (xargs :guard (state64p stat)))
  (let ((__function__ 'read64-pc))
    (declare (ignorable __function__))
    (state64->pc stat)))

Theorem: ubyte64p-of-read64-pc

(defthm ubyte64p-of-read64-pc
  (b* ((pc (read64-pc stat)))
    (ubyte64p pc))
  :rule-classes :rewrite)

Theorem: read64-pc-of-state64-fix-stat

(defthm read64-pc-of-state64-fix-stat
  (equal (read64-pc (state64-fix stat))
         (read64-pc stat)))

Theorem: read64-pc-state64-equiv-congruence-on-stat

(defthm read64-pc-state64-equiv-congruence-on-stat
  (implies (state64-equiv stat stat-equiv)
           (equal (read64-pc stat)
                  (read64-pc stat-equiv)))
  :rule-classes :congruence)