		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-transunit

Check a translation unit.

Signature
(check-transunit tunit) → wf
Arguments: tunit — Guard (transunitp tunit).
Returns: wf — Type (wellformed-resultp wf).

Starting from the initial (empty) function table, we check all the external declarations, threading the function table through, and discarding the final one (it served its pupose).

We also ensure that there is at leaast one external declaration, according to the grammatical requirement in [C:6.9/1].

We also check that the external objects and the functions have no overlap in their names (identifiers). These are all ordinary identifiers [C:6.2.3/1], and therefore must be distinct in the same (file) scope.

We also check that all the functions are defined; we perform this check on the function table that results from checking the external declarations. This is a little stricter than [C:6.9/5], which allows a function to remain undefined if it is not called in the rest of the program. However, as we look at a translation unit in isolation here, we do not have the rest of the program, and thus we make the stricter check for now.

Definitions and Theorems

Function: check-transunit

(defun check-transunit (tunit)
 (declare (xargs :guard (transunitp tunit)))
 (let ((__function__ 'check-transunit))
   (declare (ignorable __function__))
   (b* (((transunit tunit) tunit)
        ((unless (consp tunit.declons))
         (reserrf (list :transunit-empty)))
        (funtab (fun-table-init))
        (vartab (var-table-init))
        (tagenv (tag-env-init))
        ((okf funtab+vartab+tagenv)
         (check-ext-declon-list tunit.declons funtab vartab tagenv))
        (funtab (funtab+vartab+tagenv->funs funtab+vartab+tagenv))
        (vartab (funtab+vartab+tagenv->vars funtab+vartab+tagenv))
        (overlap (intersect (omap::keys funtab)
                            (omap::keys (car vartab))))
        ((unless (emptyp overlap))
         (reserrf (list :transunit-fun-obj-overlap overlap)))
        ((unless (var-table-add-block vartab))
         (reserrf (list :transunit-has-undef-var vartab)))
        ((unless (fun-table-all-definedp funtab))
         (reserrf (list :transunit-has-undef-fun funtab))))
     :wellformed)))

Theorem: wellformed-resultp-of-check-transunit

(defthm wellformed-resultp-of-check-transunit
  (b* ((wf (check-transunit tunit)))
    (wellformed-resultp wf))
  :rule-classes :rewrite)

Theorem: check-transunit-of-transunit-fix-tunit

(defthm check-transunit-of-transunit-fix-tunit
  (equal (check-transunit (transunit-fix tunit))
         (check-transunit tunit)))

Theorem: check-transunit-transunit-equiv-congruence-on-tunit

(defthm check-transunit-transunit-equiv-congruence-on-tunit
  (implies (transunit-equiv tunit tunit-equiv)
           (equal (check-transunit tunit)
                  (check-transunit tunit-equiv)))
  :rule-classes :congruence)