• 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
            • Dynamic-semantics
            • Static-semantics
            • Grammar
            • Integer-formats
            • Types
            • Portable-ascii-identifiers
            • Values
            • Integer-operations
            • Computation-states
            • Object-designators
              • Objdesign
              • Address
                • Address-fix
                • Address-equiv
                • Make-address
                • Change-address
                • Address->number
                • Addressp
              • Object-disjointp
              • Objdesign-option
            • 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
  • Object-designators

Address

Fixtype of addresses.

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

Fields
number — natp

Addresses are mentioned in several places in [C17], but there seems to be no specific place in [C17] that defines them. Nonetheless, based on how they are mentioned, it is quite clear that an address is essentially a hardware address, i.e. a number that identifies a memory location, even though [C17] does not prescribe a particular representation.

For now we treat addresses as essentially abstract entities, whose only purpose is to identify objects in memory. We model addresses as natural numbers, but we do not use any properties of natural numbers. This fixtype wraps these natural numbers, for better abstraction.

As explained in object-designators, we use these addresses to designate only whole objects in the heap, and not their sub-objects.

Subtopics

Address-fix
Fixing function for address structures.
Address-equiv
Basic equivalence relation for address structures.
Make-address
Basic constructor macro for address structures.
Change-address
Modifying constructor for address structures.
Address->number
Get the number field from a address.
Addressp
Recognizer for address structures.