GCC 4.4.0 Postcondition oddity.

xorque

unread,

Jul 4, 2009, 8:27:35 AM7/4/09

to

Hello.

See the following:

package P is

procedure X (A : out Natural);
pragma Postcondition (A >= 10);

end P;

package body P is

procedure X (A : out Natural) is
begin
A := 20;
end X;

end P;

$ gcc44 -gnatwadleG -gnatVa -gnato -gnata -gnatW8 -gnatiw -
gnaty2aAbdefhiklnprStu -c p.adb
p.ads:4:25: warning: "A" may be referenced before it has a value

Anyone else seeing this (strange) warning?

xorque

unread,

Jul 6, 2009, 8:15:41 AM7/6/09

to

Nobody else seeing this?

Looks like a compiler bug to me.

Georg Bauhaus

unread,

Jul 6, 2009, 8:39:48 AM7/6/09

to

xorque schrieb:

> Nobody else seeing this?
>
> Looks like a compiler bug to me.

$ gcc -gnatv -gnatwadleG -gnatVa -gnato -gnata -gnatW8 -gnatiw
-gnaty2aAbdefhiklnprStu -c p.adb

GNAT GPL 2009 (20090519)
Copyright 1992-2009, Free Software Foundation, Inc.

Compiling: p.adb (source file time stamp: 2009-07-06 12:35:23)
8 lines: No errors
$ uname -a
Linux kartoffel 2.6.24-24-server #1 SMP Wed Apr 15 15:41:09 UTC 2009
x86_64 GNU/Linux

xorque

unread,

Jul 6, 2009, 9:45:17 AM7/6/09

to

> $ gcc -gnatv -gnatwadleG -gnatVa -gnato -gnata -gnatW8 -gnatiw
> -gnaty2aAbdefhiklnprStu -c p.adb
>
> GNAT GPL 2009 (20090519)
> Copyright 1992-2009, Free Software Foundation, Inc.
>
> Compiling: p.adb (source file time stamp: 2009-07-06 12:35:23)
> 8 lines: No errors
> $ uname -a
> Linux kartoffel 2.6.24-24-server #1 SMP Wed Apr 15 15:41:09 UTC 2009
> x86_64 GNU/Linux

Thanks.

Looks like I'll be filing a bug report...

Tero Koskinen

unread,

Jul 6, 2009, 11:46:33 AM7/6/09

to

I think the error is already fixed in FSF gcc -trunk:

$ gcc -gnatv -gnatwadleG -gnatVa -gnato -gnata -gnatW8 -gnatiw -gnaty2aAbdefhiklnprStu -c p.adb

GNAT 4.5.0 20090416 (experimental)

Compiling: p.adb (source file time stamp: 2009-07-06 15:43:53)
9 lines: No errors
$

--
Tero Koskinen - http://iki.fi/tero.koskinen/

Samuel Tardieu

unread,

Jul 6, 2009, 1:15:23 PM7/6/09

to

>>>>> "xorque" == xorque <xorqu...@googlemail.com> writes:

xorque> Looks like I'll be filing a bug report...

Out of curiosity, what does the output of "gcc -gnatadg" look like?

Here, it is: (with a recent FSF GCC)

% gcc -c -gnatadg p.adb
with system.system__assertions;

package body p is

procedure p__x (a : out natural) is

procedure p__x___postconditions is
begin
if not (a >= 10) then
$system__assertions__raise_assert_failure (
"Postcondition failed at p.ads:4");
end if;
return;
end p__x___postconditions;
begin
a := 20;
p__x___postconditions;
return;
end p__x;
begin
null;
end p;

xorque

unread,

Jul 6, 2009, 5:25:20 PM7/6/09

to

On my system:

a := 20;
p__x___postconditions;
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
return;

Is missing. I'll try compiling trunk!

Thanks.