|
|
|---|
|
|
|
|---|
Fixtype of pointers.
This is a tagged union type, introduced by fty::deftagsum.
Pointers are mentioned in several places in [C],
but there seems to be no specific place in [C] that defines them.
Nonetheless, we can get a precise picture from various places.
[C:6.2.5/20] says that pointer types describe objects
whose values provide references to entities.
[C:6.3.2.3] specifies several things about pointers;
in particular, it talks about null pointers.
Thus, the picture is the following:
a pointer is either an object designator or a null pointer
(see the discussion in object-designators
about lower-level addresses vs. higher-level object designators).
However, in our defensive semantics, we also distinguish between
non-null pointers that designate existing objects
and non-null pointers that designate non-existing objects:
the latter arise when such objects disappear,
e.g. because they are in allocated storage and
Thus, we formalize a pointer as being either null or dangling or validly designating an object. The term `valid' here is perhaps not ideal, because in a sense a null pointer is a perfectly ``valid'' value, which may be used in well-written C code, so long as it is not deferenced. We may find a better term in the future, but for now here `valid' should be interpreted as `valid for dereferencing'.
The notion of pointer defined here is slighly different from the notion of pointer value defined in value. The latter consists of a pointer as defined here, plus a (referenced) type. Nonetheless, the pointer as defined here is the core of a pointer value, with the type being additional metadata. Thus, when clear from context, sometimes we will call `pointers' what are actually pointer values.