|
|
|---|
|
|
|
|---|
Fixtype of addresses.
This is a product type introduced by fty::defprod.
Addresses are mentioned in several places in [C], but there seems to be no specific place in [C] 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 [C] 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.