		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Decl-block-formalp

Check if a declaration has formal dynamic semantics, as a block item.

Signature
(decl-block-formalp decl) → yes/no
Arguments: decl — Guard (declp decl).
Returns: yes/no — Type (booleanp yes/no).

The declaration must not be a static assertion declaration. The GCC extensions must be absent, since they are not covered by our formal semantics. All the declaration specifiers must be type specifiers, because c::exec-block-item does not support storage class specifiers; the type specifier sequence must be a supported one. There must be exactly one supported initializer declarator.

Definitions and Theorems

Function: decl-block-formalp

(defun decl-block-formalp (decl)
 (declare (xargs :guard (declp decl)))
 (declare (xargs :guard (decl-unambp decl)))
 (let ((__function__ 'decl-block-formalp))
  (declare (ignorable __function__))
  (decl-case
   decl
   :decl (and (not decl.extension)
              (b* (((mv okp tyspecs)
                    (check-decl-spec-list-all-typespec decl.specs)))
                (and okp (type-spec-list-formalp tyspecs)))
              (consp decl.init)
              (endp (cdr decl.init))
              (initdeclor-block-formalp (car decl.init)))
   :statassert nil)))

Theorem: booleanp-of-decl-block-formalp

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

Theorem: decl-block-formalp-of-decl-fix-decl

(defthm decl-block-formalp-of-decl-fix-decl
  (equal (decl-block-formalp (decl-fix decl))
         (decl-block-formalp decl)))

Theorem: decl-block-formalp-decl-equiv-congruence-on-decl

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