		Search-engine friendly clone of the ACL2 documentation.

Missing-parents

Atc-object-designator-rules

Rules about object designators.

The first rule serves to handle access to static objects. We need to reduce objdesign-of-var, which arises when opening exec-ident, to the object designator of the static object, under the hypothesis that read-static-var on that variable yields a value and that the variable is not in automatic storage.

The second and third rules are used in the defstruct-specific theorems generated for symbolic execution of array member accesses.

The remaining rules are used in the modular proofs aboud variables in symbol tables.

The constant that collects the rules also includes some rules proved elsewhere.

Definitions and Theorems

Theorem: objdesign-of-var-when-static

(defthm objdesign-of-var-when-static
  (implies (and (valuep (read-static-var id compst))
                (not (var-autop id compst)))
           (equal (objdesign-of-var id compst)
                  (objdesign-static id))))

Theorem: not-nil-when-objdesignp

(defthm not-nil-when-objdesignp
  (implies (objdesignp x) x)
  :rule-classes :compound-recognizer)

Theorem: read-object-of-objdesign-member

(defthm read-object-of-objdesign-member
  (implies
       (and (valuep (read-object objdes compst))
            (value-case (read-object objdes compst)
                        :struct))
       (equal (read-object (objdesign-member objdes mem)
                           compst)
              (value-struct-read mem (read-object objdes compst)))))

Theorem: objdesign-of-var-of-add-var-iff

(defthm objdesign-of-var-of-add-var-iff
  (iff (objdesign-of-var var (add-var var2 val compst))
       (or (equal (ident-fix var) (ident-fix var2))
           (objdesign-of-var var compst))))

Theorem: objdesign-of-var-of-enter-scope-iff

(defthm objdesign-of-var-of-enter-scope-iff
  (implies (> (compustate-frames-number compst) 0)
           (iff (objdesign-of-var var (enter-scope compst))
                (objdesign-of-var var compst))))

Theorem: read-object-of-objdesign-of-var-of-add-var

(defthm read-object-of-objdesign-of-var-of-add-var
 (implies
  (objdesign-of-var var (add-var var2 val compst))
  (equal
       (read-object (objdesign-of-var var (add-var var2 val compst))
                    (add-var var2 val compst))
       (if (equal (ident-fix var2) (ident-fix var))
           (remove-flexible-array-member val)
         (read-object (objdesign-of-var var compst)
                      compst)))))

Theorem: read-object-of-objdesign-of-var-of-enter-scope

(defthm read-object-of-objdesign-of-var-of-enter-scope
 (implies
     (and (> (compustate-frames-number compst) 0)
          (objdesign-of-var var (enter-scope compst)))
     (equal (read-object (objdesign-of-var var (enter-scope compst))
                         (enter-scope compst))
            (read-object (objdesign-of-var var compst)
                         compst))))