		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Apconvert-expr-value

Array-to-pointer conversion [C17:6.3.2.1/3] on expression values.

Signature
(apconvert-expr-value eval) → eval1
Arguments: eval — Guard (expr-valuep eval).
Returns: eval1 — Type (expr-value-resultp eval1).

Under most circumstances, an array is converted to a pointer to the first element of the array [C17:6.3.2.1/3]; indeed, arrays are used like pointers most of the time.

This cannot be formalized on values: we need expression values, because we need to know where the array is in storage (i.e. we need to know its object designator), so that we can construct a pointer to it. Non-array expression values are left unchanged. If the array has no object designator, we return an error; this should only happen for arrays with temporary lifetime [C17:6.2.4/8], which are currently not part of our C subset.

We make a slight approximation for now: instead of returning a pointer to the first element of the array, we return a pointer to the array. This is adequate in our current formalization of our C subset, because of the way we formalize array indexing (e.g. see exec-arrsub); however, we plan to make this, and array indexing, consistent with full C.

The static counterpart of this is apconvert-type.

Definitions and Theorems

Function: apconvert-expr-value

(defun apconvert-expr-value (eval)
 (declare (xargs :guard (expr-valuep eval)))
 (let ((__function__ 'apconvert-expr-value))
  (declare (ignorable __function__))
  (b* (((expr-value eval) eval))
   (if
    (value-case eval.value :array)
    (if eval.object
      (make-expr-value
           :value (make-value-pointer
                       :core (pointer-valid eval.object)
                       :reftype (value-array->elemtype eval.value))
           :object nil)
     (error (list :array-without-designator (expr-value-fix eval))))
    (expr-value-fix eval)))))

Theorem: expr-value-resultp-of-apconvert-expr-value

(defthm expr-value-resultp-of-apconvert-expr-value
  (b* ((eval1 (apconvert-expr-value eval)))
    (expr-value-resultp eval1))
  :rule-classes :rewrite)

Theorem: apconvert-expr-value-when-not-array

(defthm apconvert-expr-value-when-not-array
  (implies (not (equal (value-kind (expr-value->value eval))
                       :array))
           (equal (apconvert-expr-value eval)
                  (expr-value-fix eval))))

Theorem: apconvert-expr-value-of-expr-value-fix-eval

(defthm apconvert-expr-value-of-expr-value-fix-eval
  (equal (apconvert-expr-value (expr-value-fix eval))
         (apconvert-expr-value eval)))

Theorem: apconvert-expr-value-expr-value-equiv-congruence-on-eval

(defthm apconvert-expr-value-expr-value-equiv-congruence-on-eval
  (implies (expr-value-equiv eval eval-equiv)
           (equal (apconvert-expr-value eval)
                  (apconvert-expr-value eval-equiv)))
  :rule-classes :congruence)