Parse an assembler name specifier.
(parse-asm-name-specifier uscores first-span parstate) → (mv erp asmspec span new-parstate)
This is used only if GCC extensions are supported.
This is called after parsing the initial
Function:
(defun parse-asm-name-specifier (uscores first-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (booleanp uscores) (spanp first-span) (parstatep parstate)))) (let ((__function__ 'parse-asm-name-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-asm-name-spec) (irr-span) parstate) ((erp & parstate) (read-punctuator "(" parstate)) ((erp token span parstate) (read-token parstate)) ((unless (and token (token-case token :string))) (reterr-msg :where (position-to-msg (span->start span)) :expected "a string literal" :found (token-to-msg token))) (parstate (unread-token parstate)) ((erp strings & parstate) (parse-*-stringlit parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-asm-name-spec :strings strings :uscores uscores) (span-join first-span last-span) parstate))))
Theorem:
(defthm asm-name-specp-of-parse-asm-name-specifier.asmspec (b* (((mv acl2::?erp ?asmspec ?span ?new-parstate) (parse-asm-name-specifier uscores first-span parstate))) (asm-name-specp asmspec)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-asm-name-specifier.span (b* (((mv acl2::?erp ?asmspec ?span ?new-parstate) (parse-asm-name-specifier uscores first-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-asm-name-specifier.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?asmspec ?span ?new-parstate) (parse-asm-name-specifier uscores first-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-asm-name-specifier-uncond (b* (((mv acl2::?erp ?asmspec ?span ?new-parstate) (parse-asm-name-specifier uscores first-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-asm-name-specifier-cond (b* (((mv acl2::?erp ?asmspec ?span ?new-parstate) (parse-asm-name-specifier uscores first-span parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)