		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Objdesign->base-address

Base address of an object designator.

Signature
(objdesign->base-address objdes) → addr
Arguments: objdes — Guard (objdesignp objdes).
Returns: addr — Type (addressp addr).

We find the top-level object by recursion. If it is an address, we return it, since it is the base address. If it is a variable, for now we just return a dummy address: for now this function is only used with object designators that have addresses at the top level, so this is adequate; this will be properly generalized at some point.

Definitions and Theorems

Function: objdesign->base-address

(defun objdesign->base-address (objdes)
 (declare (xargs :guard (objdesignp objdes)))
 (let ((__function__ 'objdesign->base-address))
   (declare (ignorable __function__))
   (objdesign-case objdes
                   :static (address 0)
                   :auto (address 0)
                   :alloc objdes.get
                   :element (objdesign->base-address objdes.super)
                   :member (objdesign->base-address objdes.super))))

Theorem: addressp-of-objdesign->base-address

(defthm addressp-of-objdesign->base-address
  (b* ((addr (objdesign->base-address objdes)))
    (addressp addr))
  :rule-classes :rewrite)

Theorem: objdesign->base-address-of-objdesign-fix-objdes

(defthm objdesign->base-address-of-objdesign-fix-objdes
  (equal (objdesign->base-address (objdesign-fix objdes))
         (objdesign->base-address objdes)))

Theorem: objdesign->base-address-objdesign-equiv-congruence-on-objdes

(defthm objdesign->base-address-objdesign-equiv-congruence-on-objdes
  (implies (objdesign-equiv objdes objdes-equiv)
           (equal (objdesign->base-address objdes)
                  (objdesign->base-address objdes-equiv)))
  :rule-classes :congruence)