When permitted by the bounds/base type of the subtype, mark it as being in ALFA, and similarly for the entity used to iterate over a loop.
Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-04 Yannick Moy <m...@adacore.com> * sem_ch3.adb (Array_Type_Declaration): move test for type in ALFA after index creation; mark unconstrained base array type generated as being in/not in ALFA as well (Make_Index): mark subtype created as in/not in ALFA * sem_ch5.adb (Analyze_Iteration_Scheme): mark entity for iterating over a loop as in/not in ALFA, depending on its type and form of loop iteration.
Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 177325) +++ sem_ch3.adb (working copy) @@ -4678,12 +4678,6 @@ Check_SPARK_Restriction ("subtype mark required", Index); end if; - if Present (Etype (Index)) - and then not Is_In_ALFA (Etype (Index)) - then - T_In_ALFA := False; - end if; - -- Add a subtype declaration for each index of private array type -- declaration whose etype is also private. For example: @@ -4738,6 +4732,12 @@ Make_Index (Index, P, Related_Id, Nb_Index); + if Present (Etype (Index)) + and then not Is_In_ALFA (Etype (Index)) + then + T_In_ALFA := False; + end if; + -- Check error of subtype with predicate for index type Bad_Predicated_Subtype_Use @@ -4878,6 +4878,7 @@ Set_Component_Type (Base_Type (T), Element_Type); Set_Packed_Array_Type (T, Empty); Set_Is_In_ALFA (T, T_In_ALFA); + Set_Is_In_ALFA (Base_Type (T), T_In_ALFA); if Aliased_Present (Component_Definition (Def)) then Check_SPARK_Restriction @@ -16538,6 +16539,19 @@ then Set_Is_Non_Static_Subtype (Def_Id); end if; + + -- By default, consider that the subtype is in ALFA if its base type + -- is in ALFA. + + Set_Is_In_ALFA (Def_Id, Is_In_ALFA (Base_Type (Def_Id))); + + -- In ALFA, all subtypes should have a static range + + if Nkind (R) = N_Range + and then not Is_Static_Range (R) + then + Set_Is_In_ALFA (Def_Id, False); + end if; end if; -- Final step is to label the index with this constructed type Index: sem_ch5.adb =================================================================== --- sem_ch5.adb (revision 177274) +++ sem_ch5.adb (working copy) @@ -2082,6 +2082,17 @@ Set_Etype (Id, Etype (DS)); end if; + -- The entity for iterating over a loop is always in ALFA if + -- its type is in ALFA, and it is not an iteration over + -- elements of a container using the OF syntax. + + if Is_In_ALFA (Etype (Id)) + and then (No (Iterator_Specification (N)) + or else not Of_Present (Iterator_Specification (N))) + then + Set_Is_In_ALFA (Id); + end if; + -- Treat a range as an implicit reference to the type, to -- inhibit spurious warnings.