Check a tag declaration.
(check-tag-declon declon tagenv) → new-tagenv
For now we only support structure type declarations, not union or enumeration type declarations. For a structure type declaration, we first check the members, obtaining a list of member types if successful. We ensure that there is at least one member [C:6.2.5/20], or at least two members if the last member is a flexible array member [C:6.2.5/18]. We use tag-env-add to ensure that there is not already another structure or union or enumeration type with the same tag, since these share one name space [C:6.2.3].
C allows a form of recursion in structure type declarations, namely that a member can be a pointer to the structure: [C:6.2.1/7] says that the scope of the tag starts where it appears, so it includes the members; and [C:6.7.2.1/9] says that a member type must be complete, which pointer types are [C:6:2.5/20]. However, we implicitly disallow even this form of recursion for now, because we check the member types against the current tag environment, which does not include the structure type yet.
Function:
(defun check-tag-declon (declon tagenv) (declare (xargs :guard (and (tag-declonp declon) (tag-envp tagenv)))) (let ((__function__ 'check-tag-declon)) (declare (ignorable __function__)) (tag-declon-case declon :struct (b* (((okf members) (check-struct-declon-list declon.members tagenv)) ((unless (consp members)) (reserrf (list :empty-struct (tag-declon-fix declon)))) ((when (b* ((member (car (last members))) (type (member-type->type member))) (and (type-case type :array) (not (type-array->size type)) (endp (cdr members))))) (reserrf (list :struct-with-just-flexible-array-member members))) (info (tag-info-struct members)) (tagenv-opt (tag-env-add declon.tag info tagenv))) (tag-env-option-case tagenv-opt :some tagenv-opt.val :none (reserrf (list :duplicate-tag declon.tag)))) :union (reserrf (list :union-not-supported (tag-declon-fix declon))) :enum (reserrf (list :enum-not-supported (tag-declon-fix declon))))))
Theorem:
(defthm tag-env-resultp-of-check-tag-declon (b* ((new-tagenv (check-tag-declon declon tagenv))) (tag-env-resultp new-tagenv)) :rule-classes :rewrite)
Theorem:
(defthm check-tag-declon-of-tag-declon-fix-declon (equal (check-tag-declon (tag-declon-fix declon) tagenv) (check-tag-declon declon tagenv)))
Theorem:
(defthm check-tag-declon-tag-declon-equiv-congruence-on-declon (implies (tag-declon-equiv declon declon-equiv) (equal (check-tag-declon declon tagenv) (check-tag-declon declon-equiv tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-tag-declon-of-tag-env-fix-tagenv (equal (check-tag-declon declon (tag-env-fix tagenv)) (check-tag-declon declon tagenv)))
Theorem:
(defthm check-tag-declon-tag-env-equiv-congruence-on-tagenv (implies (tag-env-equiv tagenv tagenv-equiv) (equal (check-tag-declon declon tagenv) (check-tag-declon declon tagenv-equiv))) :rule-classes :congruence)