		Search-engine friendly clone of the ACL2 documentation.

States32

Read32-pc

Read the program counter.

Signature
(read32-pc stat) → pc
Arguments: stat — Guard (state32p stat).
Returns: pc — Type (ubyte32p pc).

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

Definitions and Theorems

Function: read32-pc

(defun read32-pc (stat)
  (declare (xargs :guard (state32p stat)))
  (let ((__function__ 'read32-pc))
    (declare (ignorable __function__))
    (state32->pc stat)))

Theorem: ubyte32p-of-read32-pc

(defthm ubyte32p-of-read32-pc
  (b* ((pc (read32-pc stat)))
    (ubyte32p pc))
  :rule-classes :rewrite)

Theorem: read32-pc-of-state32-fix-stat

(defthm read32-pc-of-state32-fix-stat
  (equal (read32-pc (state32-fix stat))
         (read32-pc stat)))

Theorem: read32-pc-state32-equiv-congruence-on-stat

(defthm read32-pc-state32-equiv-congruence-on-stat
  (implies (state32-equiv stat stat-equiv)
           (equal (read32-pc stat)
                  (read32-pc stat-equiv)))
  :rule-classes :congruence)