		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Fundef-types

Types of the values returned by a function, from the validation information.

Signature
(fundef-types fundef) → types
Arguments: fundef — Guard (fundefp fundef).
Returns: types — Type (type-setp types).

The set of possible types returned by the function is the set of possible types returned by the body, roughly speaking. More precisely, the latter is a set of optional types, where nil means that the body terminates without a return. For a function, this is equivalent to a return without expression. Thus, we turn the nil in the set of types, if any, into void type, obtaining the set of types (not optional types) of the function's result. We use that in the theorem about the function, which says that the result, which is an optional value in our formal semantics, has a type in the set; we use c::type-of-value-option to map values to their types, and nil to void.

Although a function definition has one return type (possibly void), its body may return values of slightly different types, possibly subject to conversions. However, our formal semantics of C does not cover those conversions yet, so we adopt the more general view here.

Definitions and Theorems

Function: fundef-types

(defun fundef-types (fundef)
  (declare (xargs :guard (fundefp fundef)))
  (declare (xargs :guard (and (fundef-unambp fundef)
                              (fundef-annop fundef))))
  (b* ((types (comp-stmt-types (fundef->body fundef)))
       (types (if (in nil types)
                  (insert (type-void) (delete nil types))
                types)))
    types))

Theorem: type-setp-of-fundef-types

(defthm type-setp-of-fundef-types
  (b* ((types (fundef-types fundef)))
    (type-setp types))
  :rule-classes :rewrite)

Theorem: fundef-types-of-fundef-fix-fundef

(defthm fundef-types-of-fundef-fix-fundef
  (equal (fundef-types (fundef-fix fundef))
         (fundef-types fundef)))

Theorem: fundef-types-fundef-equiv-congruence-on-fundef

(defthm fundef-types-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (fundef-types fundef)
                  (fundef-types fundef-equiv)))
  :rule-classes :congruence)