		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-memberp

Check a structure pointer member expression [C17:6.5.2.3].

Signature
(check-memberp target-expr target-etype name tagenv) → etype
Arguments: target-expr — Guard (exprp target-expr).; target-etype — Guard (expr-typep target-etype).; name — Guard (identp name).; tagenv — Guard (tag-envp tagenv).
Returns: etype — Type (expr-type-resultp etype).

We ensure that the target has a pointer type to a structure type. We perform array-to-pointer conversion on this type, prior to ensuring it is a pointer to structure, as an array type would become a pointer type via that conversion. We look up the structure type and its member. We return the member type, with the lvalue flag set.

Definitions and Theorems

Function: check-memberp

(defun check-memberp (target-expr target-etype name tagenv)
 (declare (xargs :guard (and (exprp target-expr)
                             (expr-typep target-etype)
                             (identp name)
                             (tag-envp tagenv))))
 (let ((__function__ 'check-memberp))
  (declare (ignorable __function__))
  (b*
   ((target-type (expr-type->type target-etype))
    (target-type (apconvert-type target-type))
    ((unless (type-case target-type :pointer))
     (reserrf
         (list :arrow-operator-not-pointer (expr-fix target-expr))))
    (type (type-pointer->to target-type))
    ((unless (type-case type :struct))
     (reserrf (list :arrow-operator-not-pointer-to-struct
                    (expr-fix target-expr))))
    (tag (type-struct->tag type))
    ((okf memtype)
     (struct-member-lookup tag name tagenv)))
   (make-expr-type :type memtype
                   :lvalue t))))

Theorem: expr-type-resultp-of-check-memberp

(defthm expr-type-resultp-of-check-memberp
  (b* ((etype (check-memberp target-expr target-etype name tagenv)))
    (expr-type-resultp etype))
  :rule-classes :rewrite)

Theorem: check-memberp-of-expr-fix-target-expr

(defthm check-memberp-of-expr-fix-target-expr
  (equal (check-memberp (expr-fix target-expr)
                        target-etype name tagenv)
         (check-memberp target-expr target-etype name tagenv)))

Theorem: check-memberp-expr-equiv-congruence-on-target-expr

(defthm check-memberp-expr-equiv-congruence-on-target-expr
  (implies
       (expr-equiv target-expr target-expr-equiv)
       (equal (check-memberp target-expr target-etype name tagenv)
              (check-memberp target-expr-equiv
                             target-etype name tagenv)))
  :rule-classes :congruence)

Theorem: check-memberp-of-expr-type-fix-target-etype

(defthm check-memberp-of-expr-type-fix-target-etype
  (equal (check-memberp target-expr (expr-type-fix target-etype)
                        name tagenv)
         (check-memberp target-expr target-etype name tagenv)))

Theorem: check-memberp-expr-type-equiv-congruence-on-target-etype

(defthm check-memberp-expr-type-equiv-congruence-on-target-etype
  (implies
       (expr-type-equiv target-etype target-etype-equiv)
       (equal (check-memberp target-expr target-etype name tagenv)
              (check-memberp target-expr
                             target-etype-equiv name tagenv)))
  :rule-classes :congruence)

Theorem: check-memberp-of-ident-fix-name

(defthm check-memberp-of-ident-fix-name
  (equal (check-memberp target-expr
                        target-etype (ident-fix name)
                        tagenv)
         (check-memberp target-expr target-etype name tagenv)))

Theorem: check-memberp-ident-equiv-congruence-on-name

(defthm check-memberp-ident-equiv-congruence-on-name
  (implies
       (ident-equiv name name-equiv)
       (equal (check-memberp target-expr target-etype name tagenv)
              (check-memberp target-expr
                             target-etype name-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-memberp-of-tag-env-fix-tagenv

(defthm check-memberp-of-tag-env-fix-tagenv
  (equal (check-memberp target-expr
                        target-etype name (tag-env-fix tagenv))
         (check-memberp target-expr target-etype name tagenv)))

Theorem: check-memberp-tag-env-equiv-congruence-on-tagenv

(defthm check-memberp-tag-env-equiv-congruence-on-tagenv
  (implies
       (tag-env-equiv tagenv tagenv-equiv)
       (equal (check-memberp target-expr target-etype name tagenv)
              (check-memberp target-expr
                             target-etype name tagenv-equiv)))
  :rule-classes :congruence)