• 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
                • Iconst-fix
                • Make-iconst
                • Iconstp
                • Iconst-equiv
                • Iconst->unsignedp
                • Change-iconst
                • Iconst->length
                • Iconst->base
                • Iconst->value
              • Obj-adeclor
              • 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

Iconst

Fixtype of integer constants [C17:6.4.4.1].

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

Fields
value — natp
base — iconst-base
unsignedp — booleanp
length — iconst-length

For now we define a C integer constants as consisting of a natural number, a base, an unsigned flag, and a length suffix. While this does not cover every syntactic aspect of an integer constant, it covers the important ones.

The natural number is the value. In base 10, the value has a unique syntactic representation, because it is required to start with no 0. In C, 0 is always an octal integer constant, so our abstract syntax here captures a bit more, namely a decimal integer constant 0 that does not exist in C. This is not an issue for now, because our pretty-printer turns that into 0 in the same way as if it were octal.

In base 8, the value has a unique syntactic representation if we assume exactly one leading 0, which is not a significant limitation.

In base 16, the value has a unique syntactc representation if we assume no leading 0s and either lowercase or uppercase letters (i.e. we do not capture the difference between the hexadecimal digits a and A). We also do not capture the distinction between the hexadecimal prefixes 0x and 0X.

We do not capture the distinction between the u and U, which is not very important.

Subtopics

Iconst-fix
Fixing function for iconst structures.
Make-iconst
Basic constructor macro for iconst structures.
Iconstp
Recognizer for iconst structures.
Iconst-equiv
Basic equivalence relation for iconst structures.
Iconst->unsignedp
Get the unsignedp field from a iconst.
Change-iconst
Modifying constructor for iconst structures.
Iconst->length
Get the length field from a iconst.
Iconst->base
Get the base field from a iconst.
Iconst->value
Get the value field from a iconst.