		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-funcall

Validate a function call expression, given the types of the sub-expressions.

Signature
(valid-funcall expr type-fun types-arg) → (mv erp type)
Arguments: expr — Guard (exprp expr).; type-fun — Guard (typep type-fun).; types-arg — Guard (type-listp types-arg).
Returns: type — Type (typep type).

After converting function types to pointer types, the first sub-expression must have pointer type [C:6.5.2.2/1]; since we currently have just one pointer type, we cannot check that it is a pointer to a function. For the same reason, we do not check the argument types against the function type [C:6.5.2.2/2]. Also for the same reason, we return the unknown type, because we do not have information about the result type.

There is no need to perform array-to-pointer conversion, because array types cannot have function element types, but only (complete) object element types [C:6.2.5/20]. Thus, the conversion could never result into a pointer to a function.

Definitions and Theorems

Function: valid-funcall

(defun valid-funcall (expr type-fun types-arg)
 (declare (xargs :guard (and (exprp expr)
                             (typep type-fun)
                             (type-listp types-arg))))
 (declare (xargs :guard (expr-case expr :funcall)))
 (let ((__function__ 'valid-funcall))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-type))
    ((when (or (type-case type-fun :unknown)
               (member-equal (type-unknown)
                             (type-list-fix types-arg))))
     (retok (type-unknown)))
    (type (type-fpconvert type-fun))
    ((unless (type-case type :pointer))
     (reterr
      (msg
       "In the function call expression ~x0, ~
                      the first sub-expression has type ~x1."
       (expr-fix expr)
       (type-fix type-fun)))))
   (retok (type-unknown)))))

Theorem: typep-of-valid-funcall.type

(defthm typep-of-valid-funcall.type
  (b* (((mv acl2::?erp ?type)
        (valid-funcall expr type-fun types-arg)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-funcall-of-expr-fix-expr

(defthm valid-funcall-of-expr-fix-expr
  (equal (valid-funcall (expr-fix expr)
                        type-fun types-arg)
         (valid-funcall expr type-fun types-arg)))

Theorem: valid-funcall-expr-equiv-congruence-on-expr

(defthm valid-funcall-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (valid-funcall expr type-fun types-arg)
                  (valid-funcall expr-equiv type-fun types-arg)))
  :rule-classes :congruence)

Theorem: valid-funcall-of-type-fix-type-fun

(defthm valid-funcall-of-type-fix-type-fun
  (equal (valid-funcall expr (type-fix type-fun)
                        types-arg)
         (valid-funcall expr type-fun types-arg)))

Theorem: valid-funcall-type-equiv-congruence-on-type-fun

(defthm valid-funcall-type-equiv-congruence-on-type-fun
  (implies (type-equiv type-fun type-fun-equiv)
           (equal (valid-funcall expr type-fun types-arg)
                  (valid-funcall expr type-fun-equiv types-arg)))
  :rule-classes :congruence)

Theorem: valid-funcall-of-type-list-fix-types-arg

(defthm valid-funcall-of-type-list-fix-types-arg
  (equal (valid-funcall expr type-fun (type-list-fix types-arg))
         (valid-funcall expr type-fun types-arg)))

Theorem: valid-funcall-type-list-equiv-congruence-on-types-arg

(defthm valid-funcall-type-list-equiv-congruence-on-types-arg
  (implies (type-list-equiv types-arg types-arg-equiv)
           (equal (valid-funcall expr type-fun types-arg)
                  (valid-funcall expr type-fun types-arg-equiv)))
  :rule-classes :congruence)