		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Fundef-formalp

Check if a function definition has dynamic formal semantics.

Signature
(fundef-formalp fundef) → yes/no
Arguments: fundef — Guard (fundefp fundef).
Returns: yes/no — Type (booleanp yes/no).

There must be no GCC extensions. The declaration specifiers must be all type specifiers, and they must form a supported type specifier sequence. The declarator must be one supported for a function. There must be no assembler name specifier or attribute specifiers. There must be no declarations between the declarators and the body. The body must be a compound statement (see ldm-fundef), whose block items are all supported.

Definitions and Theorems

Function: fundef-formalp

(defun fundef-formalp (fundef)
 (declare (xargs :guard (fundefp fundef)))
 (declare (xargs :guard (fundef-unambp fundef)))
 (let ((__function__ 'fundef-formalp))
  (declare (ignorable __function__))
  (b* (((fundef fundef) fundef))
   (and
    (not fundef.extension)
    (b* (((mv okp tyspecs)
          (check-decl-spec-list-all-typespec fundef.spec)))
      (and okp (type-spec-list-formalp tyspecs)))
    (declor-fun-formalp fundef.declor)
    (not fundef.asm?)
    (endp fundef.attribs)
    (endp fundef.decls)
    (stmt-case fundef.body :compound)
    (block-item-list-formalp (stmt-compound->items fundef.body))))))

Theorem: booleanp-of-fundef-formalp

(defthm booleanp-of-fundef-formalp
  (b* ((yes/no (fundef-formalp fundef)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: fundef-formalp-of-fundef-fix-fundef

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

Theorem: fundef-formalp-fundef-equiv-congruence-on-fundef

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