		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 actually never happen (at least in our model), but we need to formulate and prove an invariant saying that every array expression value includes an object designator, which at the moment we do not have.

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)))
 (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)