Disambiguate a translation unit.
(dimb-transunit tunit gcc) → (mv erp new-tunit)
We initialize the disambiguation table, we disambiguate all the external declarations in order, and we discard the final disambiguation table.
If the GCC flag is
Function:
(defun dimb-transunit (tunit gcc) (declare (xargs :guard (and (transunitp tunit) (booleanp gcc)))) (let ((__function__ 'dimb-transunit)) (declare (ignorable __function__)) (b* (((reterr) (irr-transunit)) (edecls (transunit->decls tunit)) (table (dimb-init-table)) (table (if gcc (b* ((table (dimb-add-ident (ident "__builtin_va_list") (dimb-kind-typedef) table) ) (table (dimb-add-ident (ident "__builtin_bswap16") (dimb-kind-objfun) table) ) (table (dimb-add-ident (ident "__builtin_bswap32") (dimb-kind-objfun) table) ) (table (dimb-add-ident (ident "__builtin_bswap64") (dimb-kind-objfun) table) ) (table (dimb-add-ident (ident "_Float128") (dimb-kind-typedef) table) )) table) table) ) ((erp new-edecls &) (dimb-extdecl-list edecls table))) (retok (transunit new-edecls)))))
Theorem:
(defthm transunitp-of-dimb-transunit.new-tunit (b* (((mv acl2::?erp ?new-tunit) (dimb-transunit tunit gcc))) (transunitp new-tunit)) :rule-classes :rewrite)
Theorem:
(defthm transunit-unambp-of-dimb-transunit (b* (((mv acl2::?erp ?new-tunit) (dimb-transunit tunit gcc))) (implies (not erp) (transunit-unambp new-tunit))))
Theorem:
(defthm dimb-transunit-of-transunit-fix-tunit (equal (dimb-transunit (transunit-fix tunit) gcc) (dimb-transunit tunit gcc)))
Theorem:
(defthm dimb-transunit-transunit-equiv-congruence-on-tunit (implies (transunit-equiv tunit tunit-equiv) (equal (dimb-transunit tunit gcc) (dimb-transunit tunit-equiv gcc))) :rule-classes :congruence)
Theorem:
(defthm dimb-transunit-of-bool-fix-gcc (equal (dimb-transunit tunit (bool-fix gcc)) (dimb-transunit tunit gcc)))
Theorem:
(defthm dimb-transunit-iff-congruence-on-gcc (implies (iff gcc gcc-equiv) (equal (dimb-transunit tunit gcc) (dimb-transunit tunit gcc-equiv))) :rule-classes :congruence)