diff options
author | Arnaud Charlet <charlet@gcc.gnu.org> | 2011-09-05 15:40:04 +0200 |
---|---|---|
committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2011-09-05 15:40:04 +0200 |
commit | 9ec080cb2152ca831307b8c4fd825d9acecc4a45 (patch) | |
tree | f6cdb02884910b21f8b1c6e72a3d780e87a56745 | |
parent | 94bbf008bae624219030c93f6b74def28677e0a7 (diff) | |
download | gcc-9ec080cb2152ca831307b8c4fd825d9acecc4a45.zip gcc-9ec080cb2152ca831307b8c4fd825d9acecc4a45.tar.gz gcc-9ec080cb2152ca831307b8c4fd825d9acecc4a45.tar.bz2 |
[multiple changes]
2011-09-05 Marc Sango <sango@adacore.com>
* 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 <schonberg@adacore.com>
* sem_ch5.adb (Analyze_Iteration_Specification): Improve error
message on an iterator over an array.
2011-09-05 Robert Dewar <dewar@adacore.com>
* lib-xref-alfa.adb: Minor reformatting.
From-SVN: r178538
-rw-r--r-- | gcc/ada/ChangeLog | 15 | ||||
-rw-r--r-- | gcc/ada/lib-xref-alfa.adb | 38 | ||||
-rw-r--r-- | gcc/ada/sem_ch3.adb | 23 | ||||
-rw-r--r-- | gcc/ada/sem_ch5.adb | 7 |
4 files changed, 51 insertions, 32 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 22d261d..e267e9b 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,18 @@ +2011-09-05 Marc Sango <sango@adacore.com> + + * 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 <schonberg@adacore.com> + + * sem_ch5.adb (Analyze_Iteration_Specification): Improve error + message on an iterator over an array. + +2011-09-05 Robert Dewar <dewar@adacore.com> + + * lib-xref-alfa.adb: Minor reformatting. + 2011-09-05 Robert Dewar <dewar@adacore.com> * 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 8eef505..cc0aa3a 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 46abaa9..2953141 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 5a2d2b3..81153fa 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; |