		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-tag-declon

Check a tag declaration.

Signature
(check-tag-declon declon tagenv) → new-tagenv
Arguments: declon — Guard (tag-declonp declon).; tagenv — Guard (tag-envp tagenv).
Returns: new-tagenv — Type (tag-env-resultp 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 [C17:6.2.5/20], or at least two members if the last member is a flexible array member [C17: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 [C17:6.2.3].

C allows a form of recursion in structure type declarations, namely that a member can be a pointer to the structure: [C17:6.2.1/7] says that the scope of the tag starts where it appears, so it includes the members; and [C17:6.7.2.1/9] says that a member type must be complete, which pointer types are [C17: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.

Definitions and Theorems

Function: check-tag-declon

(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: tag-env-resultp-of-check-tag-declon

(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: check-tag-declon-of-tag-declon-fix-declon

(defthm check-tag-declon-of-tag-declon-fix-declon
  (equal (check-tag-declon (tag-declon-fix declon)
                           tagenv)
         (check-tag-declon declon tagenv)))

Theorem: check-tag-declon-tag-declon-equiv-congruence-on-declon

(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: check-tag-declon-of-tag-env-fix-tagenv

(defthm check-tag-declon-of-tag-env-fix-tagenv
  (equal (check-tag-declon declon (tag-env-fix tagenv))
         (check-tag-declon declon tagenv)))

Theorem: check-tag-declon-tag-env-equiv-congruence-on-tagenv

(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)