• 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
                • Dec/oct/hex-const-fix
                • Dec/oct/hex-const-case
                • Dec/oct/hex-const-equiv
                • Dec/oct/hex-constp
                • Dec/oct/hex-const-hex
                • Dec/oct/hex-const-oct
                • Dec/oct/hex-const-dec
                • Dec/oct/hex-const-kind
              • Simple-escape
              • Attrib
              • Ident
              • Amb-decl/stmt
              • 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

Dec/oct/hex-const

Fixtype of decimal, octal, and hexadecimal constants [C17:6.4.4.1] [C17:A.1.5].

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

Member Tags → Types
:dec → dec/oct/hex-const-dec
:oct → dec/oct/hex-const-oct
:hex → dec/oct/hex-const-hex

This captures decimal-constant, octal-constant, and hexadecimal-constant in the grammar in [C17]. The grammar does not have a nonterminal that directly corresponds to this fixtype: the three alternatives are given in the grammar rule for integer-constant, along with the optional integer suffixes. In these fixtypes, we factor this a little differently (see iconst).

A decimal constant is completely characterized by its positive integer values. Note that 0 is an octal constant (not a decimal one). Decimal constants cannot have leading zeros, and thus there is a unique list of digits that corresponds to a positive integer.

An octal constant is completely characterized by the number of (one or more) leading zeros and by its non-negative integer value. The non-negative integer value determines the non-zero-starting list of digits that follow the leading zeros. Note that the octal constant 0 is represented, in this fixtype, as consisting of one leading 0 and the value 0: the value 0 determines the empty non-zero-starting list of digits.

A hexadecimal constant consists of a prefix and a list of digits (which should be non-empty). The fixtype hex-digit-char-list corresponds, in the grammar in [C17], to hexadecimal-constant without hexadecimal-prefix. The non-decimal hexadecimal digits may be uppercase and lowercase, so in order to capture all the information from the abstract syntax we use lists of digits in this fixtype, which can be of course converted to integer values.

Subtopics

Dec/oct/hex-const-fix
Fixing function for dec/oct/hex-const structures.
Dec/oct/hex-const-case
Case macro for the different kinds of dec/oct/hex-const structures.
Dec/oct/hex-const-equiv
Basic equivalence relation for dec/oct/hex-const structures.
Dec/oct/hex-constp
Recognizer for dec/oct/hex-const structures.
Dec/oct/hex-const-hex
Dec/oct/hex-const-oct
Dec/oct/hex-const-dec
Dec/oct/hex-const-kind
Get the kind (tag) of a dec/oct/hex-const structure.