• 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
              • Const
              • Fundef
              • Unop
              • File
              • Tag-declon
              • Fun-declor
              • Obj-declon
                • Obj-declon-fix
                • Obj-declon-equiv
                • Make-obj-declon
                • Obj-declonp
                • Change-obj-declon
                • Obj-declon->tyspec
                • Obj-declon->scspec
                • Obj-declon->init?
                • Obj-declon->declor
              • 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-declon

Fixtype of object declarations [C17:6.7].

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

Fields
scspec — scspecseq
tyspec — tyspecseq
declor — obj-declor
init? — initer-option

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

For now we define an object declaration as consisting of a storage class specification sequence, a type specifier sequence, an object declarator, and an optional initializer.

For now we model no type qualifiers, no function specifiers, and no alignment specifiers.

Subtopics

Obj-declon-fix
Fixing function for obj-declon structures.
Obj-declon-equiv
Basic equivalence relation for obj-declon structures.
Make-obj-declon
Basic constructor macro for obj-declon structures.
Obj-declonp
Recognizer for obj-declon structures.
Change-obj-declon
Modifying constructor for obj-declon structures.
Obj-declon->tyspec
Get the tyspec field from a obj-declon.
Obj-declon->scspec
Get the scspec field from a obj-declon.
Obj-declon->init?
Get the init? field from a obj-declon.
Obj-declon->declor
Get the declor field from a obj-declon.