On 4/29/08 1:31 PM, Joe Buck wrote:
Such a facility can have other uses, particularly for static analysis,
by allowing simple preconditions and postconditions to be specified.
For example:
* a returned pointer is guaranteed to be non-null.
* a supplied pointer is always dereferenced.
* a supplied pointer must be dereferenceable on input, and that pointer
is no longer dereferenceable after return, e.g. free().
Indeed.
Of course, there's a tradeoff between implementation complexity and
features, as always. While these facilities might help the optimizer,
the compiler could also issue warnings if it detects that a precondition
must be violated (and this can also be used to check the correctness
of any user-supplied annotations).
Yes, one of the ideas we discussed is for the compiler to do semantic
checks when compiling the marked-up code to make sure the attributes are
not lying. Since not all the attributes can be strictly checked, we'll
probably end up emitting a mixture of errors and warnings. The latter
will probably take us into false positive problems which we'll have to
address as we find them.
These attributes cannot be checked while compiling client code, of
course. At most we can check that the code being compiled is not
calling any function marked with contradictory attributes.
Diego.
