C object designators.
In C, an object is a region of storage that contains a value [C:3.15]. This notion of object is not in the sense of object-oriented programming (in fact, C is not an object-oriented programming language). Here we introduce a notion of object designator, as an entity that (potentially) designates an object. This is in line with the terminology that defines the notion of lvalue [C:6.3.2/1].
At a low level, an object designator is an address in memory. However, in our model, we introduce a higher-level notion of object designator. We start by defining a notion of abstract addresses, used as top-level object designators for allocated storage, i.e. to designate separate objects in the heap. We also include top-level object designators for global variables, i.e. objects declared with file scope in static storage. We also include top-level object designators for local variables, i.e. objects declarad with block scope in automatic storage. Then we allow object designators to include information that selects sub-objects of the top-level objects, and sub-sub-objects of those sub-objects, and so on. The selection information is of two kinds: an identifier that is the name of a member sub-object of a structure super-object, or a natural number that is the index of an element sub-object of an array super-object.
This should be eventually extended with designators for objects in automatic storage (i.e. stack).