[Prev][Next][Index][Thread]
Re: Formal semantics for C
The "unsafe-operations-yield-undefined semantics" for C is
deterministic; it collapses all unsafe computations into the "bottom"
element of the semantic domain (cpo) of program values. This is the
well-known "trivial" approach to handling run-time errors in a
denotational semantics: simply equate all errors with divergence.
If you use a non-determinstic semantics where unsafe operations yield
the set of all possible states, then you cannot use such a semantics
justify any interesting static program analysis. Any potentially
unsafe operation (e.g., an array update or a assignment to field of
heap allocated structure) destroys all of the information that an
analysis tries to propagate. Consider the case of analyzing which
pointer fields in memory can be aliases of one another. As soon as an
unsafe operation has been executed, any pointer field can alias any
other pointer field. Such a semantics is "honest" in modeling the
catastrophic consequences of unsafe operations, but I don't how it
can be used to produce any positive results from the perspective
of program analysis.
-- Corky Cartwright
Follow-Ups:
References: