		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-obj-declon

Check an object declaration.

Signature
(check-obj-declon declon funtab vartab tagenv constp initp) → new-vartab
Arguments: declon — Guard (obj-declonp declon).; funtab — Guard (fun-tablep funtab).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).; constp — Guard (booleanp constp).; initp — Guard (booleanp initp).
Returns: new-vartab — Type (var-table-resultp new-vartab).

We ensure that the type is complete [C:6.7/7]; this is not always necessary in full C, but our C subset requires that. We also ensure that the initializer type matches the declared type, if the initializer is present.

If the declaration is in a file scope, which is the case when there is just one scope in the variable table, we allow the extern storage class specifier; otherwise, we disallow it.

The constp flag controls whether we require the initializer, if present, to be constant or not. If the initializer is absent, the test passes.

The initp flag controls whether we require the initializer to be present.

We return the updated variable table. If there is no initializer, in our C subset this must be in a file scope; since we require no extern storage class specifier for now, in this case this must be a tentative definition [C:6.9.2/2]. If instead there is an intializer, then it is a definition, regardless of whether it has file scope or block scope.

Definitions and Theorems

Function: check-obj-declon

(defun check-obj-declon (declon funtab vartab tagenv constp initp)
 (declare (xargs :guard (and (obj-declonp declon)
                             (fun-tablep funtab)
                             (var-tablep vartab)
                             (tag-envp tagenv)
                             (booleanp constp)
                             (booleanp initp))))
 (let ((__function__ 'check-obj-declon))
  (declare (ignorable __function__))
  (b*
   (((mv var scspec tyname init?)
     (obj-declon-to-ident+scspec+tyname+init declon))
    ((when (and (consp (cdr vartab))
                (scspecseq-case scspec :extern)))
     (reserrf
          (list :block-extern-disallowed (obj-declon-fix declon))))
    ((okf type)
     (check-tyname tyname tagenv))
    ((okf &) (check-ident var))
    ((unless (type-completep type))
     (reserrf
      (list :declon-error-type-incomplete (obj-declon-fix declon))))
    ((when (not init?))
     (if initp
      (reserrf
        (list :declon-initializer-required (obj-declon-fix declon)))
      (var-table-add-var var type (var-defstatus-tentative)
                         vartab)))
    (init init?)
    ((okf init-type)
     (check-initer init funtab vartab tagenv constp))
    ((okf &)
     (init-type-matchp init-type type)))
   (var-table-add-var var type (var-defstatus-defined)
                      vartab))))

Theorem: var-table-resultp-of-check-obj-declon

(defthm var-table-resultp-of-check-obj-declon
  (b* ((new-vartab
            (check-obj-declon declon
                              funtab vartab tagenv constp initp)))
    (var-table-resultp new-vartab))
  :rule-classes :rewrite)

Theorem: check-obj-declon-of-obj-declon-fix-declon

(defthm check-obj-declon-of-obj-declon-fix-declon
  (equal (check-obj-declon (obj-declon-fix declon)
                           funtab vartab tagenv constp initp)
         (check-obj-declon declon
                           funtab vartab tagenv constp initp)))

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

(defthm check-obj-declon-obj-declon-equiv-congruence-on-declon
  (implies
       (obj-declon-equiv declon declon-equiv)
       (equal (check-obj-declon declon
                                funtab vartab tagenv constp initp)
              (check-obj-declon declon-equiv
                                funtab vartab tagenv constp initp)))
  :rule-classes :congruence)

Theorem: check-obj-declon-of-fun-table-fix-funtab

(defthm check-obj-declon-of-fun-table-fix-funtab
  (equal (check-obj-declon declon (fun-table-fix funtab)
                           vartab tagenv constp initp)
         (check-obj-declon declon
                           funtab vartab tagenv constp initp)))

Theorem: check-obj-declon-fun-table-equiv-congruence-on-funtab

(defthm check-obj-declon-fun-table-equiv-congruence-on-funtab
  (implies
       (fun-table-equiv funtab funtab-equiv)
       (equal (check-obj-declon declon
                                funtab vartab tagenv constp initp)
              (check-obj-declon declon funtab-equiv
                                vartab tagenv constp initp)))
  :rule-classes :congruence)

Theorem: check-obj-declon-of-var-table-fix-vartab

(defthm check-obj-declon-of-var-table-fix-vartab
  (equal (check-obj-declon declon funtab (var-table-fix vartab)
                           tagenv constp initp)
         (check-obj-declon declon
                           funtab vartab tagenv constp initp)))

Theorem: check-obj-declon-var-table-equiv-congruence-on-vartab

(defthm check-obj-declon-var-table-equiv-congruence-on-vartab
  (implies
       (var-table-equiv vartab vartab-equiv)
       (equal (check-obj-declon declon
                                funtab vartab tagenv constp initp)
              (check-obj-declon declon funtab
                                vartab-equiv tagenv constp initp)))
  :rule-classes :congruence)

Theorem: check-obj-declon-of-tag-env-fix-tagenv

(defthm check-obj-declon-of-tag-env-fix-tagenv
  (equal (check-obj-declon declon
                           funtab vartab (tag-env-fix tagenv)
                           constp initp)
         (check-obj-declon declon
                           funtab vartab tagenv constp initp)))

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

(defthm check-obj-declon-tag-env-equiv-congruence-on-tagenv
  (implies
       (tag-env-equiv tagenv tagenv-equiv)
       (equal (check-obj-declon declon
                                funtab vartab tagenv constp initp)
              (check-obj-declon declon funtab
                                vartab tagenv-equiv constp initp)))
  :rule-classes :congruence)

Theorem: check-obj-declon-of-bool-fix-constp

(defthm check-obj-declon-of-bool-fix-constp
  (equal (check-obj-declon declon funtab
                           vartab tagenv (acl2::bool-fix constp)
                           initp)
         (check-obj-declon declon
                           funtab vartab tagenv constp initp)))

Theorem: check-obj-declon-iff-congruence-on-constp

(defthm check-obj-declon-iff-congruence-on-constp
  (implies
       (iff constp constp-equiv)
       (equal (check-obj-declon declon
                                funtab vartab tagenv constp initp)
              (check-obj-declon declon funtab
                                vartab tagenv constp-equiv initp)))
  :rule-classes :congruence)

Theorem: check-obj-declon-of-bool-fix-initp

(defthm check-obj-declon-of-bool-fix-initp
  (equal (check-obj-declon declon funtab vartab
                           tagenv constp (acl2::bool-fix initp))
         (check-obj-declon declon
                           funtab vartab tagenv constp initp)))

Theorem: check-obj-declon-iff-congruence-on-initp

(defthm check-obj-declon-iff-congruence-on-initp
  (implies
       (iff initp initp-equiv)
       (equal (check-obj-declon declon
                                funtab vartab tagenv constp initp)
              (check-obj-declon declon funtab
                                vartab tagenv constp initp-equiv)))
  :rule-classes :congruence)