Print a GCC attribute.
Function:
(defun print-attrib (attr pstate) (declare (xargs :guard (and (attribp attr) (pristatep pstate)))) (let ((__function__ 'print-attrib)) (declare (ignorable __function__)) (attrib-case attr :name (print-ident attr.name pstate) :name-param (b* ((pstate (print-ident attr.name pstate)) (pstate (print-astring "(" pstate)) (pstate (if attr.param (print-expr-list attr.param pstate) pstate)) (pstate (print-astring ")" pstate))) pstate))))
Theorem:
(defthm pristatep-of-print-attrib (b* ((new-pstate (print-attrib attr pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-attrib-of-attrib-fix-attr (equal (print-attrib (attrib-fix attr) pstate) (print-attrib attr pstate)))
Theorem:
(defthm print-attrib-attrib-equiv-congruence-on-attr (implies (attrib-equiv attr attr-equiv) (equal (print-attrib attr pstate) (print-attrib attr-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-of-pristate-fix-pstate (equal (print-attrib attr (pristate-fix pstate)) (print-attrib attr pstate)))
Theorem:
(defthm print-attrib-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-attrib attr pstate) (print-attrib attr pstate-equiv))) :rule-classes :congruence)