[multiple changes]

2014-08-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* a-cfhama.ads, a-cfhase.ads, a-cforma.ads, a-cforse.ads Add
	SPARK_Mode pragmas to the public and private part of the unit.
	* sem_ch3.adb (Derive_Type_Declaration): Ensure that a derived
	type cannot have discriminants if the parent type already has
	discriminants.
	(Process_Discriminants): Ensure that the type of a discriminant is
	discrete.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): The check on
	SPARK_Mode compatibility between a spec and a body can now be
	safely performed while processing a generic.
	* sem_ch7.adb (Analyze_Package_Body_Helper): The check on
	SPARK_Mode compatibility between a spec and a body can now be
	safely performed while processing a generic.
	* sem_prag.adb (Analyze_Pragma): Pragma SPARK_Mode can now be
	safely analyzed when processing a generic.

2014-08-04  Nicolas Roche  <roche@adacore.com>

	* g-dirope.adb: Minor reformating.

From-SVN: r213575

10 files changed, 91 insertions, 40 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 4737fc7..b6665e6 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,25 @@
+2014-08-04  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* a-cfhama.ads, a-cfhase.ads, a-cforma.ads, a-cforse.ads Add
+	SPARK_Mode pragmas to the public and private part of the unit.
+	* sem_ch3.adb (Derive_Type_Declaration): Ensure that a derived
+	type cannot have discriminants if the parent type already has
+	discriminants.
+	(Process_Discriminants): Ensure that the type of a discriminant is
+	discrete.
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): The check on
+	SPARK_Mode compatibility between a spec and a body can now be
+	safely performed while processing a generic.
+	* sem_ch7.adb (Analyze_Package_Body_Helper): The check on
+	SPARK_Mode compatibility between a spec and a body can now be
+	safely performed while processing a generic.
+	* sem_prag.adb (Analyze_Pragma): Pragma SPARK_Mode can now be
+	safely analyzed when processing a generic.
+
+2014-08-04  Nicolas Roche  <roche@adacore.com>
+
+	* g-dirope.adb: Minor reformating.
+
 2014-08-04  Robert Dewar  <dewar@adacore.com>
 
 	* sem_ch6.adb: Minor reformatting.
diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads
index 9a2b376..b5c440e 100644
--- a/gcc/ada/a-cfhama.ads
+++ b/gcc/ada/a-cfhama.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -68,6 +68,7 @@ generic
 package Ada.Containers.Formal_Hashed_Maps is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
