• 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
            • Disambiguator
            • Abstract-syntax
            • Parser
            • Validator
            • Printer
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Defpred
            • Output-files
            • Abstract-syntax-operations
            • Validation-information
            • Implementation-environments
              • Ienv
              • Ushort-rangep
              • Ullong-rangep
              • Sshort-rangep
              • Sllong-rangep
              • Ulong-rangep
              • Uint-rangep
              • Slong-rangep
              • Sint-rangep
              • Ushort-max
              • Ulong-max
              • Ullong-max
              • Uint-max
              • Uchar-rangep
              • Sshort-min
              • Sllong-min
              • Schar-rangep
              • Char-min
              • Char-max
              • Sshort-max
              • Slong-min
              • Slong-max
              • Sllong-max
              • Sint-min
              • Sint-max
              • Uchar-max
              • Schar-min
              • Schar-max
              • Ienv-default
            • Concrete-syntax
            • Unambiguity
            • Ascii-identifiers
            • 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
  • Syntax-for-tools

Implementation-environments

Implementation environments for the C syntax for tools.

These are similar in purpose to the implementation environments that are part of our formalization of C. We need to use that notion also for our C syntax for tools, specifically for certain tools that operate on it. Eventually, for this C syntax for tools, we should just use those implementation environment that are part of our formalization of C, but for this C syntax for tools we need some information that is not part of those implementation environments, and thus we define a temporary version of implementation environments exclusively for use by the C syntax of tools. When the implementation environments in the C formalization are extended to contain all the information needed for the C syntax for tools, we will eliminate this temporary definition and use those instead.

Subtopics

Ienv
Fixtype of implementation environments.
Ushort-rangep
Check if a mathematical integer is in the range of (i.e. representable in) type signed short.
Ullong-rangep
Check if a mathematical integer is in the range of (i.e. representable in) type signed llong.
Sshort-rangep
Check if a mathematical integer is in the range of (i.e. representable in) type signed short.
Sllong-rangep
Check if a mathematical integer is in the range of (i.e. representable in) type signed llong.
Ulong-rangep
Check if a mathematical integer is in the range of (i.e. representable in) type signed long.
Uint-rangep
Check if a mathematical integer is in the range of (i.e. representable in) type signed int.
Slong-rangep
Check if a mathematical integer is in the range of (i.e. representable in) type signed long.
Sint-rangep
Check if a mathematical integer is in the range of (i.e. representable in) type signed int.
Ushort-max
Maximum mathematical integer value of type unsigned short.
Ulong-max
Maximum mathematical integer value of type unsigned long.
Ullong-max
Maximum mathematical integer value of type unsigned long long.
Uint-max
Maximum mathematical integer value of type unsigned int.
Uchar-rangep
Check if a mathematical integer is in the range of (i.e. representable in) type unsigned char.
Sshort-min
Minimum mathematical integer value of type signed short.
Sllong-min
Minimum mathematical integer value of type signed long long.
Schar-rangep
Check if a mathematical integer is in the range of (i.e. representable in) type signed char.
Char-min
Minimum mathematical integer value of the type char.
Char-max
Maximum mathematical integer value of the type char.
Sshort-max
Maximum mathematical integer value of type signed short.
Slong-min
Minimum mathematical integer value of type signed long.
Slong-max
Maximum mathematical integer value of type signed long.
Sllong-max
Maximum mathematical integer value of type signed long long.
Sint-min
Minimum mathematical integer value of type signed int.
Sint-max
Maximum mathematical integer value of type signed int.
Uchar-max
Maximum mathematical integer value of type unsigned char.
Schar-min
Minimum mathematical integer value of type signed char.
Schar-max
Maximum mathematical integer value of type signed char.
Ienv-default
A default implementation environment.