The attribute reference 'Old ppears within a postcondition, but refers to
an entity in the enclosing subprogram. If the prefix is a component of a formal
its expansion might generate actual subtypes that may be referenced in an inner
context, and which must be elaborated within the subprogram itself. As a result
we create a declaration for the prefix, insert it in the enclosing subprogram
itself and expand it at once. This is properly an expansion activity but it has
to be performed now to prevent out-of-order issues in the back-end.
the following commands
gnatmake -q -gnat12 -gnata my_test
my_test
must yield:
Max = 9
Min = 0
Average = 4
Find 0 in T1 4
Find 9 in T2 4
---
with Simple_Unc_Arrays; use Simple_Unc_Arrays;
with Ada.Text_IO; use Ada.Text_IO;
procedure My_Test is
T1 : Table := (10, (5, 1, 3, 0, 9, 8, 2, 7, 4, 6));
T2 : Table := (10, (4, 8, 6, 9, 0, 1, 7, 2, 5, 3));
T3 : Table (10);
begin
Put_Line ("Max = " & Max (T1)'img);
Put_Line ("Min = " & Min (T1)'img );
Put_Line ("Average = " & Average (T1)'img);
Put_Line ("Find 0 in T1 " & Search (T1, 0)'img);
Put_Line ("Find 9 in T2 " & Search (T2, 9)'img);
T3 := Add (T1, T2);
pragma Assert (for all I in 1 .. T3.Last => T3.V (I) = 9);
T3 := Bubble_Sort (T1);
Quick_Sort (T1);
pragma Assert (T1 = T3);
end;
---
package Simple_Unc_Arrays is
-- This should be a generic parameter
type Value is new Integer; -- should be range <>;
-- This is declaring arrays with a fixed first bound of 1
type Values is array (Positive range <>) of Value;
type Table (Last : Natural) is record
V : Values (1 .. Last);
end record;
---------
-- Add --
---------
function Add (A, B : Table) return Table
with Pre => Same_Range (A, B),
Post => Same_Range (Add'Result, A)
and then (for all J in 1 .. A.Last =>
(Add'Result.V (J) = A.V (J) + B.V (J)));
-------------
-- Reverse --
-------------
Procedure Inverse (A : in out Table)
with Post => (for all J in 1 .. A.Last => (A.V (J) = A.V'Old (A.Last - J +
1)));
-- Reverses the content of A
---------
-- Min --
---------
function Min (A : Table) return Value
with
Pre => not Empty (A),
Post => (for all J in 1 .. A.Last => Min'Result <= A.V (J))
and then (for some J in 1 .. A.Last => Min'Result = A.V (J));
-- Returns the minimum value occurring in A
---------
-- Max --
---------
function Max (A : Table) return Value
with
Pre => not Empty (A),
Post => (for all J in 1 .. A.Last => Max'Result >= A.V (J))
and then (for some J in 1 .. A.Last => Max'Result = A.V (J));
-- Returns the maximun value occurring in A
-------------
-- Average --
-------------
function Average (A : Table) return Value
with
Pre => not Empty (A),
Post => Min (A) <= Average'Result
and then Max (A) >= Average'Result;
-- Returns the average value in A. Here, the given postcondition does not
-- describe completely the value returned.
------------
-- Search --
------------
function Search (A : Table; V : Value) return Natural
with Post => (Search'Result = 0 and then Not_In (A, V, 1 ,A.Last))
or else (A.V (Search'Result) = V
and then Not_In (A, V, 1, Search'Result-1));
-- Returns the first index at which value V occurs in array A, or else 0
-----------------
-- Bubble_Sort --
-----------------
function Bubble_Sort (A: Table) return Table
with Post => (for all J in 1 .. A.Last - 1 =>
Bubble_Sort'Result.V (J) <= Bubble_Sort'Result.V (J+1))
and then (for all J in 1 .. A.Last =>
(for some K in 1 .. A.Last => A.V (J) = Bubble_Sort'Result.V
(K)));
-- Sorts an array in increasing order by using bubble sort
----------------
-- Quick_Sort --
----------------
Procedure Quick_Sort (A: in out Table);
-- with Post => (for all J in 1 .. A.Last - 1 => A.V (J) <= A.V (J+1))
-- and then (for all J in 1 .. A.Last =>
-- (for some K in 1 .. A.Last => A.V'Old (J) = A.V (K)));
-- Sorts an array in increasing order by using quick sort
-----------------
-- utililities --
-----------------
function Empty (A : Table) return Boolean is (1 > A.Last);
function Same_Range (A, B : Table) return Boolean is (A.Last = B.Last);
function Not_In (A : Table;
V : Value;
Low : Positive;
Up : Natural)
return Boolean is
(Up > A.Last or else (for all J in Low .. Up => A.V (J) /= V));
procedure Swap (V, W : in out Value)
with Post => (V = W'Old and then W = V'Old);
-- Swaps two values V and W
end Simple_Unc_Arrays;
---
package body Simple_Unc_Arrays is
---------
-- Add --
---------
function Add (A, B : Table) return Table is
begin
return C : Table (A.Last) do
for I in 1 .. A.Last loop
pragma Assert
((for all J in 1 .. I-1 => C.V (J) = A.V (J) + B.V (J))
-- and then (for all K in I .. A.Last => C.V (K) = C.V'old (K)));
);
C.V (I) := A.V (I) + B.V (I);
end loop;
end return;
end Add;
-------------
-- Reverse --
-------------
procedure Inverse (A : in out Table) is
Low : Positive := 1;
High : Natural := A.Last;
begin
while Low < High loop
pragma Assert
(for all J in 1 .. Low - 1 => (A.V (J) = A.V'Old (A.Last - J + 1))
and then (for all J in Low -1 .. A.Last => (A.V (J) = A.V'Old (J)))
);
Swap (A.V (Low), A.V (High));
Low := Low + 1;
High := High - 1;
end loop;
end Inverse;
---------
-- Min --
---------
function Min (A : Table) return Value is
Res : Value := A.V (1);
begin
for I in 2 .. A.Last loop
pragma Assert (for all J in 1 .. I - 1 => Res <= A.V (J));
if Res > A.V (I) then
Res := A.V (I);
end if;
end loop;
return Res;
end Min;
---------
-- Max --
---------
function Max (A : Table) return Value is
begin
return Res : Value := A.V (1) do
for I in 2 .. A.Last loop
pragma Assert (for all J in 1 .. I - 1 => Res >= A.V (J));
if Res < A.V (I) then
Res := A.V (I);
end if;
end loop;
end return;
end Max;
-------------
-- Average --
-------------
function Average (A : Table) return Value is
Sum : Value := 0;
begin
for I in 1 .. A.Last loop
Sum := Sum + A.V (I);
end loop;
return Sum / Value (A.Last);
end Average;
------------
-- Search --
------------
function Search (A : Table; V : Value) return Natural is
Pos : Natural := 0;
begin
for I in A.V'range loop
pragma Assert (for all J in 1 .. I - 1 => A.V (J) /= V);
if A.V (I) = V then
Pos := I;
exit;
end if;
end loop;
return Pos;
end Search;
-----------------
-- Bubble_Sort --
-----------------
function Bubble_Sort (A: Table) return Table is
Bull : Boolean := True;
Res : Table := A;
begin
while Bull loop
Bull := False;
for I in 1 .. Res.Last - 1 loop
if Res.V (I + 1) < Res.V (I) then
Swap (Res.V (I), Res.V (I+1));
Bull := True;
end if;
end loop;
end loop;
return Res;
end Bubble_Sort;
----------------
-- Quick_Sort --
----------------
procedure Quick_Sort (A : in out Table) is
procedure Q_S (First, Last : Natural);
-- for the recursive call
procedure Q_S (First, Last : Natural) is
Pivot_Index, Right, Left : Natural;
Pivot_Value: Value;
begin
if First < Last then
Pivot_Index := (First + Last + 1) / 2;
Pivot_Value := A.V (Pivot_Index);
Left := First;
Right := Last;
loop
while Left < Last and then A.V (Left) < Pivot_Value loop
Left := Left + 1;
end loop;
while Right > First and then A.V (Right) > Pivot_Value loop
Right := Right - 1;
end loop;
exit when Left >= Right;
Swap (A.V (Left), A.V (Right));
end loop;
if Right > First then
Q_S (First, Right - 1);
end if;
if Left < Last then
Q_S (Left, Last);
end if;
end if;
end Q_S;
begin
Q_S (1, A.Last);
end Quick_Sort;
procedure Swap (V, W : in out Value) is
Tmp : Value;
begin
Tmp := V;
V := W;
W := Tmp;
end Swap;
end Simple_Unc_Arrays;
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-31 Ed Schonberg <schonb...@adacore.com>
* sem_attr.adb (Analyze_Attribute, case 'Old): If prefix may be a
discriminated component of an actual, expand at once to prevent
ouf-of-order references with generated subtypes.
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 178358)
+++ sem_attr.adb (working copy)
@@ -1939,7 +1939,7 @@
-- Analyze prefix and exit if error in analysis. If the prefix is an
-- incomplete type, use full view if available. Note that there are
-- some attributes for which we do not analyze the prefix, since the
- -- prefix is not a normal name.
+ -- prefix is not a normal name, or else needs special handling.
if Aname /= Name_Elab_Body
and then
@@ -1950,6 +1950,8 @@
Aname /= Name_UET_Address
and then
Aname /= Name_Enabled
+ and then
+ Aname /= Name_Old
then
Analyze (P);
P_Type := Etype (P);
@@ -3772,6 +3774,12 @@
end if;
Check_E0;
+
+ -- Prefix has not been analyzed yet, and its full analysis will take
+ -- place during expansion (see below).
+
+ Preanalyze_And_Resolve (P);
+ P_Type := Etype (P);
Set_Etype (N, P_Type);
if No (Current_Subprogram) then
@@ -3852,6 +3860,24 @@
end if;
end Check_Local;
+ -- The attribute ppears within a pre/postcondition, but refers to
+ -- an entity in the enclosing subprogram. If it is a component of a
+ -- formal its expansion might generate actual subtypes that may be
+ -- referenced in an inner context, and which must be elaborated
+ -- within the subprogram itself. As a result we create a declaration
+ -- for it and insert it at the start of the enclosing subprogram
+ -- This is properly an expansion activity but it has to be performed
+ -- now to prevent out-of-order issues.
+
+ if Nkind (P) = N_Selected_Component
+ and then Has_Discriminants (Etype (Prefix (P)))
+ then
+ P_Type := Base_Type (P_Type);
+ Set_Etype (N, P_Type);
+ Set_Etype (P, P_Type);
+ Expand (N);
+ end if;
+
------------
-- Output --
------------
