Parse an attribute.
This is only used if GCC extensions are supported.
See the ABNF grammar rule for
Function:
(defun parse-attribute (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-attribute)) (declare (ignorable __function__)) (b* (((reterr) (irr-attrib) (irr-span) (irr-parstate)) ((erp ident ident-span pstate) (read-identifier pstate)) ((erp token & pstate) (read-token pstate))) (cond ((equal token (token-punctuator "(")) (b* ((pstate (unread-token pstate)) ((erp exprs span pstate) (parse-attribute-parameters pstate))) (retok (make-attrib-name-param :name ident :param exprs) (span-join ident-span span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (attrib-name ident) ident-span pstate)))))))
Theorem:
(defthm attribp-of-parse-attribute.attr (b* (((mv acl2::?erp ?attr ?span ?new-pstate) (parse-attribute pstate))) (attribp attr)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-attribute.span (b* (((mv acl2::?erp ?attr ?span ?new-pstate) (parse-attribute pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-attribute.new-pstate (b* (((mv acl2::?erp ?attr ?span ?new-pstate) (parse-attribute pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-attribute-uncond (b* (((mv acl2::?erp ?attr ?span ?new-pstate) (parse-attribute pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-cond (b* (((mv acl2::?erp ?attr ?span ?new-pstate) (parse-attribute pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)