		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Decl-obj-formalp

Check if a declaration has formal dynamic semantics, as an object declaration (not in a block).

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

This complements initdeclor-obj-formalp; see the documentation of that function. The declaration must not be a static assertion declaration. We require a single supported initializer declarator. The declaration specifiers must be all type specifiers and storage class specifiers: the former must form a supported sequence, and the latter must be either absent or a single extern. We do not support GCC extensions.

Definitions and Theorems

Function: decl-obj-formalp

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

Theorem: booleanp-of-decl-obj-formalp

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

Theorem: decl-obj-formalp-of-decl-fix-decl

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

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

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