		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-obj-adeclor

Check an abstract object declarator.

Signature
(check-obj-adeclor declor type) → type
Arguments: declor — Guard (obj-adeclorp declor).; type — Guard (typep type).
Returns: type — Type (type-resultp type).

This is checked with respect to a type, which initially is the type denoted by the type specifier sequence that precedes the abstract object declarator, and then is the type obtained by augmenting that initial type with the layers that form the abstract object declarator.

When we reach the end of the abstract object declarator, we just return the type. If we find a pointer layer, we wrap the type into a pointer type and we continue through the subsequent layers recursively. If we find an array layer, we ensure that the current type, which is the element type, is complete [C:6.2.5/20]. If the array size is present, we check that it is well-formed and non-zero, and we use its value as the array size. Whether the size is present or not, we wrap the type into an array type and we continue through the subsequent layers recursively.

Definitions and Theorems

Function: check-obj-adeclor

(defun check-obj-adeclor (declor type)
 (declare (xargs :guard (and (obj-adeclorp declor)
                             (typep type))))
 (let ((__function__ 'check-obj-adeclor))
  (declare (ignorable __function__))
  (obj-adeclor-case
     declor :none (type-fix type)
     :pointer
     (check-obj-adeclor declor.decl (type-pointer type))
     :array
     (b* (((unless (type-completep type))
           (reserrf (list :incomplete-array-type-element
                          (type-fix type)
                          (obj-adeclor-fix declor))))
          ((unless declor.size)
           (check-obj-adeclor declor.decl
                              (make-type-array :of type :size nil)))
          ((okf &) (check-iconst declor.size))
          (size (iconst->value declor.size))
          ((when (equal size 0))
           (reserrf (list :zero-size-array-type (type-fix type)
                          (obj-adeclor-fix declor)))))
       (check-obj-adeclor declor.decl
                          (make-type-array :of type
                                           :size size))))))

Theorem: type-resultp-of-check-obj-adeclor

(defthm type-resultp-of-check-obj-adeclor
  (b* ((type (check-obj-adeclor declor type)))
    (type-resultp type))
  :rule-classes :rewrite)

Theorem: check-obj-adeclor-of-obj-adeclor-fix-declor

(defthm check-obj-adeclor-of-obj-adeclor-fix-declor
  (equal (check-obj-adeclor (obj-adeclor-fix declor)
                            type)
         (check-obj-adeclor declor type)))

Theorem: check-obj-adeclor-obj-adeclor-equiv-congruence-on-declor

(defthm check-obj-adeclor-obj-adeclor-equiv-congruence-on-declor
  (implies (obj-adeclor-equiv declor declor-equiv)
           (equal (check-obj-adeclor declor type)
                  (check-obj-adeclor declor-equiv type)))
  :rule-classes :congruence)

Theorem: check-obj-adeclor-of-type-fix-type

(defthm check-obj-adeclor-of-type-fix-type
  (equal (check-obj-adeclor declor (type-fix type))
         (check-obj-adeclor declor type)))

Theorem: check-obj-adeclor-type-equiv-congruence-on-type

(defthm check-obj-adeclor-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (check-obj-adeclor declor type)
                  (check-obj-adeclor declor type-equiv)))
  :rule-classes :congruence)