Check if a declarator has formal dynamic semantics, as part of a block item declaration.
The direct declarator part must be supported, and we can have any number of supported pointers.
Function:
(defun declor-block-formalp (declor) (declare (xargs :guard (declorp declor))) (declare (xargs :guard (declor-unambp declor))) (let ((__function__ 'declor-block-formalp)) (declare (ignorable __function__)) (and (pointers-formalp (declor->pointers declor)) (dirdeclor-block-formalp (declor->decl declor)))))
Theorem:
(defthm booleanp-of-declor-block-formalp (b* ((yes/no (declor-block-formalp declor))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm declor-block-formalp-of-declor-fix-declor (equal (declor-block-formalp (declor-fix declor)) (declor-block-formalp declor)))
Theorem:
(defthm declor-block-formalp-declor-equiv-congruence-on-declor (implies (declor-equiv declor declor-equiv) (equal (declor-block-formalp declor) (declor-block-formalp declor-equiv))) :rule-classes :congruence)