		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-cast

Check a cast expression [C17:6.5.4].

Signature
(check-cast arg-expr arg-etype tyname tagenv) → etype
Arguments: arg-expr — Guard (exprp arg-expr).; arg-etype — Guard (expr-typep arg-etype).; tyname — Guard (tynamep tyname).; tagenv — Guard (tag-envp tagenv).
Returns: etype — Type (expr-type-resultp etype).

A cast is allowed between scalar types. The result has the type indicated in the cast. See [C17:6.5.4]; note that the additional requirements on the type do not apply to our currently simplified model of C types. We apply lvalue conversion to the operand. We also apply array-to-pointer conversion, which could turn an array into a pointer (and thus scalar) type. A cast expression is never an lvalue.

Definitions and Theorems

Function: check-cast

(defun check-cast (arg-expr arg-etype tyname tagenv)
  (declare (xargs :guard (and (exprp arg-expr)
                              (expr-typep arg-etype)
                              (tynamep tyname)
                              (tag-envp tagenv))))
  (let ((__function__ 'check-cast))
    (declare (ignorable __function__))
    (b* ((arg-type (expr-type->type arg-etype))
         (arg-type (apconvert-type arg-type))
         ((unless (type-scalarp arg-type))
          (reserrf (list :cast-mistype-operand (expr-fix arg-expr)
                         :required :scalar
                         :supplied arg-type)))
         ((okf type)
          (check-tyname tyname tagenv))
         ((unless (type-scalarp type))
          (reserrf (list :cast-mistype-type (expr-fix arg-expr)
                         :required :scalar
                         :supplied type))))
      (make-expr-type :type type
                      :lvalue nil))))

Theorem: expr-type-resultp-of-check-cast

(defthm expr-type-resultp-of-check-cast
  (b* ((etype (check-cast arg-expr arg-etype tyname tagenv)))
    (expr-type-resultp etype))
  :rule-classes :rewrite)

Theorem: check-cast-of-expr-fix-arg-expr

(defthm check-cast-of-expr-fix-arg-expr
  (equal (check-cast (expr-fix arg-expr)
                     arg-etype tyname tagenv)
         (check-cast arg-expr arg-etype tyname tagenv)))

Theorem: check-cast-expr-equiv-congruence-on-arg-expr

(defthm check-cast-expr-equiv-congruence-on-arg-expr
  (implies (expr-equiv arg-expr arg-expr-equiv)
           (equal (check-cast arg-expr arg-etype tyname tagenv)
                  (check-cast arg-expr-equiv
                              arg-etype tyname tagenv)))
  :rule-classes :congruence)

Theorem: check-cast-of-expr-type-fix-arg-etype

(defthm check-cast-of-expr-type-fix-arg-etype
  (equal (check-cast arg-expr (expr-type-fix arg-etype)
                     tyname tagenv)
         (check-cast arg-expr arg-etype tyname tagenv)))

Theorem: check-cast-expr-type-equiv-congruence-on-arg-etype

(defthm check-cast-expr-type-equiv-congruence-on-arg-etype
  (implies (expr-type-equiv arg-etype arg-etype-equiv)
           (equal (check-cast arg-expr arg-etype tyname tagenv)
                  (check-cast arg-expr
                              arg-etype-equiv tyname tagenv)))
  :rule-classes :congruence)

Theorem: check-cast-of-tyname-fix-tyname

(defthm check-cast-of-tyname-fix-tyname
  (equal (check-cast arg-expr arg-etype (tyname-fix tyname)
                     tagenv)
         (check-cast arg-expr arg-etype tyname tagenv)))

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

(defthm check-cast-tyname-equiv-congruence-on-tyname
  (implies (tyname-equiv tyname tyname-equiv)
           (equal (check-cast arg-expr arg-etype tyname tagenv)
                  (check-cast arg-expr
                              arg-etype tyname-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-cast-of-tag-env-fix-tagenv

(defthm check-cast-of-tag-env-fix-tagenv
  (equal (check-cast arg-expr
                     arg-etype tyname (tag-env-fix tagenv))
         (check-cast arg-expr arg-etype tyname tagenv)))

Theorem: check-cast-tag-env-equiv-congruence-on-tagenv

(defthm check-cast-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-cast arg-expr arg-etype tyname tagenv)
                  (check-cast arg-expr
                              arg-etype tyname tagenv-equiv)))
  :rule-classes :congruence)