• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
        • Soft
        • C
          • Syntax-for-tools
            • Disambiguator
            • Abstract-syntax
              • Expr
              • Exprs/decls/stmts
              • Type-spec
              • Binop
              • Stmt
              • Amb-expr/tyname
              • Dirdeclor
              • Unop
              • Asm-stmt
                • Make-asm-stmt
                • Asm-stmt-equiv
                • Asm-stmtp
                • Change-asm-stmt
                • Asm-stmt->clobbers
                • Asm-stmt->uscores
                • Asm-stmt->template
                • Asm-stmt->outputs
                • Asm-stmt->num-colons
                • Asm-stmt->labels
                • Asm-stmt->inputs
                • Asm-stmt->quals
                • Asm-stmt-fix
                • Asm-stmt-count
              • Dec/oct/hex-const
              • Simple-escape
              • Attrib
              • Ident
              • Amb-decl/stmt
              • Dirabsdeclor
              • Decl-spec
              • Structdecl
              • Fundef
              • Transunit-ensemble
              • Asm-name-spec
              • Amb-declor/absdeclor
              • Param-declor
              • Declor
              • Type-qual
              • Absdeclor
              • Strunispec
              • Stor-spec
              • Keyword-uscores
              • Align-spec
              • Label
              • Expr-option
              • Spec/qual
              • Lsuffix
              • Hex-frac-const
              • Desiniter
              • Tyname
              • Iconst
              • Dirabsdeclor-option
              • Dec-frac-const
              • Dec-core-fconst
              • Extdecl
              • Amb?-declor/absdeclor
              • Isuffix
              • Initdeclor
              • Hex-core-fconst
              • Const-expr-option
              • Attrib-spec
              • Structdeclor
              • Escape
              • Decl
              • Amb?-expr/tyname
              • Ident-option
              • Bin-expo
              • Absdeclor-option
              • Statassert
              • Param-declon
              • Member-designor
              • Initer-option
              • Initer
              • Fsuffix
              • Enumspec
              • Declor-option
              • Const
              • Hex-quad
              • Eprefix
              • Const-expr
              • Block-item
              • Oct-escape
              • Inc/dec-op
              • Fun-spec
              • Dec-expo
              • Cprefix-option
              • Asm-name-spec-option
              • Amb?-decl/stmt
              • S-char
              • Isuffix-option
              • Genassoc
              • Fundef-option
              • Fsuffix-option
              • Fconst
              • Eprefix-option
              • Dec-expo-option
              • Cprefix
              • C-char
              • Type-spec-option
              • Sign-option
              • Iconst-option
              • Asm-output
              • Asm-input
              • Const-option
              • Usuffix
              • Univ-char-name
              • Transunit
              • Hprefix
              • Enumer
              • Designor
              • Attrib-name
              • Sign
              • Asm-qual
              • Typequal/attribspec
              • Dec-expo-prefix
              • Bin-expo-prefix
              • Stringlit
              • Cconst
              • Expr/tyname
              • Decl/stmt
              • Declor/absdeclor
              • Asm-clobber
              • Typequal/attribspec-list
              • Decl-spec-list
              • Stringlit-list
              • Spec/qual-list
              • Inc/dec-op-list
              • Desiniter-list
              • S-char-list
              • Param-declon-list
              • Decl-list
              • C-char-list
              • Block-item-list
              • Typequal/attribspec-list-list
              • Structdeclor-list
              • Structdecl-list
              • Initdeclor-list
              • Genassoc-list
              • Filepath-transunit-map
              • Extdecl-list
              • Expr-list
              • Enumer-list
              • Attrib-spec-list
              • Type-spec-list
              • Ident-list
              • Asm-qual-list
              • Asm-output-list
              • Asm-input-list
              • Asm-clobber-list
              • Stor-spec-list
              • Ident-set
              • Ident-option-set
              • Eprefix-option-list
              • Designor-list
              • Attrib-list
            • Parser
            • Validator
            • Printer
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Defpred
            • Output-files
            • Abstract-syntax-operations
            • Validation-information
            • Implementation-environments
            • Concrete-syntax
            • Unambiguity
            • Ascii-identifiers
            • Preprocessing
            • Abstraction-mapping
          • Atc
          • Language
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Abstract-syntax
  • Exprs/decls/stmts

Asm-stmt

Fixtype of assembler statements.

This is a product type introduced by fty::defprod.

Fields
uscores — keyword-uscores
quals — asm-qual-list
template — stringlit-list
num-colons — natp
outputs — asm-output-list
inputs — asm-input-list
clobbers — asm-clobber-list
labels — ident-list

This is a GCC extension. Our abstract syntax of assembler statements is based on their definition in the ABNF grammar, which is in turn derived from the GCC documentation. As in the grammar, we unify the representation of basic and extended assembler statements. The grammar contains four nested optional parts (output operands etc.); the nesting is such that any prefix of the sequence of four parts, ranging from no parts to all four parts, may be present. In the abstract syntax, we include a component that counts the number of parts, or equivalently the number of colons, since each part starts with a colon. Then each part consists of a list of things, four lists, one per part. If num-colons is less than 4, the fourth list must be empty; if num-colons is less than 3, the fourth and third lists must be empty; and so on, but we do not explicitly capture these constraints in the fixtype.

Subtopics

Make-asm-stmt
Basic constructor macro for asm-stmt structures.
Asm-stmt-equiv
Basic equivalence relation for asm-stmt structures.
Asm-stmtp
Recognizer for asm-stmt structures.
Change-asm-stmt
Modifying constructor for asm-stmt structures.
Asm-stmt->clobbers
Get the clobbers field from a asm-stmt.
Asm-stmt->uscores
Get the uscores field from a asm-stmt.
Asm-stmt->template
Get the template field from a asm-stmt.
Asm-stmt->outputs
Get the outputs field from a asm-stmt.
Asm-stmt->num-colons
Get the num-colons field from a asm-stmt.
Asm-stmt->labels
Get the labels field from a asm-stmt.
Asm-stmt->inputs
Get the inputs field from a asm-stmt.
Asm-stmt->quals
Get the quals field from a asm-stmt.
Asm-stmt-fix
Fixing function for asm-stmt structures.
Asm-stmt-count
Measure for recurring over asm-stmt structures.