		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-memberp

Execute a structure pointer member operation on an expression value.

Signature
(exec-memberp str mem compst) → eval
Arguments: str — Guard (expr-valuep str).; mem — Guard (identp mem).; compst — Guard (compustatep compst).
Returns: eval — Type (expr-value-resultp eval).

This is for the -> operator. We perform array-to-pointer conversion [C17:6.3.2.1/3] on the operand. The resulting operand must be a valid pointer to a structure of type consistent with the structure. The named member must be in the structure. The value associated to the member is returned.

We return an expression value whose object designator is obtained by adding the member to the object designator in the pointer.

Definitions and Theorems

Function: exec-memberp

(defun exec-memberp (str mem compst)
 (declare (xargs :guard (and (expr-valuep str)
                             (identp mem)
                             (compustatep compst))))
 (let ((__function__ 'exec-memberp))
  (declare (ignorable __function__))
  (b*
   ((str (apconvert-expr-value str))
    ((when (errorp str)) str)
    (str (expr-value->value str))
    ((unless (value-case str :pointer))
     (error (list :mistype-memberp
                  :required :pointer
                  :supplied (type-of-value str))))
    ((unless (value-pointer-validp str))
     (error (list :invalid-pointer str)))
    (objdes (value-pointer->designator str))
    (reftype (value-pointer->reftype str))
    (struct (read-object objdes compst))
    ((when (errorp struct))
     (error (list :struct-not-found
                  str (compustate-fix compst))))
    ((unless (value-case struct :struct))
     (error (list :not-struct
                  str (compustate-fix compst))))
    ((unless (equal reftype
                    (type-struct (value-struct->tag struct))))
     (error (list :mistype-struct-read
                  :pointer reftype
                  :array (type-struct (value-struct->tag struct)))))
    (val (value-struct-read mem struct))
    ((when (errorp val)) val)
    (objdes-mem (make-objdesign-member :super objdes
                                       :name mem)))
   (make-expr-value :value val
                    :object objdes-mem))))

Theorem: expr-value-resultp-of-exec-memberp

(defthm expr-value-resultp-of-exec-memberp
  (b* ((eval (exec-memberp str mem compst)))
    (expr-value-resultp eval))
  :rule-classes :rewrite)

Theorem: exec-memberp-of-expr-value-fix-str

(defthm exec-memberp-of-expr-value-fix-str
  (equal (exec-memberp (expr-value-fix str)
                       mem compst)
         (exec-memberp str mem compst)))

Theorem: exec-memberp-expr-value-equiv-congruence-on-str

(defthm exec-memberp-expr-value-equiv-congruence-on-str
  (implies (expr-value-equiv str str-equiv)
           (equal (exec-memberp str mem compst)
                  (exec-memberp str-equiv mem compst)))
  :rule-classes :congruence)

Theorem: exec-memberp-of-ident-fix-mem

(defthm exec-memberp-of-ident-fix-mem
  (equal (exec-memberp str (ident-fix mem)
                       compst)
         (exec-memberp str mem compst)))

Theorem: exec-memberp-ident-equiv-congruence-on-mem

(defthm exec-memberp-ident-equiv-congruence-on-mem
  (implies (ident-equiv mem mem-equiv)
           (equal (exec-memberp str mem compst)
                  (exec-memberp str mem-equiv compst)))
  :rule-classes :congruence)

Theorem: exec-memberp-of-compustate-fix-compst

(defthm exec-memberp-of-compustate-fix-compst
  (equal (exec-memberp str mem (compustate-fix compst))
         (exec-memberp str mem compst)))

Theorem: exec-memberp-compustate-equiv-congruence-on-compst

(defthm exec-memberp-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-memberp str mem compst)
                  (exec-memberp str mem compst-equiv)))
  :rule-classes :congruence)