Parse zero or more attribute specifiers.
(parse-*-attribute-specifier pstate) → (mv erp attrspecs span new-pstate)
This is only used if GCC extensions are supported.
We parse a
If the next token is the
If there are no attribute specifiers, we return an irrelevant span. When combining the span of the first attribute specifier (if present) with the span of the remaining zero or more attribute specifiers, we join spans only if the remaining ones are one or more; if there are zero, the span of the first attribute specifier is also the span of the whole sequence.
Function:
(defun parse-*-attribute-specifier (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-*-attribute-specifier)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp token first-span pstate) (read-token pstate)) ((unless (equal token (token-keyword "__attribute__"))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok nil (irr-span) pstate))) ((erp attrspec span pstate) (parse-attribute-specifier first-span pstate)) ((erp attrspecs last-span pstate) (parse-*-attribute-specifier pstate))) (retok (cons attrspec attrspecs) (if attrspecs (span-join span last-span) span) pstate))))
Theorem:
(defthm attrib-spec-listp-of-parse-*-attribute-specifier.attrspecs (b* (((mv acl2::?erp ?attrspecs ?span ?new-pstate) (parse-*-attribute-specifier pstate))) (attrib-spec-listp attrspecs)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-*-attribute-specifier.span (b* (((mv acl2::?erp ?attrspecs ?span ?new-pstate) (parse-*-attribute-specifier pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-*-attribute-specifier.new-pstate (b* (((mv acl2::?erp ?attrspecs ?span ?new-pstate) (parse-*-attribute-specifier pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-*-attribute-specifier-uncond (b* (((mv acl2::?erp ?attrspecs ?span ?new-pstate) (parse-*-attribute-specifier pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)