Parse an attribute specifier.
(parse-attribute-specifier first-span pstate) → (mv erp attrspec span new-pstate)
This is only used if GCC extensions are supported.
See the ABNF grammar rule for
This is called after parsing the initial
Function:
(defun parse-attribute-specifier (first-span pstate) (declare (xargs :guard (and (spanp first-span) (parstatep pstate)))) (let ((__function__ 'parse-attribute-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-attrib-spec) (irr-span) (irr-parstate)) ((erp & pstate) (read-punctuator "(" pstate)) ((erp & pstate) (read-punctuator "(" pstate)) ((erp attrs & pstate) (parse-attribute-list pstate)) ((erp & pstate) (read-punctuator ")" pstate)) ((erp last-span pstate) (read-punctuator ")" pstate))) (retok (attrib-spec attrs) (span-join first-span last-span) pstate))))
Theorem:
(defthm attrib-specp-of-parse-attribute-specifier.attrspec (b* (((mv acl2::?erp ?attrspec ?span ?new-pstate) (parse-attribute-specifier first-span pstate))) (attrib-specp attrspec)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-attribute-specifier.span (b* (((mv acl2::?erp ?attrspec ?span ?new-pstate) (parse-attribute-specifier first-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-attribute-specifier.new-pstate (b* (((mv acl2::?erp ?attrspec ?span ?new-pstate) (parse-attribute-specifier first-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-attribute-specifier-uncond (b* (((mv acl2::?erp ?attrspec ?span ?new-pstate) (parse-attribute-specifier first-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-specifier-cond (b* (((mv acl2::?erp ?attrspec ?span ?new-pstate) (parse-attribute-specifier first-span pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)