		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-cast

Execute a type cast on an expression value.

Signature
(exec-cast tyname arg) → eval
Arguments: tyname — Guard (tynamep tyname).; arg — Guard (expr-valuep arg).
Returns: eval — Type (expr-value-resultp eval).

We perform array-to-pointer conversion [C17:5.3.2.1/3] on the operand.

Definitions and Theorems

Function: exec-cast

(defun exec-cast (tyname arg)
  (declare (xargs :guard (and (tynamep tyname)
                              (expr-valuep arg))))
  (let ((__function__ 'exec-cast))
    (declare (ignorable __function__))
    (b* ((arg (apconvert-expr-value arg))
         ((when (errorp arg)) arg)
         (val (eval-cast tyname (expr-value->value arg)))
         ((when (errorp val)) val))
      (make-expr-value :value val
                       :object nil))))

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

(defthm expr-value-resultp-of-exec-cast
  (b* ((eval (exec-cast tyname arg)))
    (expr-value-resultp eval))
  :rule-classes :rewrite)

Theorem: exec-cast-of-tyname-fix-tyname

(defthm exec-cast-of-tyname-fix-tyname
  (equal (exec-cast (tyname-fix tyname) arg)
         (exec-cast tyname arg)))

Theorem: exec-cast-tyname-equiv-congruence-on-tyname

(defthm exec-cast-tyname-equiv-congruence-on-tyname
  (implies (tyname-equiv tyname tyname-equiv)
           (equal (exec-cast tyname arg)
                  (exec-cast tyname-equiv arg)))
  :rule-classes :congruence)

Theorem: exec-cast-of-expr-value-fix-arg

(defthm exec-cast-of-expr-value-fix-arg
  (equal (exec-cast tyname (expr-value-fix arg))
         (exec-cast tyname arg)))

Theorem: exec-cast-expr-value-equiv-congruence-on-arg

(defthm exec-cast-expr-value-equiv-congruence-on-arg
  (implies (expr-value-equiv arg arg-equiv)
           (equal (exec-cast tyname arg)
                  (exec-cast tyname arg-equiv)))
  :rule-classes :congruence)