+   pragma SPARK_Mode (On);
 
    type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with
      Iterable => (First       => First,
@@ -276,6 +277,7 @@ private
    pragma Inline (Has_Element);
    pragma Inline (Equivalent_Keys);
    pragma Inline (Next);
+   pragma SPARK_Mode (Off);
 
    type Node_Type is record
       Key         : Key_Type;
@@ -285,11 +287,10 @@ private
    end record;
 
    package HT_Types is new
-     Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types
-       (Node_Type);
+     Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
 
    type Map (Capacity : Count_Type; Modulus : Hash_Type) is
-      new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
+     new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
 
    use HT_Types;
 
diff --git a/gcc/ada/a-cfhase.ads b/gcc/ada/a-cfhase.ads
index 4e54ef9..2a2f4e8 100644
--- a/gcc/ada/a-cfhase.ads
+++ b/gcc/ada/a-cfhase.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -70,6 +70,7 @@ generic
 package Ada.Containers.Formal_Hashed_Sets is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
+   pragma SPARK_Mode (On);
 
    type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with
      Iterable => (First       => First,
@@ -329,8 +330,8 @@ package Ada.Containers.Formal_Hashed_Sets is
    --  scanned yet.
 
 private
-
    pragma Inline (Next);
+   pragma SPARK_Mode (Off);
 
    type Node_Type is
       record
@@ -343,7 +344,7 @@ private
      Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
 
    type Set (Capacity : Count_Type; Modulus : Hash_Type) is
-      new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
+     new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
 
    use HT_Types;
 
diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads
index 64d77fa..e9a5f97 100644
--- a/gcc/ada/a-cforma.ads
+++ b/gcc/ada/a-cforma.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -69,6 +69,7 @@ generic
 package Ada.Containers.Formal_Ordered_Maps is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
+   pragma SPARK_Mode (On);
 
    function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
      Global => null;
@@ -265,10 +266,11 @@ package Ada.Containers.Formal_Ordered_Maps is
    function Overlap (Left, Right : Map) return Boolean with
      Global => null;
    --  Overlap returns True if the containers have common keys
-private
 
+private
    pragma Inline (Next);
    pragma Inline (Previous);
+   pragma SPARK_Mode (Off);
 
    subtype Node_Access is Count_Type;
 
@@ -288,7 +290,7 @@ private
      new Ada.Containers.Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
 
    type Map (Capacity : Count_Type) is
-      new Tree_Types.Tree_Type (Capacity) with null record;
+     new Tree_Types.Tree_Type (Capacity) with null record;
 
    type Cursor is record
       Node : Node_Access;
diff --git a/gcc/ada/a-cforse.ads b/gcc/ada/a-cforse.ads
index 8d3189e..dc17407 100644
--- a/gcc/ada/a-cforse.ads
+++ b/gcc/ada/a-cforse.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -67,6 +67,7 @@ generic
 package Ada.Containers.Formal_Ordered_Sets is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
+   pragma SPARK_Mode (On);
 
    function Equivalent_Elements (Left, Right : Element_Type) return Boolean
    with
@@ -347,9 +348,9 @@ package Ada.Containers.Formal_Ordered_Sets is
    --  scanned yet.
 
 private
-
    pragma Inline (Next);
    pragma Inline (Previous);
+   pragma SPARK_Mode (Off);
 
    type Node_Type is record
       Has_Element : Boolean := False;
diff --git a/gcc/ada/g-dirope.adb b/gcc/ada/g-dirope.adb
index bf579f5..3b745b1 100644
--- a/gcc/ada/g-dirope.adb
+++ b/gcc/ada/g-dirope.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                     Copyright (C) 1998-2012, AdaCore                     --
+--                     Copyright (C) 1998-2014, AdaCore                     --
 --                                                                          --
 -- 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- --
@@ -693,7 +693,7 @@ package body GNAT.Directory_Operations is
    end Read;
 
    -------------------------
-   -- Read_Is_Thread_Sage --
+   -- Read_Is_Thread_Safe --
    -------------------------
 
    function Read_Is_Thread_Safe return Boolean is
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 73a63e7..aa410e4 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -15046,7 +15046,7 @@ package body Sem_Ch3 is
       end if;
 
       --  Only composite types other than array types are allowed to have
-      --  discriminants. In SPARK, no types are allowed to have discriminants.
+      --  discriminants.
 
       if Present (Discriminant_Specifications (N)) then
          if (Is_Elementary_Type (Parent_Type)
@@ -15057,8 +15057,22 @@ package body Sem_Ch3 is
               ("elementary or array type cannot have discriminants",
                Defining_Identifier (First (Discriminant_Specifications (N))));
             Set_Has_Discriminants (T, False);
+
+         --  The type is allowed to have discriminants
+
          else
             Check_SPARK_05_Restriction ("discriminant type is not allowed", N);
+
+            --  The following check is only relevant when SPARK_Mode is on as
+            --  it is not a standard Ada legality rule. A derived type cannot
+            --  have discriminants if the parent type is discriminated.
+
+            if SPARK_Mode = On and then Has_Discriminants (Parent_Type) then
+               SPARK_Msg_N
+                 ("discriminants not allowed if parent type is discriminated",
+                  Defining_Identifier
+                    (First (Discriminant_Specifications (N))));
+            end if;
          end if;
       end if;
 
@@ -18024,24 +18038,44 @@ package body Sem_Ch3 is
             end if;
          end if;
 
-         if Is_Access_Type (Discr_Type) then
+         --  The following checks are only relevant when SPARK_Mode is on as
+         --  they are not standard Ada legality rules.
+
+         if SPARK_Mode = On then
+            if Is_Access_Type (Discr_Type) then
+               SPARK_Msg_N
+                 ("discriminant cannot have an access type",
+                  Discriminant_Type (Discr));
+
+            elsif not Is_Discrete_Type (Discr_Type) then
+               SPARK_Msg_N
+                 ("discriminant must have a discrete type",
+                  Discriminant_Type (Discr));
+            end if;
 
-            --  Ada 2005 (AI-230): Access discriminant allowed in non-limited
-            --  record types
+         --  Normal Ada rules
 
-            if Ada_Version < Ada_2005 then
-               Check_Access_Discriminant_Requires_Limited
-                 (Discr, Discriminant_Type (Discr));
-            end if;
+         else
+            if Is_Access_Type (Discr_Type) then
+
+               --  Ada 2005 (AI-230): Access discriminant allowed in non-
+               --  limited record types
+
+               if Ada_Version < Ada_2005 then
+                  Check_Access_Discriminant_Requires_Limited
+                    (Discr, Discriminant_Type (Discr));
+               end if;
 
-            if Ada_Version = Ada_83 and then Comes_From_Source (Discr) then
+               if Ada_Version = Ada_83 and then Comes_From_Source (Discr) then
+                  Error_Msg_N
+                    ("(Ada 83) access discriminant not allowed", Discr);
+               end if;
+
+            elsif not Is_Discrete_Type (Discr_Type) then
                Error_Msg_N
-                 ("(Ada 83) access discriminant not allowed", Discr);
+                 ("discriminants must have a discrete or access type",
+                  Discriminant_Type (Discr));
             end if;
-
-         elsif not Is_Discrete_Type (Discr_Type) then
-            Error_Msg_N ("discriminants must have a discrete or access type",
-              Discriminant_Type (Discr));
          end if;
 
          Set_Etype (Defining_Identifier (Discr), Discr_Type);
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index f7b7375..01c6e26 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3741,10 +3741,7 @@ package body Sem_Ch6 is
 
       --  Verify that the SPARK_Mode of the body agrees with that of its spec
 
-      if not Inside_A_Generic
-        and then Present (Spec_Id)
-        and then Present (SPARK_Pragma (Body_Id))
-      then
+      if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then
          if Present (SPARK_Pragma (Spec_Id)) then
             if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
                  and then
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 583621f..4821db5 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -439,7 +439,7 @@ package body Sem_Ch7 is
 
       --  Verify that the SPARK_Mode of the body agrees with that of its spec
 
-      if not Inside_A_Generic and then Present (SPARK_Pragma (Body_Id)) then
+      if Present (SPARK_Pragma (Body_Id)) then
          if Present (SPARK_Aux_Pragma (Spec_Id)) then
             if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
                  and then
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index ad51ce3..da9c066 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -19243,13 +19243,6 @@ package body Sem_Prag is
                Rewrite (N, Make_Null_Statement (Loc));
                Analyze (N);
                return;
-
-            --  Do not analyze the pragma when it appears inside a generic
-            --  because the semantic information of the related context is
-            --  scarce.
-
-            elsif Inside_A_Generic then
-               return;
             end if;
 
             GNAT_Pragma;