		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)
         (type-spec-case (decl-spec-typespec->spec (car decl.specs))
                         :struct)
         (strunispec-formalp
              (type-spec-struct->spec
                   (decl-spec-typespec->spec (car decl.specs))))
         (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)