From 7f2c8954dac84a3fa5cabcc726b5e7d1ddff1142 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 13 Jun 2014 11:40:19 +0200 Subject: [PATCH] [multiple changes] 2014-06-13 Yannick Moy * sem_warn.adb (Check_Unset_References): Take case of Refined_Post into account in Within_Postcondition check. 2014-06-13 Hristian Kirtchev * freeze.adb (Freeze_Record_Type): Volatile types are not allowed in SPARK. 2014-06-13 Yannick Moy * sem_ch13.adb (Analyze_Aspect_Specifications/Aspect_Import, Aspect_Export): Consider that variables may be set outside the program. From-SVN: r211611 --- gcc/ada/ChangeLog | 15 +++++++++++++++ gcc/ada/freeze.adb | 13 +++---------- gcc/ada/sem_ch13.adb | 15 ++++++++++++++- gcc/ada/sem_warn.adb | 6 ++++-- 4 files changed, 36 insertions(+), 13 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b2cdbc578b8b..3a0b1e6567ed 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,18 @@ +2014-06-13 Yannick Moy + + * sem_warn.adb (Check_Unset_References): Take + case of Refined_Post into account in Within_Postcondition check. + +2014-06-13 Hristian Kirtchev + + * freeze.adb (Freeze_Record_Type): Volatile types are not allowed in + SPARK. + +2014-06-13 Yannick Moy + + * sem_ch13.adb (Analyze_Aspect_Specifications/Aspect_Import, + Aspect_Export): Consider that variables may be set outside the program. + 2014-06-13 Robert Dewar * back_end.adb (Make_Id): New function. diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 97d21d38d3de..bfd15f3bd18c 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -3359,18 +3359,11 @@ package body Freeze is -- they are not standard Ada legality rules. if SPARK_Mode = On then - if Is_SPARK_Volatile (Rec) then - - -- A discriminated type cannot be volatile (SPARK RM C.6(4)) - - if Has_Discriminants (Rec) then - Error_Msg_N ("discriminated type & cannot be volatile", Rec); - -- A tagged type cannot be volatile (SPARK RM C.6(5)) + -- Volatile types are not allowed in SPARK (SPARK RM C.6(1)) - elsif Is_Tagged_Type (Rec) then - Error_Msg_N ("tagged type & cannot be volatile", Rec); - end if; + if Is_SPARK_Volatile (Rec) then + Error_Msg_N ("volatile type not allowed", Rec); -- A non-volatile record type cannot contain volatile components -- (SPARK RM C.6(2)). The check is performed at freeze point diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 3e1398ba1636..31256d22f8f6 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1603,7 +1603,7 @@ package body Sem_Ch13 is goto Continue; end if; - -- For case of address aspect, we don't consider that we + -- For the case of aspect Address, we don't consider that we -- know the entity is never set in the source, since it is -- is likely aliasing is occurring. @@ -2691,6 +2691,19 @@ package body Sem_Ch13 is elsif A_Id = Aspect_Import or else A_Id = Aspect_Export then + -- For the case of aspects Import and Export, we don't + -- consider that we know the entity is never set in the + -- source, since it is is likely modified outside the + -- program. + + -- Note: one might think that the analysis of the + -- resulting pragma would take care of that, but + -- that's not the case since it won't be from source. + + if Ekind (E) = E_Variable then + Set_Never_Set_In_Source (E, False); + end if; + -- Verify that there is an aspect Convention that will -- incorporate the Import/Export aspect, and eventual -- Link/External names. diff --git a/gcc/ada/sem_warn.adb b/gcc/ada/sem_warn.adb index 0043ef61b7fe..4c2f78c2bc29 100644 --- a/gcc/ada/sem_warn.adb +++ b/gcc/ada/sem_warn.adb @@ -1810,8 +1810,9 @@ package body Sem_Warn is SE : constant Entity_Id := Scope (E); function Within_Postcondition return Boolean; - -- Returns True iff N is within a Postcondition, an - -- Ensures component in a Test_Case, or a Contract_Cases. + -- Returns True iff N is within a Postcondition, a + -- Refined_Post, an Ensures component in a Test_Case, + -- or a Contract_Cases. -------------------------- -- Within_Postcondition -- @@ -1826,6 +1827,7 @@ package body Sem_Warn is if Nkind (Nod) = N_Pragma and then Nam_In (Pragma_Name (Nod), Name_Postcondition, + Name_Refined_Post, Name_Contract_Cases) then return True; -- 2.47.3