Check if an initializer declarator has formal dynamic semantics, as part of a block item declaration.
(initdeclor-block-formalp initdeclor) → yes/no
In c::exec-block-item, the initializer must be present and supported. The declarator must be supported too.
Function:
(defun initdeclor-block-formalp (initdeclor) (declare (xargs :guard (initdeclorp initdeclor))) (declare (xargs :guard (initdeclor-unambp initdeclor))) (let ((__function__ 'initdeclor-block-formalp)) (declare (ignorable __function__)) (b* (((initdeclor initdeclor) initdeclor)) (and (declor-block-formalp initdeclor.declor) (not initdeclor.asm?) initdeclor.init? (initer-formalp initdeclor.init?)))))
Theorem:
(defthm booleanp-of-initdeclor-block-formalp (b* ((yes/no (initdeclor-block-formalp initdeclor))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm initdeclor-block-formalp-of-initdeclor-fix-initdeclor (equal (initdeclor-block-formalp (initdeclor-fix initdeclor)) (initdeclor-block-formalp initdeclor)))
Theorem:
(defthm initdeclor-block-formalp-initdeclor-equiv-congruence-on-initdeclor (implies (initdeclor-equiv initdeclor initdeclor-equiv) (equal (initdeclor-block-formalp initdeclor) (initdeclor-block-formalp initdeclor-equiv))) :rule-classes :congruence)