From cbee4f7497366895219ee4caa04b9d2f4c45ce83 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 6 Feb 2014 10:58:37 +0100 Subject: [PATCH] [multiple changes] 2014-02-06 Ed Schonberg * exp_ch6.adb (Expand_Subprogram_Contract, Append_Enabled_Item): Take into account the Split_PPC flag to ensure that conjuncts in a composite postcondition aspect are tested in source order. 2014-02-06 Hristian Kirtchev * sem_ch6.adb (Analyze_Generic_Subprogram_Body): Flag illegal use of SPARK_Mode. * sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): Flag illegal use of SPARK_Mode. (Instantiate_Subprogram_Body): Flag illegal use of SPARK_Mode. * sem_prag.adb (Analyze_Pragma): Code reformatting. * sem_util.adb Add with and use clause for Aspects. (Check_SPARK_Mode_In_Generic): New routine. * sem_util.ads (Check_SPARK_Mode_In_Generic): New routine. 2014-02-06 Thomas Quinot * a-calend.adb (Formatting_Operations.Split): Ensure that Time_Error is raised for invalid time values. From-SVN: r207536 --- gcc/ada/ChangeLog | 23 +++++++++++++++++++++++ gcc/ada/a-calend.adb | 6 +++++- gcc/ada/exp_ch6.adb | 13 ++++++++++++- gcc/ada/sem_ch12.adb | 2 ++ gcc/ada/sem_ch6.adb | 2 ++ gcc/ada/sem_prag.adb | 15 ++++++++------- gcc/ada/sem_util.adb | 26 ++++++++++++++++++++++++++ gcc/ada/sem_util.ads | 5 +++++ 8 files changed, 83 insertions(+), 9 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index c2d9eaef90ef..3a866ca8035d 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,26 @@ +2014-02-06 Ed Schonberg + + * exp_ch6.adb (Expand_Subprogram_Contract, Append_Enabled_Item): + Take into account the Split_PPC flag to ensure that conjuncts + in a composite postcondition aspect are tested in source order. + +2014-02-06 Hristian Kirtchev + + * sem_ch6.adb (Analyze_Generic_Subprogram_Body): Flag illegal + use of SPARK_Mode. + * sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): Flag + illegal use of SPARK_Mode. + (Instantiate_Subprogram_Body): Flag illegal use of SPARK_Mode. + * sem_prag.adb (Analyze_Pragma): Code reformatting. + * sem_util.adb Add with and use clause for Aspects. + (Check_SPARK_Mode_In_Generic): New routine. + * sem_util.ads (Check_SPARK_Mode_In_Generic): New routine. + +2014-02-06 Thomas Quinot + + * a-calend.adb (Formatting_Operations.Split): Ensure that + Time_Error is raised for invalid time values. + 2014-02-06 Arnaud Charlet * sem_prag.adb (Analyze_Pragma): Rewrite as a null statement diff --git a/gcc/ada/a-calend.adb b/gcc/ada/a-calend.adb index dbc95771e710..0043a91e9fe1 100644 --- a/gcc/ada/a-calend.adb +++ b/gcc/ada/a-calend.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2012, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -1384,6 +1384,10 @@ package body Ada.Calendar is Hour_Seconds := Day_Seconds mod 3_600; Minute := Hour_Seconds / 60; Second := Hour_Seconds mod 60; + + exception + when Constraint_Error => + raise Time_Error; end Split; ------------- diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 4aad9d46518e..52cc9c8d1ee2 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -8887,7 +8887,18 @@ package body Exp_Ch6 is List := New_List; end if; - Append (Item, List); + -- If the pragma is a conjunct in a composite postcondition, it + -- has been processed in reverse order. In the postcondition body + -- if must appear before the others. + + if Nkind (Item) = N_Pragma + and then From_Aspect_Specification (Item) + and then Split_PPC (Item) + then + Prepend (Item, List); + else + Append (Item, List); + end if; end if; end Append_Enabled_Item; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 78881a903347..e8784e5b784e 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3118,6 +3118,8 @@ package body Sem_Ch12 is Set_Parent_Spec (New_N, Save_Parent); Rewrite (N, New_N); + Check_SPARK_Mode_In_Generic (N); + -- The aspect specifications are not attached to the tree, and must -- be copied and attached to the generic copy explicitly. diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 5b91519630f9..07117d6dd340 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1193,6 +1193,8 @@ package body Sem_Ch6 is end loop; end; + Check_SPARK_Mode_In_Generic (N); + Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Body_Id, True); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index c5c749a8a654..98e674f5433c 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -19217,10 +19217,6 @@ package body Sem_Prag is Check_No_Identifiers; Check_At_Most_N_Arguments (1); - if Inside_A_Generic then - Error_Pragma ("incorrect placement of pragma% in a generic"); - end if; - -- Check the legality of the mode (no argument = ON) if Arg_Count = 1 then @@ -19233,9 +19229,15 @@ package body Sem_Prag is Mode_Id := Get_SPARK_Mode_Type (Mode); Context := Parent (N); + -- Packages and subprograms declared in a generic unit cannot be + -- subject to the pragma. + + if Inside_A_Generic then + Error_Pragma ("incorrect placement of pragma% in a generic"); + -- The pragma appears in a configuration pragmas file - if No (Context) then + elsif No (Context) then Check_Valid_Configuration_Pragma; if Present (SPARK_Mode_Pragma) then @@ -19258,8 +19260,7 @@ package body Sem_Prag is and then Nkind (Unit (Library_Unit (Context))) in N_Generic_Declaration) then - Error_Pragma - ("incorrect placement of pragma% in a generic unit"); + Error_Pragma ("incorrect placement of pragma% in a generic"); end if; SPARK_Mode_Pragma := N; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index ba978e1aa764..a2501cadbffc 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -23,6 +23,7 @@ -- -- ------------------------------------------------------------------------------ +with Aspects; use Aspects; with Atree; use Atree; with Casing; use Casing; with Checks; use Checks; @@ -2699,6 +2700,31 @@ package body Sem_Util is end if; end Check_Result_And_Post_State; + --------------------------------- + -- Check_SPARK_Mode_In_Generic -- + --------------------------------- + + procedure Check_SPARK_Mode_In_Generic (N : Node_Id) is + Aspect : Node_Id; + + begin + -- Try to find aspect SPARK_Mode and flag it as illegal + + if Has_Aspects (N) then + Aspect := First (Aspect_Specifications (N)); + while Present (Aspect) loop + if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then + Error_Msg_Name_1 := Name_SPARK_Mode; + Error_Msg_N + ("incorrect placement of aspect % on a generic", Aspect); + exit; + end if; + + Next (Aspect); + end loop; + end if; + end Check_SPARK_Mode_In_Generic; + ------------------------------ -- Check_Unprotected_Access -- ------------------------------ diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 0e26161fe211..15232b953288 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -62,6 +62,7 @@ package Sem_Util is -- Precondition -- Refined_Depends -- Refined_Global + -- Refined_Post -- Refined_States -- Test_Case @@ -289,6 +290,10 @@ package Sem_Util is -- and post-state. Prag is a [refined] postcondition or a contract-cases -- pragma. Result_Seen is set when the pragma mentions attribute 'Result. + procedure Check_SPARK_Mode_In_Generic (N : Node_Id); + -- Given a generic package [body] or a generic subprogram [body], inspect + -- the aspect specifications (if any) and flag SPARK_Mode as illegal. + procedure Check_Unprotected_Access (Context : Node_Id; Expr : Node_Id); -- 2.47.3