CHeck if all the variables in a scope are defined.
(var-scope-all-definedp varscope) → 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 [C:6.9.2/2]. So we go through the variables in the (file) scope, ensuring that they are defined or tentatively defined.
Function:
(defun var-scope-all-definedp (varscope) (declare (xargs :guard (var-table-scopep varscope))) (let ((__function__ 'var-scope-all-definedp)) (declare (ignorable __function__)) (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:
(defthm booleanp-of-var-scope-all-definedp (b* ((yes/no (var-scope-all-definedp varscope))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(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:
(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)