Uninitialized out parameters.

[ah...@marriott.org]

Hi,

Is this a GNAT (GPL-2015) bug or my not understanding Ada?

I was surprised that I could compile
procedure Test (V : out Positive) is null;

and even more by the results of calling the procedure

V : Positive;
begin
Test (V);
Ada.Text_IO.Put_Line ("V:" & V'img);

The value zero is output, which because V is positive should be impossible.

I would have thought that null procedures with out parameters would fail to compile.

Opinions anyone?

MfG
Ahlan

[riea...@comcast.net]

There are two issues here. One is whether this program is 'legal' Ada. Short answer, there are many, many more Ada programs than Ada programs that "make sense." This is just another example. The second issue? Are compilers allowed to warn you about this code? Sure. But why allow it? Right now I am working on a generic package where GNAT warns me that some of the code in an instantiation will Constraint_Error if executed. But it can only be reached if the generic is instantiated with a generic formal such that the code will not raise an error. I'll add pragma Suppress (Index_Check) before I'm done, but for now, if a fifth warning shows up, I'll know to be concerned. ;-)

Is it possible to write code which will only raise an error if Fermat's Last Theorem is false? Sure, I've done it. I did it just to show that a proposal for elaboration order checking was flawed. The ARG navigates a fine line between allowing all useful programs to be written, and requiring compilers to do tons of checks for unintended errors. Look for example at 6.5.1 Nonreturning procedures.

Is it meaningful for a nonreturning procedure to set an out parameter? Should a compiler be required to make that check? (Either for or against.) The answer is that Ada is used in many contexts where nonreturning procedures are meaningful--I normally did so in flight guidance software. For manned aircraft you certainly want to be sure that the main processing loop never exits while power is on. But the intersection of a parameter check and nonreturning procedures (whatever you would expect that check to do) is just making unnecessary work for the compiler. Similarly a procedure may be called with an out parameter that already has a value. So it is the programmer's job to deal with the union of these issues in a sensible way.

Could GNAT (or any other) compiler provide a warning? Sure, and it does:

procedure NoSet is
Counter: Positive;
procedure Reset (V : out Positive;
User_Check: Boolean := True) is
function Ask_User return Boolean is begin return True; end; -- TBD
begin
if User_Check and then Ask_User then return; end if;
V := 1;
end Reset;
begin
Reset(Counter);
end NoSet;

gnatmake -O3 noset.adb
gcc -c -O3 noset.adb
noset.adb:7:42: warning: "out" parameter "V" not set before return
gnatbind -x noset.ali
gnatlink noset.ali -O3

Compilation finished at Tue Apr 05 09:13:54

[ah...@marriott.org]

Hi,
You write

"Could GNAT (or any other) compiler provide a warning? Sure, and it does: "

but that's my whole point - GNAT doesn't in my example.
And I feel that it should.
A null procedure is NOT a non-returning procedure - it does return and moreover in my example actually returns an illegal value!

In my gpr I compile with
package Compiler is
for Default_Switches ("ada") use ("-O1", "-gnatQ", "-gnato", "-g", "-gnat12",
"-gnatwcehijkmopruvz.c.n.p.t.w.x", "-gnatykmpM120");
end Compiler;

Is there a warning that I need to explicitly switch on in order that GNAT checks for out parameters in null procedures?

MfG
Ahlan

[G.B.]

On 05.04.16 14:02, ah...@marriott.org wrote:
> Ada.Text_IO.Put_Line ("V:" & V'img);
>
> The value zero is output, which because V is positive should be impossible.

Addressing just this issue: the line is calling
implementation defined attribute 'IMG, which can
do as it pleases. The Ada type attribute 'Image
takes a value of type Positive'Base, which includes 0,
which is why outputting 0 is perfectly fine.

(It's not a subtype attribute, but a type attribute,
if this makes sense.)

[ah...@marriott.org]

The issue here is not whether or not 'img fails but the fact that V is returned with a value out of range.
But even that is not the point I'm trying to make.
I am suggesting that it ought not to be possible to define a null procedure that has out parameters without some form of warning being issued.

[Mark Lorenzen]

On Tuesday, April 5, 2016 at 4:07:18 PM UTC+2, ah...@marriott.org wrote:
>
> In my gpr I compile with
> package Compiler is
> for Default_Switches ("ada") use ("-O1", "-gnatQ", "-gnato", "-g", "-gnat12",
> "-gnatwcehijkmopruvz.c.n.p.t.w.x", "-gnatykmpM120");
> end Compiler;
>
> Is there a warning that I need to explicitly switch on in order that GNAT checks for out parameters in null procedures?

You have enabled a lot of warnings, but why not start with -gnatwa? That is usually a good starting point and then you can add further swicthes. Try to add -gnatwf that should enable warnings about unreferenced formal parameters.

You can also use the GNATcheck tool to check your coding standard. GNATcheck is able to find some instances of unassigned out parameters (rule Unassigned_OUT_Parameters). If you want to be 100% sure that you do not have uninitialized variable or out parameters, you will need to use a stronger static analysis tool.

Regards,
Mark L

[G.B.]

On 06.04.16 10:19, ah...@marriott.org wrote:
> On Tuesday, April 5, 2016 at 6:19:47 PM UTC+2, G.B. wrote:
>> On 05.04.16 14:02, ah...@marriott.org wrote:
>>> Ada.Text_IO.Put_Line ("V:" & V'img);
>>>
>>> The value zero is output, which because V is positive should be impossible.
>>
>> Addressing just this issue: the line is calling
>> implementation defined attribute 'IMG, which can
>> do as it pleases. The Ada type attribute 'Image
>> takes a value of type Positive'Base, which includes 0,
>> which is why outputting 0 is perfectly fine.
>>
>> (It's not a subtype attribute, but a type attribute,
>> if this makes sense.)
>
> The issue here is not whether or not 'img fails but the fact that V is returned with a value out of range.

The issue is rather, I think, whether V is returned at all.
There would have to be an assignment within the null procedure.

> But even that is not the point I'm trying to make.
> I am suggesting that it ought not to be possible to define a null procedure that has out parameters without some form of warning being issued.

I think the usual answer is that the compiler is not a mind
reader and the best you could get is a warning. Who knows?
Maybe the technical requirements are such that the programmer
uses a procedure like Test as a placeholder, maybe its existence
is dictated by an abstract type, maybe a null procedure really
should do nothing at all, which includes not touching V.

[AdaMagica]

Hm, from the point of view of the RM, the RM has nothing to say about warnings - only whether the code is legal or illegal. So giving warnings is up to the compiler.

Now for scalar variables, the RM says, in mode variables are copied in, out mode variables are copied out, in out variables are both. So as I understand, even a null procedure with an out parameter does something to the parameter: it copies out an uninitialized variable (which can have any value whatsoever). Language lawyers - please?

[ah...@marriott.org]

On Wednesday, April 6, 2016 at 1:37:41 PM UTC+2, AdaMagica wrote:
> Hm, from the point of view of the RM, the RM has nothing to say about warnings - only whether the code is legal or illegal. So giving warnings is up to the compiler.
>
> Now for scalar variables, the RM says, in mode variables are copied in, out mode variables are copied out, in out variables are both. So as I understand, even a null procedure with an out parameter does something to the parameter: it copies out an uninitialized variable (which can have any value whatsoever). Language lawyers - please?

In the annotated RM, in the section concerning Null Procedures, it says "There are no null functions because the return value has to be constructed somehow; a function that always raises Program_Error doesn't seem very useful or worth the complication"
If there are no null functions because a return value has to be constructed then surely the same applies to null procedures that have out parameters. These too should be prohibited because they too require that a value has to be constructed. If not prohibited then at least Program_Error should be raised and ideally a warning is generated by the compiler warning that calling the null procedure will always raise Program_Error.
Currently GNAT simply returns "something" - zero or null that sometimes escapes detection. This is NOT desirable.

[Mark Lorenzen]

On Wednesday, April 6, 2016 at 3:44:08 PM UTC+2, ah...@marriott.org wrote:
> If there are no null functions because a return value has to be constructed then surely the same applies to null procedures that have out parameters. These too should be prohibited because they too require that a value has to be constructed. If not prohibited then at least Program_Error should be raised and ideally a warning is generated by the compiler warning that calling the null procedure will always raise Program_Error.
> Currently GNAT simply returns "something" - zero or null that sometimes escapes detection. This is NOT desirable.

It would of course be useful if GNAT would issue a warning, but it would only solve the (somewhat conceived) example of a null procedure with an out parameter. There are more interesting situations where an out parameter or variable may end up having an undefined value.

If you want to write bullet-proff software you should maybe have a look at the SPARK 2014 subset of Ada and the related tools (GNATprove).

Anyway, you can suggest to AdaCore that GNAT should issue a warning in your example.

Regards,
Mark L

[G.B.]

On 06.04.16 15:44, ah...@marriott.org wrote:
> If there are no null functions because a return value has to be constructed then surely the same applies to null procedures that have out parameters. These too should be prohibited because they too require that a value has to be constructed.

Arguably, procedures do not need to construct a value
for an out parameter whenever they do not assign any:
the actual parameter is allocated already, whether it
is initialized or not.
Does the RM require an assignment happening as part
of the call?

[Niklas Holsti]

On 16-04-06 14:44 , Dennis Lee Bieber wrote:
> On Wed, 6 Apr 2016 12:17:05 +0200, "G.B." <bau...@futureapps.invalid>
> declaimed the following:

>
>> On 06.04.16 10:19, ah...@marriott.org wrote:
>>> On Tuesday, April 5, 2016 at 6:19:47 PM UTC+2, G.B. wrote:
>>>> On 05.04.16 14:02, ah...@marriott.org wrote:
>>>>> Ada.Text_IO.Put_Line ("V:" & V'img);
>>>>>
>>>>> The value zero is output, which because V is positive should be impossible.
>>>>
>>>> Addressing just this issue: the line is calling
>>>> implementation defined attribute 'IMG, which can
>>>> do as it pleases. The Ada type attribute 'Image
>>>> takes a value of type Positive'Base, which includes 0,
>>>> which is why outputting 0 is perfectly fine.
>>>>
>>>> (It's not a subtype attribute, but a type attribute,
>>>> if this makes sense.)
>>>
>>> The issue here is not whether or not 'img fails but the fact that V is returned with a value out of range.
>>
>> The issue is rather, I think, whether V is returned at all.
>> There would have to be an assignment within the null procedure.
>>

> Which could be a case if the compiler used copy-in/copy-out semantics
> for scalars (or just copy-out for the test sample). GNAT, if I recall, uses
> reference semantics,

Then GNAT would be in violation of the Ada standard -- see RM 6.2(3/3).
I hope and believe that is not the case...

--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .

[Randy Brukardt]

"G.B." <bau...@futureapps.invalid> wrote in message
news:ne2ngo$uea$1...@dont-email.me...

> On 06.04.16 10:19, ah...@marriott.org wrote:

...

>> But even that is not the point I'm trying to make.
>> I am suggesting that it ought not to be possible to define a null
>> procedure
>> that has out parameters without some form of warning being issued.
>
> I think the usual answer is that the compiler is not a mind
> reader and the best you could get is a warning. Who knows?
> Maybe the technical requirements are such that the programmer
> uses a procedure like Test as a placeholder, maybe its existence
> is dictated by an abstract type, maybe a null procedure really
> should do nothing at all, which includes not touching V.

I agree with Georg here. It *seems* like checks like the one Ahlan is
suggesting are a good idea, until you trip over one. (The check in Ada that
every function have at least one return is a similar idea, which causes no
end of trouble.)

I can think of at least three reasons why one might write a null procedure
with an out parameter:
(1) The null procedure body is a TBD placeholder. It will be replaced with a
real body at some future point, but we still want to compile.
(2) The out parameter isn't used for some implementations. This often comes
up when there are multiple parameters. (We ran into this commonly in Claw,
although we usually used in out parameters in such cases to avoid
de-initializing objects.) The situation is that some objects need additional
return information and others don't:
procedure Do_Something (Obj : in out Object; Result : in out
Result_Type; Extra_Info : out Natural);
Extra_Info is only used if Result has a particular value.
(3) The null procedure is used in an interface. In that case, giving a body
isn't possible.

I think you could make a case that all of these are better written some
other way, but that's irrelevant, in that each of these could happen in real
code, and making a legality check would break that code. (Thus, making it
illegal would probably be considered too incompatible for future Ada, unless
of course we discovered some semantic problem that doing that would fix.)

The Ada Standard has nothing to say about warnings (other than for pragmas).
Perhaps some future version of Ada will change that, but as of now, every
warning is implementation-defined, and thus it they don't have anything to
do with the language. (That is, talk to your vendor about warnings.)

Randy.

[Stefan...@uni-weimar.de]

On Wed, 6 Apr 2016, ah...@marriott.org wrote:

> In the annotated RM, in the section concerning Null Procedures, it says
> "There are no null functions because the return value has to be
> constructed somehow; a function that always raises Program_Error doesn't
> seem very useful or worth the complication" If there are no null
> functions because a return value has to be constructed then surely the
> same applies to null procedures that have out parameters. These too

> should be prohibited [...]

This seems to be right. It does not make much sense to allow the
declaration of

procedure X(Formal: out T) is null;

while prohibiting the declaration of

function Y return R is null;

The point is, you can neither call X nor Y. Semantically, both statements

X(Actual);
Actual := Y;

are equally useless, or at least their effect is equally undefined.
Allowing the declaration of X, but prohibiting the declaration of Y is
inconsistent.


If people really think they need to declare something like the above
procedure X, a revised Ada standard could allow declarations such as

procedure X(Formal: T) is raise;

and

function Y return T is raise;

where "is raise" stands for "raise Program_Error". That may sometimes come
handy in the context of inheritance, or so.


-------- I love the taste of Cryptanalysis in the morning! --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----

[Randy Brukardt]

"Dennis Lee Bieber" <wlf...@ix.netcom.com> wrote in message
news:c7t9gb1972nrm7e64...@4ax.com...
...

>>The issue is rather, I think, whether V is returned at all.
>>There would have to be an assignment within the null procedure.
>>

> Which could be a case if the compiler used copy-in/copy-out semantics
> for scalars (or just copy-out for the test sample). GNAT, if I recall,
> uses

> reference semantics, and as out-only wouldn't be checking the initial
> value
> on entry.

Scalars in Ada are always by-copy, so the *effect* always have to be
copy-in/copy-out, regardless of how that's implemented. (I can't speak for
GNAT, but Janus/Ada makes copies at the call-site if we want to/need to use
by-reference parameter passing.)

The rules for whether an out parameter is initialized (and if so, how) are
complicated - see 6.4.1(12-15). 6.4.1(15) most likely applies in this case
(assuming no Default_Value aspect is involved), and that says that the value
is uninitialized. And of course the value of an uninitialized object can be
anything.

Randy.

[Jeffrey R. Carter]

On Tuesday, April 5, 2016 at 4:07:18 PM UTC+2, ah...@marriott.org wrote:
>
> In my gpr I compile with
> package Compiler is
> for Default_Switches ("ada") use ("-O1", "-gnatQ", "-gnato", "-g", "-gnat12",
> "-gnatwcehijkmopruvz.c.n.p.t.w.x", "-gnatykmpM120");
> end Compiler;

I think the first question is whether the procedure is called at all. Since the
compiler knows it's null and so is supposed to do nothing, and since
optimization is turned on, it seems a reasonable optimization to eliminate the
call. The the value passed to 'Img is whatever bits you get from an
uninitialized variable of the type.

--
Jeff Carter
"You can never forget too much about C++."
115

[Randy Brukardt]

I said:
> It *seems* like checks like the one Ahlan is suggesting are a good idea,
> until you trip over one. (The check in Ada that every function have at
> least one return is a similar idea, which causes no end of trouble.)

On top of that, exactly what would the check be? Which of the following
ought to be illegal?

procedure Foo1 (Obj : out Positive) is null;

procedure Foo2 (Obj : out Positive) is
begin
null;
end Foo2;

Debug : constant Boolean := False;
procedure Foo3 (Obj : out Positive) is
begin
if Debug then
Put_Line ("Foo3 called");
end if;
end Foo3;

Foo1 and Foo2 are semantically identical (Foo1 is in fact defined in terms
of Foo2). But it is clearly a lot harder for an Ada compiler to detect Foo2
compared to Foo1 (and changing between them is common). Having different
legality for Foo1 and Foo2 would be annoying at best.

Obviously, detecting Foo3 is even harder for a compiler, but again,
semantically it is identical to Foo2. So where do you stop? And why?

Randy.

[Randy Brukardt]

<Stefan...@uni-weimar.de> wrote in message
news:alpine.DEB.2.20.1604062240350.29458@debian...

[Niklas Holsti]

On 16-04-06 23:53 , Stefan...@uni-weimar.de wrote:
> On Wed, 6 Apr 2016, ah...@marriott.org wrote:
>
>> In the annotated RM, in the section concerning Null Procedures, it
>> says "There are no null functions because the return value has to be
>> constructed somehow; a function that always raises Program_Error
>> doesn't seem very useful or worth the complication" If there are no
>> null functions because a return value has to be constructed then
>> surely the same applies to null procedures that have out parameters.
>> These too should be prohibited [...]
>
> This seems to be right. It does not make much sense to allow the
> declaration of
>
> procedure X(Formal: out T) is null;

If T has default initialization (which is now possible even for scalars,
with the Default_Value aspect), that seems reasonable to me. It is
equivalent to having "is begin null; end X;" as the body, which has a
well-defined effect when there is a Default_Value, by RM 6.4.1(13.1/4)
and other paragraphs in 6.4.1.

> while prohibiting the declaration of
>
> function Y return R is null;

For a function, a null body is illegal (no "return" statement). Ok,
that's a nit-pick; without that rule, this could be as defined as X,
under the same circumstances.

> The point is, you can neither call X nor Y. Semantically, both statements
>
> X(Actual);
> Actual := Y;
>
> are equally useless, or at least their effect is equally undefined.

Not undefined in the case of X, when the type has a default value.

[Dmitry A. Kazakov]

Simple, the rules must be same as ones for the function return, which
are exemplarily annoying, nevertheless considered OK.

To the question "where to stop" there is a simple rule:

no false negatives

Thus is you want to stop at Foo3, the outcome is "illegal" regardless
Debug value.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

[Randy Brukardt]

<Stefan...@uni-weimar.de> wrote in message
news:alpine.DEB.2.20.1604062240350.29458@debian...

On Wed, 6 Apr 2016, ah...@marriott.org wrote:

>> In the annotated RM, in the section concerning Null Procedures, it says
>> "There are no null functions because the return value has to be
>> constructed somehow; a function that always raises Program_Error doesn't
>> seem very useful or worth the complication" If there are no null
>> functions because a return value has to be constructed then surely the
>> same applies to null procedures that have out parameters. These too
>> should be prohibited [...]
>
>This seems to be right. It does not make much sense to allow the
>declaration of
>
> procedure X(Formal: out T) is null;
>
>while prohibiting the declaration of
>
> function Y return R is null;

Playing Devil's Advocate here, the latter always raises Program_Error; if
you really meant that there are better ways (see below). The former does
nothing at all other than deinitialize its actual parameter. So they're not
really the same thing.

> The point is, you can neither call X nor Y. Semantically, both statements
>
> X(Actual);
> Actual := Y;
>
>are equally useless, or at least their effect is equally undefined.

No, both are very well-defined. And there is nothing wrong in either case
with making a call (so long as Actual is not used afterwards.

I have *lots* of procedures for which one or more actuals are meaningless
after the call, and better not be touched. (The case where *all* parameters
are like that is of course pathological, but to have one of of several is
pretty common.)

>Allowing the declaration of X, but prohibiting the declaration of Y is
>inconsistent.

Maybe, but there is a big difference: allowing the declaration of Y is new
feature that would be a lot of work for implementers and is 100% useless.
(Again, there is a better way to write a function that always raises
Program_Error, see below.) Whereas *disallowing* the declaration of X would
be additional work for implementers (and now would also be incompatible).
The null procedure feature itself has many obvious uses, and you are talking
about a tiny corner case.

I can see that it might have made sense to disallow out parameters when the
feature was defined, but I don't think we ever thought of it. As I noted in
another message, a null procedure is semantically just a short-hand for
"begin null; end;" and I don't think we considered having *different*
Legality Rules for it.

And it's definitely too late now; breaking existing code (especially
interface declarations) for this issue seems like a non-starter. Such a rule
would do very little to reduce this problem (it happens to me periodically
for normal procedures), so the incompatibility would just not be tolerable.

And of course, changing the rules to raise Program_Error, as the OP
suggested, would be even more of a nonstarter as a runtime incompatibility.
No one would want programs that work fine today start raising Program_Error
because some object that is never used got de-initialized. We had a similar
case that involved a real semantic problem with access types, and we
eventually decided to make it illegal (rather than raise Program_Error or
make it erroneous) as the best of a bad set of choices (Program_Error was
the least liked of all). [We did choose Program_Error for a similar case,
but that was because we assumed that there were no such programs as "scalar
with Default_Value" was first added in Ada 2012, not so for things in Ada 83
(or Ada 2005).]

Ada 83 got the handling of uninitialized objects wrong (including this case
of out parameters) for a language which defaults to "safe". We're pretty
much stuck with that today, changes would break almost all existing code.
That's too bad, but I guess it just shows that no language is perfect.

>If people really think they need to declare something like the above
>procedure X, a revised Ada standard could allow declarations such as
>
> procedure X(Formal: T) is raise;
>
>and
>
> function Y return T is raise;
>
>where "is raise" stands for "raise Program_Error". That may sometimes come
>handy in the context of inheritance, or so.

(1) The above null procedure X does not and would never raise Program_Error,
so the first part of this doesn't make any sense.

(2) The latter can be written in current Ada 2012: (that is, with TC1
implemented)
function Y return T is (raise Program_Error);

which is both clearer and hardly any longer. I can't imagine why we'd add
another feature just to save two parens and a name (that it actually helps
to make explicit).

Randy.

[ah...@marriott.org]

We use -gnatwu which includes -gnatwf

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
news:ne3un4$5qf$1...@gioia.aioe.org...
...

> Simple, the rules must be same as ones for the function return, which are
> exemplarily annoying, nevertheless considered OK.

Umm, no, they're not considered "OK". We don't feel comfortable removing the
function return Legality Rule (some people view that as moving to a less
safe version of Ada), but we surely don't want any more like that. (We've
learned our lesson, I hope.)

Randy.

[Georg Bauhaus]

On 06/04/16 22:53, Stefan...@uni-weimar.de wrote:
> If people really think they need to declare something like the above procedure X, a revised Ada standard could allow declarations such as
>
> procedure X(Formal: T) is raise;
>
> and
>
> function Y return T is raise;
>
> where "is raise" stands for "raise Program_Error". That may sometimes come handy in the context of inheritance, or so.

Two prominent use cases will suggest this hammer won't fly ;-)
if used as a replacement:

1. Testing, or integration builds at various incomplete stages:
one couldn't test part B of a program if part A of the program,
calling X, always raises before it gets to B.

2. OPENSTEP style programming (a.k.a. Cocoa) as an example, meaning
that, conceptually, whenever an object is not (yet) defined (nil),
but then receives a message, nothing happens.

So, if a procedure does nothing and out comes nothing,
then it doesn't do harm either, at least if programmers know what
to expect. They fill in the blanks later.

I'd rather accept null functions in the set of oddities of
Ada than be forced to always have finished everything.
Note that raising disallows stubs like

procedure X (Formal : out T) is
begin
pragma Warning ("TODO: compute a value for out Formal!")
null;
end X;

Treating warnings as errors should help with strict rejection
rules where the projects demand them.

[Stefan...@uni-weimar.de]

The OP suggested change the semantic and raise Programm_Error for the
above null procedure. I just suggested a possible syntax if you really
want to indicate "this is not yet implemented and will raise an exception
if you dare calling it."

On the other hand, the existing Ada 2012 syntax will *almost* serve that
purpose.

procedure X(Formal: out T) is null with pre => False;

-- Procedure X will be implemented in a forthcoming update.
-- Until then, don't even think of calling it!

Alas, this seems only to work if T is tagged and the aspect is
"pre'class", rather than plain "pre".

> (2) The latter can be written in current Ada 2012: (that is, with TC1
> implemented)
> function Y return T is (raise Program_Error);

Great! I wasn't aware of that. I always thought, the expression in
brackets had to be of type T.

Stefan

[AdaMagica]

Am Donnerstag, 7. April 2016 11:57:02 UTC+2 schrieb Stefan...@uni-weimar.de:

> > (2) The latter can be written in current Ada 2012: (that is, with TC1
> > implemented)
> > function Y return T is (raise Program_Error);
>
> Great! I wasn't aware of that. I always thought, the expression in
> brackets had to be of type T.
>
> Stefan

A raise_expression matches any type. See RM.

[Randy Brukardt]

"AdaMagica" <christ-u...@t-online.de> wrote in message
news:51041ba8-3243-46bc...@googlegroups.com...

Right. One can think of it sort of like "bottom" in a functional language -
it represents the "not a value" of any type. (And touch it and you die.)

OTOH, like me, you may not want to think of functional languages much. ;-)

Randy.

[Dmitry A. Kazakov]

Yes, better think it typed!

It is same as an IEEE float which values are real U {NaN, +Inf, -Inf}.
Propagating exceptions is a sort of value.

In

function Y return T is (raise Program_Error);

we assume that T consists of values of T values and exceptions of all
sorts. That is weakly typed, a bit. But it also a way how to spell Y's
post-condition: "T or Program_Error raised" could be a type Y returns.
That would make an implementation (raise Constraint_Error) illegal.