Re: [RFC] Modeling the behavior of function calls

[Diego Novillo <dnovillo at google dot com>]

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.