[Prev][Next][Index][Thread]
Re: Formal semantics for C
Matthias Felleisen writes:
> What's the boundary of a pointer? -- Matthias
While the pointer value itself probably won't include a boundary, the
state of the machine in terms of its "contents of memory" can record
where things are allocated, so that attempts to look at parts of the
memory where a program shouldn't will be classed as undefined.
Naturally, when memory is allocated, you have to specify its actual
placement in an under-determined way; maybe next to other values,
maybe not.
The question of the level at which to stop describing the combined
system of language implementation, operating system etc, is an
interesting one, but one that is easy enough to answer; in my case, I
attempted to model the very minimalist assumptions that the ISO
standard itself makes. (I also made life easier by ignoring the
Library.)
This is fairly careful to specify that doing things like
* looking at uninitialised memory
* writing or reading unallocated memory
* causing signed integers to overflow
* dividing by zero
* breaking the arcane sequence point rules (e.g., i + i++)
all cause undefinedness, at which point your semantics can throw up
its hands, and say "illegal program" / "abort".
The fact that many implementations won't do this, and will instead
continue to look as if they're doing useful work, is neither here nor
there.
Michael.
References: