Print a list of one or more GCC attributes, comma-separated.
(print-attrib-list attrs pstate) → new-pstate
Function:
(defun print-attrib-list (attrs pstate) (declare (xargs :guard (and (attrib-listp attrs) (pristatep pstate)))) (declare (xargs :guard (consp attrs))) (let ((__function__ 'print-attrib-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp attrs))) (pristate-fix pstate)) (pstate (print-attrib (car attrs) pstate)) ((when (endp (cdr attrs))) pstate) (pstate (print-astring ", " pstate))) (print-attrib-list (cdr attrs) pstate))))
Theorem:
(defthm pristatep-of-print-attrib-list (b* ((new-pstate (print-attrib-list attrs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-attrib-list-of-attrib-list-fix-attrs (equal (print-attrib-list (attrib-list-fix attrs) pstate) (print-attrib-list attrs pstate)))
Theorem:
(defthm print-attrib-list-attrib-list-equiv-congruence-on-attrs (implies (attrib-list-equiv attrs attrs-equiv) (equal (print-attrib-list attrs pstate) (print-attrib-list attrs-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-list-of-pristate-fix-pstate (equal (print-attrib-list attrs (pristate-fix pstate)) (print-attrib-list attrs pstate)))
Theorem:
(defthm print-attrib-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-attrib-list attrs pstate) (print-attrib-list attrs pstate-equiv))) :rule-classes :congruence)