		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-member

Execute a structure member operation on an expression value.

Signature
(exec-member str mem) → eval
Arguments: str — Guard (expr-valuep str).; mem — Guard (identp mem).
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 structure (it actually makes no difference whether we make this check before or after the array-to-pointer conversion, but we maintain the uniformity of always performing the conversion). The named member must be in the structure. The value associated to the member is returned.

If the structure expression value has an object designator, we return an expression value with the object designator obtained by adding the member to the one for the structure. If there is no object designator in the input, there is none in the output.

Definitions and Theorems

Function: exec-member

(defun exec-member (str mem)
  (declare (xargs :guard (and (expr-valuep str) (identp mem))))
  (let ((__function__ 'exec-member))
    (declare (ignorable __function__))
    (b* ((str (apconvert-expr-value str))
         ((when (errorp str)) str)
         (val-str (expr-value->value str))
         ((unless (value-case val-str :struct))
          (error (list :mistype-member
                       :required :struct
                       :supplied (type-of-value val-str))))
         (val-mem (value-struct-read mem val-str))
         ((when (errorp val-mem)) val-mem)
         (objdes-str (expr-value->object str))
         (objdes-mem (and objdes-str
                          (make-objdesign-member :super objdes-str
                                                 :name mem))))
      (make-expr-value :value val-mem
                       :object objdes-mem))))

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

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

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

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

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

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

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

(defthm exec-member-of-ident-fix-mem
  (equal (exec-member str (ident-fix mem))
         (exec-member str mem)))

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

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