		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Var-scope-all-definedp

CHeck if all the variables in a scope are defined.

Signature
(var-scope-all-definedp varscope) → yes/no
Arguments: varscope — Guard (var-table-scopep varscope).
Returns: yes/no — Type (booleanp yes/no).

This applies to the file scope; see var-table-all-definedp.

Even though C allows a variable to remain undefined in a translation unit (if it is not used in expressions), we are more strict and require every variable to be defined. This includes the case of a tentative definition, which is automatically turned into a full definition [C17:6.9.2/2]. So we go through the variables in the (file) scope, ensuring that they are defined or tentatively defined.

Definitions and Theorems

Function: var-scope-all-definedp

(defun var-scope-all-definedp (varscope)
  (declare (xargs :guard (var-table-scopep varscope)))
  (b* ((varscope (var-table-scope-fix varscope))
       ((when (omap::emptyp varscope)) t)
       ((mv & info) (omap::head varscope))
       (defstatus (var-sinfo->defstatus info))
       ((unless (or (var-defstatus-case defstatus :defined)
                    (var-defstatus-case defstatus :tentative)))
        nil))
    (var-scope-all-definedp (omap::tail varscope))))

Theorem: booleanp-of-var-scope-all-definedp

(defthm booleanp-of-var-scope-all-definedp
  (b* ((yes/no (var-scope-all-definedp varscope)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: var-scope-all-definedp-of-var-table-scope-fix-varscope

(defthm var-scope-all-definedp-of-var-table-scope-fix-varscope
  (equal (var-scope-all-definedp (var-table-scope-fix varscope))
         (var-scope-all-definedp varscope)))

Theorem: var-scope-all-definedp-var-table-scope-equiv-congruence-on-varscope

(defthm
 var-scope-all-definedp-var-table-scope-equiv-congruence-on-varscope
 (implies (var-table-scope-equiv varscope varscope-equiv)
          (equal (var-scope-all-definedp varscope)
                 (var-scope-all-definedp varscope-equiv)))
 :rule-classes :congruence)