• 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
              • Disambiguator
              • Unambiguity
                • Abstract-syntax-unambp
                  • Exprs/decls/stmts-unambp
                  • Filepath-transunit-map-unambp
                  • Transunit-ensemble-unambp
                  • Declor/absdeclor-unambp
                  • Type-spec-list-unambp
                  • Fundef-option-unambp
                  • Extdecl-list-unambp
                  • Expr/tyname-unambp
                  • Code-ensemble-unambp
                  • Fundef-unambp
                  • Decl/stmt-unambp
                  • Transunit-unambp
                  • Extdecl-unambp
                  • Typequal/attribspec-list-unambp
                  • Typequal/attribspec-list-list-unambp
                  • Typequal/attribspec-unambp
                  • Struni-spec-unambp
                  • Struct-declor-unambp
                  • Struct-declor-list-unambp
                  • Struct-declon-unambp
                  • Struct-declon-list-unambp
                  • Statassert-unambp
                  • Spec/qual-unambp
                  • Spec/qual-list-unambp
                  • Param-declor-unambp
                  • Param-declon-unambp
                  • Param-declon-list-unambp
                  • Member-designor-unambp
                  • Initer-option-unambp
                  • Initdeclor-unambp
                  • Initdeclor-list-unambp
                  • Genassoc-list-unambp
                  • Expr-option-unambp
                  • Enumer-list-unambp
                  • Dirabsdeclor-unambp
                  • Dirabsdeclor-option-unambp
                  • Desiniter-list-unambp
                  • Designor-list-unambp
                  • Declor-option-unambp
                  • Decl-spec-list-unambp
                  • Const-expr-unambp
                  • Const-expr-option-unambp
                  • Block-item-unambp
                  • Block-item-list-unambp
                  • Attrib-spec-unambp
                  • Attrib-spec-list-unambp
                  • Attrib-list-unambp
                  • Asm-output-unambp
                  • Asm-output-list-unambp
                  • Asm-input-list-unambp
                  • Amb-expr/tyname-unambp
                  • Amb-decl/stmt-unambp
                  • Amb-declor/absdeclor-unambp
                  • Align-spec-unambp
                  • Absdeclor-option-unambp
                  • Type-spec-unambp
                  • Tyname-unambp
                  • Stmt-unambp
                  • Label-unambp
                  • Initer-unambp
                  • Genassoc-unambp
                  • Expr-unambp
                  • Expr-list-unambp
                  • Enumer-unambp
                  • Enum-spec-unambp
                  • Dirdeclor-unambp
                  • Desiniter-unambp
                  • Designor-unambp
                  • Declor-unambp
                  • Decl-unambp
                  • Decl-spec-unambp
                  • Decl-list-unambp
                  • Comp-stmt-unambp
                  • Attrib-unambp
                  • Asm-stmt-unambp
                  • Asm-input-unambp
                  • Absdeclor-unambp
                • Abstract-syntax-unambp-additional-theorems
                • Type-spec-list-unambp-of-sublists
                • Expr-unambp-of-operation-on-expr-unambp
            • Validation
            • Gcc-builtins
            • Preprocessing
            • Parsing
          • 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
  • Unambiguity

Abstract-syntax-unambp

Definition of the unambiguity predicates.

We use fty::deffold-reduce to define these predicates concisely.

The :default value is t, because constructs like identifiers and constants are unambiguous; ambiguities may only exist in expressions, type names, etc.

We override the boilerplate to return nil on the fixtype cases with ambig in their names, the fixtypes amb-..., and the dummy base case of dirabsdeclor; although the latter is not properly an ambiguous construct, we take the opportunity to exclude it here from consideration whenever unambiguous constructs are concerned (which is for most of the tools, except for parser and disambiguator).

We override the boilerplate to return t on GCC attributes, attribute specifiers, and assembler constructs.

Subtopics

Exprs/decls/stmts-unambp
Filepath-transunit-map-unambp
Transunit-ensemble-unambp
Declor/absdeclor-unambp
Type-spec-list-unambp
Fundef-option-unambp
Extdecl-list-unambp
Expr/tyname-unambp
Code-ensemble-unambp
Fundef-unambp
Decl/stmt-unambp
Transunit-unambp
Extdecl-unambp
Typequal/attribspec-list-unambp
Typequal/attribspec-list-list-unambp
Typequal/attribspec-unambp
Struni-spec-unambp
Struct-declor-unambp
Struct-declor-list-unambp
Struct-declon-unambp
Struct-declon-list-unambp
Statassert-unambp
Spec/qual-unambp
Spec/qual-list-unambp
Param-declor-unambp
Param-declon-unambp
Param-declon-list-unambp
Member-designor-unambp
Initer-option-unambp
Initdeclor-unambp
Initdeclor-list-unambp
Genassoc-list-unambp
Expr-option-unambp
Enumer-list-unambp
Dirabsdeclor-unambp
Dirabsdeclor-option-unambp
Desiniter-list-unambp
Designor-list-unambp
Declor-option-unambp
Decl-spec-list-unambp
Const-expr-unambp
Const-expr-option-unambp
Block-item-unambp
Block-item-list-unambp
Attrib-spec-unambp
Attrib-spec-list-unambp
Attrib-list-unambp
Asm-output-unambp
Asm-output-list-unambp
Asm-input-list-unambp
Amb-expr/tyname-unambp
Amb-decl/stmt-unambp
Amb-declor/absdeclor-unambp
Align-spec-unambp
Absdeclor-option-unambp
Type-spec-unambp
Tyname-unambp
Stmt-unambp
Label-unambp
Initer-unambp
Genassoc-unambp
Expr-unambp
Expr-list-unambp
Enumer-unambp
Enum-spec-unambp
Dirdeclor-unambp
Desiniter-unambp
Designor-unambp
Declor-unambp
Decl-unambp
Decl-spec-unambp
Decl-list-unambp
Comp-stmt-unambp
Attrib-unambp
Asm-stmt-unambp
Asm-input-unambp
Absdeclor-unambp