Parse a declaration.
A declaration is either an assert declaration,
recognized by the starting
If GCC extensions are supported, we must also allow for
an optional assembler name specifier,
as well as for zero or more attribute specifiers,
ending a declaration, just before the semicolon;
and we must also allow for an
Function:
(defun parse-declaration (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-decl) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((or (token-declaration-specifier-start-p token) (and (equal token (token-keyword "__extension__")) (parstate->gcc pstate))) (b* (((mv extension pstate) (if (and (equal token (token-keyword "__extension__")) (parstate->gcc pstate)) (mv t pstate) (mv nil (unread-token pstate)))) ((erp declspecs span pstate) (parse-declaration-specifiers nil pstate)) ((erp token2 span2 pstate) (read-token pstate))) (cond ((and (or (equal token2 (token-keyword "asm")) (equal token2 (token-keyword "__asm__"))) (parstate->gcc pstate)) (b* ((uscores (equal token2 (token-keyword "__asm__"))) ((erp asmspec & pstate) (parse-asm-name-specifier uscores span2 pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (make-decl-decl :extension extension :specs declspecs :init nil :asm? asmspec :attrib attrspecs) (span-join span last-span) pstate))) ((and (equal token2 (token-keyword "__attribute__")) (parstate->gcc pstate)) (b* ((pstate (unread-token pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (make-decl-decl :extension extension :specs declspecs :init nil :asm? nil :attrib attrspecs) (span-join span last-span) pstate))) ((token-declarator-start-p token2) (b* ((pstate (unread-token pstate)) ((erp initdeclors & pstate) (parse-init-declarator-list pstate)) ((erp asmspec? & pstate) (if (parstate->gcc pstate) (parse-?-asm-name-specifier pstate) (retok nil (irr-span) pstate))) ((erp attrspecs & pstate) (if (parstate->gcc pstate) (parse-*-attribute-specifier pstate) (retok nil (irr-span) pstate))) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (make-decl-decl :extension extension :specs declspecs :init initdeclors :asm? asmspec? :attrib attrspecs) (span-join span last-span) pstate))) ((equal token2 (token-punctuator ";")) (retok (make-decl-decl :extension extension :specs declspecs :init nil :asm? nil :attrib nil) (span-join span span2) pstate)) (t (reterr-msg :where (position-to-msg (span->start span2)) :expected "a declarator or a semicolon" :found (token-to-msg token2)))))) ((equal token (token-keyword "_Static_assert")) (b* (((erp statassert last-span pstate) (parse-static-assert-declaration span pstate))) (retok (decl-statassert statassert) (span-join span last-span) pstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "a declaration specifier ~ or the _Static_assert keyword" :found (token-to-msg token)))))))
Theorem:
(defthm declp-of-parse-declaration.decl (b* (((mv acl2::?erp ?decl ?span ?new-pstate) (parse-declaration pstate))) (declp decl)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-declaration.span (b* (((mv acl2::?erp ?decl ?span ?new-pstate) (parse-declaration pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-declaration.new-pstate (b* (((mv acl2::?erp ?decl ?span ?new-pstate) (parse-declaration pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-declaration-uncond (b* (((mv acl2::?erp ?decl ?span ?new-pstate) (parse-declaration pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-cond (b* (((mv acl2::?erp ?decl ?span ?new-pstate) (parse-declaration pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)