• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • C
          • Syntax-for-tools
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Compilation-database
            • Printer
            • Output-files
            • Abstract-syntax-operations
            • Implementation-environments
            • Abstract-syntax
            • Concrete-syntax
            • Disambiguation
            • Validation
            • Gcc-builtins
            • Preprocessing
            • Parsing
              • Parser
                • Parse-exprs/decls/stmts
                • Parser-states
                • Parse-external-declaration
                • Parse-cast-expression
                • Parse-expression-or-type-name
                • Parse-postfix-expression
                • Lexer
                • Parse-primary-expression
                • Token-unary-expression-start-p
                • Parse-declaration-specifier
                • Parse-declaration-specifiers
                • Parse-unary-expression-or-parenthesized-type-name
                • Parse-asm-name-specifier
                • Parse-specifier/qualifier
                • Parse-expression-rest
                • Token-type-specifier-keyword-p
                • Parse-fileset
                • Parse-*-external-declaration
                • Parse-declarator-or-abstract-declarator
                • Parse-asm-goto-labels
                • Parse-asm-clobbers
                • Parse-translation-unit
                • Parse-*-label-declaration
                • Token-postfix-expression-rest-start-p
                • Parse-?-asm-name-specifier
                • Parse-*-comma-identifier
                • Parse-postfix-expression-rest
                • Parse-expression
                • Make-expr-unary-with-preinc/predec-ops
                • Parse-*-stringlit
                • Parse-statement
                • Token-struct-declaration-start-p
                • Parse-*-attribute-specifier
                • Parse-initializer-list
                • Parse-file
                • Parse-pointer
                • Parse-label-declaration
                • Parse-array/function-declarator
                • Token-type-qualifier-p
                • Parse-*-asm-qualifier
                • Parse-parameter-declaration
                • Parse-attribute-name
                • Parse-argument-expressions
                • Make-expr-cast/add-or-cast/sub-ambig
                • Parse-struct-or-union-specifier
                • Parse-declaration-or-statement
                • Parse-assignment-expression
                • Parse-asm-clobber
                • Token-specifier/qualifier-start-p
                • Token-primary-expression-start-p
                • Token-function-specifier-p
                • Token-expression-start-p
                • Parse-*-increment/decrement
                • Parse-direct-abstract-declarator
                • Parse-compound-statement
                • Token-to-type-specifier-keyword
                • Parse-unary-expression
                • Parse-argument-expressions-rest
                • Parse-generic-associations-rest
                • Parse-conditional-expression
                • Parse-fileset-loop
                • Parse-direct-abstract-declarator-rest
                • Token-designation?-initializer-start-p
                • Token-declaration-specifier-start-p
                • Parse-designator-list
                • Token-abstract-declarator-start-p
                • Parse-?-asm-output-operands
                • Parse-?-asm-input-operands
                • Parse-struct-declaration
                • Parse-specifier-qualifier-list
                • Parse-parameter-declaration-list
                • Parse-constant-expression
                • Token-type-specifier-start-p
                • Token-type-qualifier-or-attribute-specifier-start-p
                • Parse-static-assert-declaration
                • Parse-direct-declarator
                • Parse-declaration
                • Parse-attribute-parameters
                • Token-unary-operator-p
                • Token-to-unary-operator
                • Token-to-type-qualifier
                • Token-storage-class-specifier-p
                • Token-initializer-start-p
                • Token-direct-abstract-declarator-start-p
                • Token-declarator-start-p
                • Parse-initializer
                • Parse-direct-declarator-rest
                • Token-to-storage-class-specifier
                • Token-to-assignment-operator
                • Token-to-asm-qualifier
                • Token-struct-declarator-start-p
                • Token-direct-declarator-start-p
                • Token-assignment-operator-p
                • Parse-type-qualifier-and-attribute-specifier-list
                • Parse-enumerator-list
                • Parse-designation?-initializer
                • Parse-compound-literal
                • Parse-block-item
                • Token-type-name-start-p
                • Token-to-function-specifier
                • Token-preinc/predec-operator-p
                • Token-multiplicative-operator-p
                • Token-designator-start-p
                • Token-designation-start-p
                • Parse-generic-association
                • Parse-declaration-list
                • Parse-attribute-specifier
                • Parse-asm-output-operands
                • Token-to-relational-operator
                • Token-to-preinc/predec-operator
                • Token-to-multiplicative-operator
                • Token-relational-operator-p
                • Token-equality-operator-p
                • Token-asm-qualifier-p
                • Token-additive-operator-p
                • Parse-asm-statement
                • Parse-asm-input-operands
                • Token-to-equality-operator
                • Token-to-additive-operator
                • Token-shift-operator-p
                • Parser-messages
                • Parse-type-name
                • Parse-struct-declarator-list
                • Parse-struct-declaration-list
                • Parse-relational-expression-rest
                • Parse-multiplicative-expression-rest
                • Parse-logical-or-expression-rest
                • Parse-logical-and-expression-rest
                • Parse-inclusive-or-expression-rest
                • Parse-exclusive-or-expression-rest
                • Parse-equality-expression-rest
                • Parse-array/function-abstract-declarator
                • Parse-additive-expression-rest
                • Token-to-shift-operator
                • Parse-struct-declarator
                • Parse-shift-expression-rest
                • Parse-member-designor
                • Parse-init-declarator-list
                • Parse-init-declarator
                • Parse-designator
                • Parse-and-expression-rest
                • Parse-alignment-specifier
                • Reader
                • Parse-shift-expression
                • Parse-relational-expression
                • Parse-multiplicative-expression
                • Parse-logical-or-expression
                • Parse-logical-and-expression
                • Parse-inclusive-or-expression
                • Parse-exclusive-or-expression
                • Parse-equality-expression
                • Parse-enum-specifier
                • Parse-block-item-list
                • Parse-attribute-list
                • Parse-and-expression
                • Parse-additive-expression
                • Parse-abstract-declarator
                • Parse-member-designor-rest
                • Parse-declarator
                • Parse-attribute
                • Parse-type-qualifier-or-attribute-specifier
                • Parse-enumerator
                • Parse-asm-output-operand
                • Parse-asm-input-operand
            • Atc
            • Transformation-tools
            • Language
            • Representation
            • Insertion-sort
            • Pack
          • Soft
          • Bv
          • Imp-language
          • Ethereum
          • Event-macros
          • Java
          • Riscv
          • Bitcoin
          • Zcash
          • Yul
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Axe
          • Lists-light
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Parser
    • Parse-exprs/decls/stmts

    Parse-asm-input-operand

    Parse an assembler input operand.

    Signature
    (parse-asm-input-operand parstate) 
  → 
(mv erp input span new-parstate)
    Arguments
    parstate — Guard (parstatep parstate).
    Returns
    input — Type (asm-inputp input).
    span — Type (spanp span).
    new-parstate — Type (parstatep new-parstate), given (parstatep parstate).