		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Pointers-formalp

Check if a list of pointers has formal dynamic semantics.

Signature
(pointers-formalp pointers) → yes/no
Arguments: pointers — Guard (typequal/attribspec-list-listp pointers).
Returns: yes/no — Type (booleanp yes/no).

Here `pointers' refers to the constructs that may precede a direct declarator to form a declarator, or a direct abstract declarator to form an abstract declarator. Currently only (non-abstract) declarators are supported, so for now we are only interested in the pointers in them. We support any number of pointers, but without type qualifiers or attribute specifiers. So we just check that each inner list is empty. Refer declor for an explanation of how pointers are modeled.

Definitions and Theorems

Function: pointers-formalp

(defun pointers-formalp (pointers)
  (declare (xargs :guard (typequal/attribspec-list-listp pointers)))
  (let ((__function__ 'pointers-formalp))
    (declare (ignorable __function__))
    (or (endp pointers)
        (and (endp (car pointers))
             (pointers-formalp (cdr pointers))))))

Theorem: booleanp-of-pointers-formalp

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

Theorem: pointers-formalp-of-typequal/attribspec-list-list-fix-pointers

(defthm
     pointers-formalp-of-typequal/attribspec-list-list-fix-pointers
 (equal
     (pointers-formalp (typequal/attribspec-list-list-fix pointers))
     (pointers-formalp pointers)))

Theorem: pointers-formalp-typequal/attribspec-list-list-equiv-congruence-on-pointers

(defthm
 pointers-formalp-typequal/attribspec-list-list-equiv-congruence-on-pointers
 (implies
      (typequal/attribspec-list-list-equiv pointers pointers-equiv)
      (equal (pointers-formalp pointers)
             (pointers-formalp pointers-equiv)))
 :rule-classes :congruence)