		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-memberp

Validate a member pointer expression, given the type of the sub-expression.

Signature
(valid-memberp expr type-arg) → (mv erp type)
Arguments: expr — Guard (exprp expr).; type-arg — Guard (typep type-arg).
Returns: erp — Type (maybe-msgp erp).; type — Type (typep type).

The type of the sub-expression is calculated (recursively) by valid-expr.

The argument type must be a pointer to a structure or union type [C17:6.5.2.3/2]. We perform array-to-pointer conversion, then check that the type is a pointer to a struct type. As we refine our type system, we will eventually check that the struct type has a member of the name being accessed. We do not conver functions to pointers, because that would result into a pointer to function, which is not a pointer to structure or union as required; thus, by leaving function types unchanged, we reject them here.

Since we cannot yet look up members in structure and union types, we return the unknown type.

Definitions and Theorems

Function: valid-memberp

(defun valid-memberp (expr type-arg)
 (declare (xargs :guard (and (exprp expr) (typep type-arg))))
 (declare (xargs :guard (expr-case expr :memberp)))
 (b*
  (((reterr) (irr-type))
   ((when (type-case type-arg :unknown))
    (retok (type-unknown)))
   (type (type-apconvert type-arg))
   ((unless (and (type-case type :pointer)
                 (or (type-case (type-pointer->to type)
                                :unknown)
                     (type-case (type-pointer->to type)
                                :struct))))
    (retmsg$
     "In the member pointer expression ~x0, ~
                  the sub-expression has type ~x1."
     (expr-fix expr)
     (type-fix type-arg))))
  (retok (type-unknown))))

Theorem: maybe-msgp-of-valid-memberp.erp

(defthm maybe-msgp-of-valid-memberp.erp
  (b* (((mv acl2::?erp ?type)
        (valid-memberp expr type-arg)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: typep-of-valid-memberp.type

(defthm typep-of-valid-memberp.type
  (b* (((mv acl2::?erp ?type)
        (valid-memberp expr type-arg)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-memberp-of-expr-fix-expr

(defthm valid-memberp-of-expr-fix-expr
  (equal (valid-memberp (expr-fix expr) type-arg)
         (valid-memberp expr type-arg)))

Theorem: valid-memberp-expr-equiv-congruence-on-expr

(defthm valid-memberp-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (valid-memberp expr type-arg)
                  (valid-memberp expr-equiv type-arg)))
  :rule-classes :congruence)

Theorem: valid-memberp-of-type-fix-type-arg

(defthm valid-memberp-of-type-fix-type-arg
  (equal (valid-memberp expr (type-fix type-arg))
         (valid-memberp expr type-arg)))

Theorem: valid-memberp-type-equiv-congruence-on-type-arg

(defthm valid-memberp-type-equiv-congruence-on-type-arg
  (implies (type-equiv type-arg type-arg-equiv)
           (equal (valid-memberp expr type-arg)
                  (valid-memberp expr type-arg-equiv)))
  :rule-classes :congruence)