[multiple changes]

2014-02-06  Ed Schonberg  <schonberg@adacore.com>

	* 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  <kirtchev@adacore.com>

	* 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  <quinot@adacore.com>

	* a-calend.adb (Formatting_Operations.Split): Ensure that
	Time_Error is raised for invalid time values.

From-SVN: r207536

8 files changed, 83 insertions, 9 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index c2d9eae..3a866ca 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,26 @@
+2014-02-06  Ed Schonberg  <schonberg@adacore.com>
+
+	* 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  <kirtchev@adacore.com>
+
+	* 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  <quinot@adacore.com>
+
+	* a-calend.adb (Formatting_Operations.Split): Ensure that
+	Time_Error is raised for invalid time values.
+
 2014-02-06  Arnaud Charlet  <charlet@adacore.com>
 
 	* 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 dbc9577..0043a91 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 4aad9d4..52cc9c8 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 78881a9..e8784e5 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 5b91519..07117d6 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 c5c749a..98e674f 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 ba978e1..a2501ca 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 0e26161..15232b9 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);