• 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
          • Atc
          • Language
            • Abstract-syntax
              • Tyspecseq
              • Expr
              • Binop
              • Fileset
              • Obj-declor
              • Ident
              • Iconst
              • Obj-adeclor
                • Obj-adeclor-fix
                • Obj-adeclor-case
                • Obj-adeclor-count
                • Obj-adeclorp
                • Obj-adeclor-equiv
                • Obj-adeclor-array
                • Obj-adeclor-pointer
                • Obj-adeclor-none
                • Obj-adeclor-kind
              • Const
              • Fundef
              • Unop
              • File
              • Tag-declon
              • Fun-declor
              • Obj-declon
              • Iconst-length
              • Abstract-syntax-operations
              • Label
              • Struct-declon
              • Initer
              • Ext-declon
              • Fun-adeclor
              • Expr-option
              • Iconst-base
              • Initer-option
              • Iconst-option
              • Tyspecseq-option
              • Stmt-option
              • Scspecseq
              • Param-declon
              • Obj-declon-option
              • File-option
              • Tyname
              • Transunit
              • Fun-declon
              • Transunit-result
              • Param-declon-list
              • Struct-declon-list
              • Expr-list
              • Tyspecseq-list
              • Ident-set
              • Ident-list
              • Ext-declon-list
              • Unop-list
              • Tyname-list
              • Fundef-list
              • Fun-declon-list
              • Binop-list
              • Stmt-fixtypes
              • Expr-fixtypes
            • Integer-ranges
            • Implementation-environments
            • Dynamic-semantics
            • Static-semantics
            • Grammar
            • Integer-formats
            • Types
            • Portable-ascii-identifiers
            • Values
            • Integer-operations
            • Computation-states
            • Object-designators
            • Operations
            • Errors
            • Tag-environments
            • Function-environments
            • Character-sets
            • Flexible-array-member-removal
            • Arithmetic-operations
            • Pointer-operations
            • Bytes
            • Keywords
            • Real-operations
            • Array-operations
            • Scalar-operations
            • Structure-operations
          • 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

Obj-adeclor

Fixtype of abstract object declarators [C17:6.7.7].

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:none → obj-adeclor-none
:pointer → obj-adeclor-pointer
:array → obj-adeclor-array

These are abstract declarators for objects. [C17] does not have a separate syntactic category for them (it just has abstract declarators, for objects and other things), but in our abstract syntax it is useful to differentiate them from other kinds of abstract declarators.

For now we only capture three kinds of abstract object declarators, corresponding to the (non-abstract) object declarators captured in obj-declor: an abstract declarator is like a declarator without the identifier. Abstract declarators are used in type names, which are like declarations without identifiers [C17:6.7.7/2].

From a point of view, it may seem strange to have an explicit value, in this fixtype, for no abstract object declarator, since the fixtype should consist of abstract object declarators. However, this modeling choice is justified by the correspondence between abstract declarators and declarators explained just above.

Subtopics

Obj-adeclor-fix
Fixing function for obj-adeclor structures.
Obj-adeclor-case
Case macro for the different kinds of obj-adeclor structures.
Obj-adeclor-count
Measure for recurring over obj-adeclor structures.
Obj-adeclorp
Recognizer for obj-adeclor structures.
Obj-adeclor-equiv
Basic equivalence relation for obj-adeclor structures.
Obj-adeclor-array
Obj-adeclor-pointer
Obj-adeclor-none
Obj-adeclor-kind
Get the kind (tag) of a obj-adeclor structure.