• 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
              • Schar-format
              • Uinteger-sinteger-bit-roles-wfp
              • Integer-format
              • Sinteger-format
              • 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
                • Ienv-fix
                • Ienvp
                • Ienv->char+short+int+long+llong-format
                • Make-ienv
                • Ienv-equiv
                • Change-ienv
              • Uinteger-bit-role
              • Long-format-32tcnt
              • Int-format-16tcnt
              • Uinteger-bit-roles-wfp
              • 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
              • Ienv->sshort-min
              • Ienv->sllong-min
              • Char-format-8u
              • Ienv->ushort-max
              • Ienv->ulong-max
              • Ienv->ullong-max
              • Ienv->uint-max
              • Ienv->sshort-max
              • Ienv->slong-min
              • Ienv->slong-max
              • Ienv->sllong-max
              • Ienv->sint-min
              • Ienv->sint-max
              • 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

Ienv

Fixtype of implementation environments.

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

Fields
char+short+int+long+llong-format — char+short+int+long+llong-format
Additional Requirements

The following invariant is enforced on the fields:

(char+short+int+long+llong-format-wfp 
     char+short+int+long+llong-format) 

For now this only contains a few components, but we plan to add more components.

Currently we include the format of the three character types, and the standard signed integer types and their unsigned counterparts.

The reason for using the ``intermediate'' fixtype char+short+int+long+llong-format is the same as explained in integer-format about the ``intermediate'' fixtype used there. We may eliminate this at some point.

Subtopics

Ienv-fix
Fixing function for ienv structures.
Ienvp
Recognizer for ienv structures.
Ienv->char+short+int+long+llong-format
Get the char+short+int+long+llong-format field from a ienv.
Make-ienv
Basic constructor macro for ienv structures.
Ienv-equiv
Basic equivalence relation for ienv structures.
Change-ienv
Modifying constructor for ienv structures.