• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
        • C
          • Syntax-for-tools
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Compilation-database
            • Printer
            • Output-files
            • Abstract-syntax-operations
            • Implementation-environments
              • Ienv
                • Ienvp
                • Ienv-fix
                • Make-ienv
                • Ienv->short-bytes
                • Ienv->llong-bytes
                • Ienv-equiv
                • Ienv->long-bytes
                • Ienv->int-bytes
                • Ienv->plain-char-signedp
                • Change-ienv
                • Ienv->version
              • Ldm-ienv
              • Ienv-ushort-rangep
              • Ienv-ulong-rangep
              • Ienv-ullong-rangep
              • Ienv-uchar-rangep
              • Ienv-sshort-rangep
              • Ienv-slong-rangep
              • Ienv-sllong-rangep
              • Ienv-sint-rangep
              • Ienv-schar-rangep
              • Ienv-uint-rangep
              • Ienv-char-rangep
              • Ienv->uchar-max
              • Ienv->schar-min
              • Ienv->schar-max
              • Ienv->ushort-max
              • Ienv->ulong-max
              • Ienv->ullong-max
              • Ienv->sshort-max
              • Ienv->slong-max
              • Ienv->sllong-max
              • Ienv->uint-max
              • Ienv->sint-max
              • Ienv->sshort-min
              • Ienv->slong-min
              • Ienv->sllong-min
              • Ienv->sint-min
              • Ienv->char-min
              • Ienv->char-max
              • Ienv->std
              • Ienv->gcc
              • Ienv-default
            • Abstract-syntax
            • Concrete-syntax
            • Disambiguation
            • Validation
            • Gcc-builtins
            • Preprocessing
            • Parsing
          • Atc
          • Transformation-tools
          • Language
          • Representation
          • Insertion-sort
          • Pack
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • Java
        • Riscv
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Axe
        • Lists-light
        • 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
version — c::version
short-bytes — posp
int-bytes — posp
long-bytes — posp
llong-bytes — posp
plain-char-signedp — booleanp
Additional Requirements

The following invariant is enforced on the fields:

(and (<= short-bytes int-bytes) 
     (<= int-bytes long-bytes) 
     (<= long-bytes llong-bytes) 
     (<= 2 short-bytes) 
     (<= 2 int-bytes) 
     (<= 4 long-bytes) 
     (<= 8 llong-bytes)) 

We include an indication of the version of C, including whether GCC extensions are enabled or not; see c::version. Currently we mainly support C17, with and without GCC extensions, but we are starting to adding some support for C23 as well.

We assume that bytes are 8 bits, that signed integers use two's complement, and that there are no padding bits or trap representations. Therefore, the characteristics of the integer types are defined by four numbers, i.e. the numbers of bytes of (signed and unsigned) short, int, long, and long long; constraints on those number are derived from [C17:5.2.4.2.1] (for the minima) and [C17:6.2.5/8] (for the increasing sizes).

We also need a flag saying whether the plain char type has the same range as signed char or not [C17:6.2.5/15]. If the flag is false, it has the same range as unsigned char.

We also need a flag saying whether GCC extensions are enabled or not. This could eventually evolve into a rich set of C versions, similar to the options supported by compilers like GCC.

Subtopics

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