		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Decl-struct-formalp

Check if a declaration has formal dynamic semantics, as a declaration for a structure type.

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

This must not be a static assertion declaration. It must consists of a single type specifier without declarators. The type specifier must be for a structure type, and have a supported structure or union specifier. There must be no GCC extensions.

Definitions and Theorems

Function: decl-struct-formalp

(defun decl-struct-formalp (decl)
 (declare (xargs :guard (declp decl)))
 (declare (xargs :guard (decl-unambp decl)))
 (let ((__function__ 'decl-struct-formalp))
  (declare (ignorable __function__))
  (decl-case
     decl
     :decl
     (and (not decl.extension)
          (consp decl.specs)
          (endp (cdr decl.specs))
          (decl-spec-case (car decl.specs)
                          :typespec)
          (b* ((tyspec (decl-spec-typespec->spec (car decl.specs))))
            (and (type-spec-case tyspec :struct)
                 (b* ((strunispec (type-spec-struct->spec tyspec)))
                   (and (strunispec-formalp strunispec)
                        (endp decl.init))))))
     :statassert nil)))

Theorem: booleanp-of-decl-struct-formalp

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

Theorem: decl-struct-formalp-of-decl-fix-decl

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

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

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