This is the mail archive of the
gcc@gcc.gnu.org
mailing list for the GCC project.
Re: [RFC] Modeling the behavior of function calls
- From: "Andrew Pinski" <pinskia at gmail dot com>
- To: "Diego Novillo" <dnovillo at google dot com>
- Cc: "Joe Buck" <Joe dot Buck at synopsys dot com>, gcc at gcc dot gnu dot org, "Xinliang David Li" <davidxl at google dot com>, "Robert Hundt" <rhundt at google dot com>
- Date: Tue, 29 Apr 2008 11:03:40 -0700
- Subject: Re: [RFC] Modeling the behavior of function calls
- References: <48161FD8.4000302@google.com> <20080429173155.GM3596@synopsys.com> <481761ED.3090301@google.com>
On Tue, Apr 29, 2008 at 10:59 AM, Diego Novillo <dnovillo@google.com> wrote:
> 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.
We already have the second one, called nonnull
The first one is recorded as PR 20318.
Thanks,
Andrew Pinski