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 (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-decl) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((or (token-declaration-specifier-start-p token) (and (token-keywordp token "__extension__") (parstate->gcc parstate))) (b* (((mv extension parstate) (if (and (token-keywordp token "__extension__") (parstate->gcc parstate)) (mv t parstate) (b* ((parstate (unread-token parstate))) (mv nil parstate)))) ((erp declspecs span parstate) (parse-declaration-specifiers nil parstate)) ((erp token2 span2 parstate) (read-token parstate))) (cond ((and (or (token-keywordp token2 "asm") (token-keywordp token2 "__asm") (token-keywordp token2 "__asm__")) (parstate->gcc parstate)) (b* ((uscores (cond ((token-keywordp token2 "asm") (keyword-uscores-none)) ((token-keywordp token2 "__asm") (keyword-uscores-start)) ((token-keywordp token2 "__asm__") (keyword-uscores-both)))) ((erp asmspec & parstate) (parse-asm-name-specifier uscores span2 parstate)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (make-decl-decl :extension extension :specs declspecs :init nil :asm? asmspec :attrib attrspecs) (span-join span last-span) parstate))) ((and (token-keywordp token2 "__attribute__") (parstate->gcc parstate)) (b* ((parstate (unread-token parstate)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (make-decl-decl :extension extension :specs declspecs :init nil :asm? nil :attrib attrspecs) (span-join span last-span) parstate))) ((token-declarator-start-p token2) (b* ((parstate (unread-token parstate)) ((erp initdeclors & parstate) (parse-init-declarator-list parstate)) ((erp asmspec? & parstate) (if (parstate->gcc parstate) (parse-?-asm-name-specifier parstate) (retok nil (irr-span) parstate))) ((erp attrspecs & parstate) (if (parstate->gcc parstate) (parse-*-attribute-specifier parstate) (retok nil (irr-span) parstate))) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (make-decl-decl :extension extension :specs declspecs :init initdeclors :asm? asmspec? :attrib attrspecs) (span-join span last-span) parstate))) ((token-punctuatorp token2 ";") (retok (make-decl-decl :extension extension :specs declspecs :init nil :asm? nil :attrib nil) (span-join span span2) parstate)) (t (reterr-msg :where (position-to-msg (span->start span2)) :expected "a declarator or a semicolon" :found (token-to-msg token2)))))) ((token-keywordp token "_Static_assert") (b* (((erp statassert last-span parstate) (parse-static-assert-declaration span parstate))) (retok (decl-statassert statassert) (span-join span last-span) parstate))) (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-parstate) (parse-declaration parstate))) (declp decl)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-declaration.span (b* (((mv acl2::?erp ?decl ?span ?new-parstate) (parse-declaration parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-declaration.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?decl ?span ?new-parstate) (parse-declaration parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-declaration-uncond (b* (((mv acl2::?erp ?decl ?span ?new-parstate) (parse-declaration parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-cond (b* (((mv acl2::?erp ?decl ?span ?new-parstate) (parse-declaration parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)