• 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
            • Integer-ranges
            • Implementation-environments
              • Uinteger-bit-roles-for-sinteger-bit-roles
              • Sinteger-bit-roles-for-uinteger-bit-roles
              • Integer-format
              • Schar-format
              • Uinteger-sinteger-bit-roles-wfp
              • Sinteger-format
                • Sinteger-format-fix
                • Sinteger-format-equiv
                • Make-sinteger-format
                • Sinteger-format->bits
                • Sinteger-format->signed
                • Change-sinteger-format
                • Sinteger-formatp
                • Sinteger-format->traps
              • Integer-format-llong-wfp
              • Integer-format-short-wfp
              • Integer-format-long-wfp
              • Integer-format-int-wfp
              • Uinteger-format
              • Schar-format->min
              • Char+short+int+long+llong-format
              • Uchar-format
              • Char-format->min
              • Integer-format-inc-sign-tcnpnt
              • Char-format->max
              • Sinteger-format->min
              • Sinteger-bit-role
              • Sinteger-bit-roles-wfp
              • Schar-format->max
              • Signed-format
              • Short-format-16tcnt
              • Llong-format-64tcnt
              • Ienv
              • Uinteger-bit-roles-wfp
              • Uinteger-bit-role
              • Long-format-32tcnt
              • Int-format-16tcnt
              • Uinteger+sinteger-format
              • Uinteger-bit-roles-value-count
              • Sinteger-bit-roles-value-count
              • Sinteger-bit-roles-inc-n-and-sign
              • Uinteger-bit-roles-inc-n
              • Sinteger-format-inc-sign-tcnpnt
              • Sinteger-bit-roles-inc-n
              • Uchar-format->max
              • Char+short+int+long+llong-format-wfp
              • Uinteger-bit-roles-exponents
              • Sinteger-bit-roles-exponents
              • Integer-format->bit-size
              • Char-format
              • Sinteger-bit-roles-sign-count
              • Ienv->char-min
              • Uinteger-format-inc-npnt
              • Ienv->schar-min
              • Ienv->char-size
              • Ienv->char-max
              • Uinteger-format->max
              • Sinteger-format->max
              • Ienv->schar-max
              • Ienv->uchar-max
              • Ienv->short-bit-size
              • Ienv->long-bit-size
              • Ienv->llong-bit-size
              • Schar-format-8tcnt
              • Ienv->int-bit-size
              • Char-format-8u
              • Char8+short16+int16+long32+llong64-tcnt
              • Uchar-format-8
              • Uinteger-bit-role-list
              • Sinteger-bit-role-list
              • Uinteger-sinteger-bit-roles-wfp-of-inc-n-and-sign
            • 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
  • Implementation-environments

Sinteger-format

Fixtype of formats of signed integer objects.

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

Fields
bits — sinteger-bit-role-list
signed — signed-format
traps
Additional Requirements

The following invariant is enforced on the fields:

(sinteger-bit-roles-wfp bits)

This is for signed integer objects other than those of type signed char, which are covered by schar-format. See [C17:6.2.6.2./2].

The format definition includes a list of bit roles, which should be thought as the juxtaposition of the bytes that form the unsigned integer object, in little endian order, i.e. from lower to higher address. The length of the list of bit roles must be a mulitple of CHAR_BIT, which we capture in uchar-format: we express this constraint elsewhere, because we do not have that value available here. The list of bit roles must be well-formed.

The format description also identifies one of the three signed formats. It is not clear from [C17] whether all the signed integer type, within an implementation, use that same signed format, but out model allows them to differ.

We also include a placeholder component meant to define which bit values are trap representations [C17:6.2.6.2/5]. We plan to flesh this out in the future.

Subtopics

Sinteger-format-fix
Fixing function for sinteger-format structures.
Sinteger-format-equiv
Basic equivalence relation for sinteger-format structures.
Make-sinteger-format
Basic constructor macro for sinteger-format structures.
Sinteger-format->bits
Get the bits field from a sinteger-format.
Sinteger-format->signed
Get the signed field from a sinteger-format.
Change-sinteger-format
Modifying constructor for sinteger-format structures.
Sinteger-formatp
Recognizer for sinteger-format structures.
Sinteger-format->traps
Get the traps field from a sinteger-format.