From 9ec080cb2152ca831307b8c4fd825d9acecc4a45 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 5 Sep 2011 15:40:04 +0200 Subject: [PATCH] [multiple changes] 2011-09-05 Marc Sango * sem_ch3.adb (Analyze_Object_Declaration): Remove the wrong test and add the correct test to detect the violation of illegal use of unconstrained string type in SPARK mode. 2011-09-05 Ed Schonberg * sem_ch5.adb (Analyze_Iteration_Specification): Improve error message on an iterator over an array. 2011-09-05 Robert Dewar * lib-xref-alfa.adb: Minor reformatting. From-SVN: r178538 --- gcc/ada/ChangeLog | 15 +++++++++++++++ gcc/ada/lib-xref-alfa.adb | 38 +++++++++++++++++++------------------- gcc/ada/sem_ch3.adb | 23 +++++++++++------------ gcc/ada/sem_ch5.adb | 7 ++++++- 4 files changed, 51 insertions(+), 32 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 22d261d95b3..e267e9b48bc 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,18 @@ +2011-09-05 Marc Sango + + * sem_ch3.adb (Analyze_Object_Declaration): Remove + the wrong test and add the correct test to detect the violation + of illegal use of unconstrained string type in SPARK mode. + +2011-09-05 Ed Schonberg + + * sem_ch5.adb (Analyze_Iteration_Specification): Improve error + message on an iterator over an array. + +2011-09-05 Robert Dewar + + * lib-xref-alfa.adb: Minor reformatting. + 2011-09-05 Robert Dewar * sem_ch3.adb, sem_res.adb, par.adb, par-ch6.adb, g-comlin.adb, diff --git a/gcc/ada/lib-xref-alfa.adb b/gcc/ada/lib-xref-alfa.adb index 8eef5055792..cc0aa3ac84d 100644 --- a/gcc/ada/lib-xref-alfa.adb +++ b/gcc/ada/lib-xref-alfa.adb @@ -586,10 +586,12 @@ package body Alfa is function Is_Alfa_Reference (E : Entity_Id; Typ : Character) return Boolean; - -- Return whether the reference is adequate for this entity + -- Return whether entity reference E meets Alfa requirements. Typ + -- is the reference type. function Is_Alfa_Scope (E : Entity_Id) return Boolean; - -- Return whether the entity or reference scope is adequate + -- Return whether the entity or reference scope meets requirements + -- for being an Alfa scope. function Is_Global_Constant (E : Entity_Id) return Boolean; -- Return True if E is a global constant for which we should ignore @@ -604,35 +606,33 @@ package body Alfa is Typ : Character) return Boolean is begin + -- The only references of interest on callable entities are calls. + -- On non-callable entities, the only references of interest are + -- reads and writes. if Ekind (E) in Overloadable_Kind then - - -- The only references of interest on callable entities are - -- calls. On non-callable entities, the only references of - -- interest are reads and writes. - return Typ = 's'; - elsif Is_Constant_Object (E) then - - -- References to constant objects are not considered in Alfa - -- section, as these will be translated as constants in the - -- intermediate language for formal verification, and should - -- therefore never appear in frame conditions. + -- References to constant objects are not considered in Alfa + -- section, as these will be translated as constants in the + -- intermediate language for formal verification, and should + -- therefore never appear in frame conditions. + elsif Is_Constant_Object (E) then return False; - elsif Present (Etype (E)) and then - Ekind (Etype (E)) in Concurrent_Kind then - - -- Objects of Task type or protected type are not Alfa - -- references. + -- Objects of Task type or protected type are not Alfa references + elsif Present (Etype (E)) + and then Ekind (Etype (E)) in Concurrent_Kind + then return False; + -- In all other cases, result is true for reference/modify cases, + -- and false for all other cases. + else return Typ = 'r' or else Typ = 'm'; - end if; end Is_Alfa_Reference; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 46abaa99839..2953141d30d 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -3267,6 +3267,16 @@ package body Sem_Ch3 is if Is_Indefinite_Subtype (T) then + -- In SPARK, a declaration of unconstrained type is allowed + -- only for constants of type string. + + if Is_String_Type (T) + and then not Constant_Present (Original_Node (N)) then + Check_SPARK_Restriction + ("declaration of object of unconstrained type not allowed", + N); + end if; + -- Nothing to do in deferred constant case if Constant_Present (N) and then No (E) then @@ -3313,21 +3323,10 @@ package body Sem_Ch3 is -- Case of initialization present else - -- Check restrictions in Ada 83 and SPARK modes + -- Check restrictions in Ada 83 if not Constant_Present (N) then - -- In SPARK, a declaration of unconstrained type is allowed - -- only for constants of type string. - - -- Isn't following check the wrong way round??? - - if Nkind (E) = N_String_Literal then - Check_SPARK_Restriction - ("declaration of object of unconstrained type not allowed", - E); - end if; - -- Unconstrained variables not allowed in Ada 83 mode if Ada_Version = Ada_83 diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 5a2d2b37216..81153fa7d30 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -2336,13 +2336,18 @@ package body Sem_Ch5 is if Is_Array_Type (Typ) then if Of_Present (N) then Set_Etype (Def_Id, Component_Type (Typ)); + + elsif Ada_Version < Ada_2012 then + Error_Msg_N + ("missing Range attribute in iteration over an array", N); + else Error_Msg_N ("to iterate over the elements of an array, use OF", N); -- Prevent cascaded errors - Set_Ekind (Def_Id, E_Constant); + Set_Ekind (Def_Id, E_Loop_Parameter); Set_Etype (Def_Id, Etype (First_Index (Typ))); end if; -- 2.30.2