• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
              • Dec/oct/hex-const
              • Simple-escape
              • Attrib
              • Ident
              • Amb-decl/stmt
                • Amb-decl/stmt-equiv
                • Amb-decl/stmt-p
                • Make-amb-decl/stmt
                • Change-amb-decl/stmt
                • Amb-decl/stmt->stmt
                • Amb-decl/stmt->decl
                • Amb-decl/stmt-fix
                • Amb-decl/stmt-count
              • 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
            • Ascii-identifiers
            • Unambiguity
            • 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

Amb-decl/stmt

Fixtype of ambiguous declarations or statements.

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

Fields
decl — decl
stmt — expr

A block item may be a declaration or a statement, but there is a complex syntactic overlap between declarations and statements, specifically expression statements. For instance, if I1, ..., In are identifiers, I1(I2(...(In)...)); could be either a declaration or a statement. It is a declaration if I1 is a type specifier (a typedef name) and (I2(...(In)...)) is a declarator of I2, which is a function with a parameter I3, which is a function with a parameter I4, and so on; here I3, I4, etc. are type specifiers (typedef names). It is instead an expression statement if I1 is a function, called with argument I2(...(In)...), which is itself a function call, and so on. There are also other, more complex patterns, for example similar to the ones above but with multiple function arguments.

So, similarly to amb-expr/tyname and amb-declor/absdeclor, here we define a fixtype of ambiguous declarations or statements, which contain both the declaration and the expression (since the only ambiguity is with expression statements). These two components should look the same in concrete syntax, but we do not enforce that in this fixtype definition.

Subtopics

Amb-decl/stmt-equiv
Basic equivalence relation for amb-decl/stmt structures.
Amb-decl/stmt-p
Recognizer for amb-decl/stmt structures.
Make-amb-decl/stmt
Basic constructor macro for amb-decl/stmt structures.
Change-amb-decl/stmt
Modifying constructor for amb-decl/stmt structures.
Amb-decl/stmt->stmt
Get the stmt field from a amb-decl/stmt.
Amb-decl/stmt->decl
Get the decl field from a amb-decl/stmt.
Amb-decl/stmt-fix
Fixing function for amb-decl/stmt structures.
Amb-decl/stmt-count
Measure for recurring over amb-decl/stmt structures.