Note that this correspond to the "not null" feature added to Ada 2006 in various places, including pointer type definitions:
type Ptr is not null access Integer; You can also have a regular pointer type and subtype it with not null, but I guess the Ada front-end introduces a generated subtype: type P is access Integer; function F return not null P; The trunk Ada front-end supports this when the -gnat05 flag is used. Laurent On Sat, 2005-11-12 at 09:05 -0800, Per Bothner wrote: > A "function-never-returns-null" attribute doesn't seem like > the right mechanism. Instead, there should be a "never-null" > attribute on pointer types. A "function-never-returns-null" is > just a function whose return-type has the "never-null" attribute. > > A type attribute is much more useful. For example it allows: > String x = shared ? "x" : new String("x"); > // The type of x [in a single-assignment-world] is non-null. > > [If we already have such a mechanism, I apologize.]