[multiple changes]

2014-10-30  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_util.adb (Inherit_Subprogram_Contract):
	Add a guard to protect against enumeration literal overriding.
	* sem_ch3.adb, sem_ch4.adb, sem_res.adb, sem_util.adb:
	Minor reformatting (add SPARK RM references).

2014-10-30  Robert Dewar  <dewar@adacore.com>

	* exp_dbug.adb, opt.ads: Minor reformatting.

From-SVN: r216920

7 files changed, 45 insertions, 16 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 65e0b602754..36e8faf4d6e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,14 @@
+2014-10-30  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_util.adb (Inherit_Subprogram_Contract):
+	Add a guard to protect against enumeration literal overriding.
+	* sem_ch3.adb, sem_ch4.adb, sem_res.adb, sem_util.adb:
+	Minor reformatting (add SPARK RM references).
+
+2014-10-30  Robert Dewar  <dewar@adacore.com>
+
+	* exp_dbug.adb, opt.ads: Minor reformatting.
+
 2014-10-30  Yannick Moy  <moy@adacore.com>
 
 	* inline.adb (Has_Single_Return_In_GNATprove_Mode):
diff --git a/gcc/ada/exp_dbug.adb b/gcc/ada/exp_dbug.adb
index c025f05f378..0d30f421e5b 100644
--- a/gcc/ada/exp_dbug.adb
+++ b/gcc/ada/exp_dbug.adb
@@ -604,10 +604,15 @@ package body Exp_Dbug is
             Add_Real_To_Buffer (Small_Value (E));
          end if;
 
-      --  Discrete case where bounds do not match size
-
-      elsif Is_Discrete_Type (E)
-        and then not Bounds_Match_Size (E)
+      --  Discrete case where bounds do not match size. Match only biased
+      --  types when asked to output as little encodings as possible.
+
+      elsif ((GNAT_Encodings /= DWARF_GNAT_Encodings_Minimal
+               and then Is_Discrete_Type (E))
+             or else
+             (GNAT_Encodings = DWARF_GNAT_Encodings_Minimal
+               and then Has_Biased_Representation (E)))
+            and then not Bounds_Match_Size (E)
       then
          declare
             Lo : constant Node_Id := Type_Low_Bound (E);
@@ -618,13 +623,11 @@ package body Exp_Dbug is
 
             Lo_Discr : constant Boolean :=
                          Nkind (Lo) = N_Identifier
-                           and then
-                         Ekind (Entity (Lo)) = E_Discriminant;
+                          and then Ekind (Entity (Lo)) = E_Discriminant;
 
             Hi_Discr : constant Boolean :=
                          Nkind (Hi) = N_Identifier
-                           and then
-                         Ekind (Entity (Hi)) = E_Discriminant;
+                          and then Ekind (Entity (Hi)) = E_Discriminant;
 
             Lo_Encode : constant Boolean := Lo_Con or Lo_Discr;
             Hi_Encode : constant Boolean := Hi_Con or Hi_Discr;
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 7706827f8f5..a17d9fe5936 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -730,6 +730,17 @@ package Opt is
    --  True if a pragma Discard_Names appeared as a configuration pragma for
    --  the current compilation unit.
 
+   GNAT_Encodings : Int;
+   pragma Import (C, GNAT_Encodings, "gnat_encodings");
+   --  Constant controlling the balance between GNAT encodings and standard
+   --  DWARF to emit in the debug information. See jmissing.c and aamissing.c
+   --  for definitions for dotnet/jgnat and GNAAMP back ends. It accepts the
+   --  following values.
+
+   DWARF_GNAT_Encodings_All     : constant Int := 0;
+   DWARF_GNAT_Encodings_GDB     : constant Int := 1;
+   DWARF_GNAT_Encodings_Minimal : constant Int := 2;
+
    Identifier_Character_Set : Character;
    --  GNAT
    --  This variable indicates the character set to be used for identifiers.
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 78b4697b6b3..bff1ac4713f 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3704,7 +3704,7 @@ package body Sem_Ch3 is
          --  A formal parameter of a specific tagged type whose related
          --  subprogram is subject to pragma Extensions_Visible with value
          --  "False" cannot be implicitly converted to a class-wide type by
-         --  means of an initialization expression.
+         --  means of an initialization expression (SPARK RM 6.1.7(3)).
 
          if Is_Class_Wide_Type (T) and then Is_EVF_Expression (E) then
             Error_Msg_N
@@ -9809,7 +9809,8 @@ package body Sem_Ch3 is
 
                   --  A null extension is not obliged to override an inherited
                   --  procedure subject to pragma Extensions_Visible with value
-                  --  False and at least one controlling OUT parameter.
+                  --  False and at least one controlling OUT parameter
+                  --  (SPARK RM 6.1.7(6)).
 
                   elsif Is_Null_Extension (T)
                     and then Is_EVF_Procedure (Subp)
@@ -9941,7 +9942,7 @@ package body Sem_Ch3 is
 
          --  A subprogram subject to pragma Extensions_Visible with value
          --  "True" cannot override a subprogram subject to the same pragma
-         --  with value "False".
+         --  with value "False" (SPARK RM 6.1.7(5)).
 
          elsif Extensions_Visible_Status (Subp) = Extensions_Visible_True
            and then Present (Overridden_Operation (Subp))
@@ -14541,7 +14542,7 @@ package body Sem_Ch3 is
 
       --  A subprogram subject to pragma Extensions_Visible with value False
       --  requires overriding if the subprogram has at least one controlling
-      --  OUT parameter.
+      --  OUT parameter (SPARK RM 6.1.7(6)).
 
       elsif Ada_Version >= Ada_2005
         and then (Is_Abstract_Subprogram (Alias (New_Subp))
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 8b2a8050e2f..ee56e746042 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -5019,7 +5019,7 @@ package body Sem_Ch4 is
 
       --  A formal parameter of a specific tagged type whose related subprogram
       --  is subject to pragma Extensions_Visible with value "False" cannot
-      --  appear in a class-wide conversion.
+      --  appear in a class-wide conversion (SPARK RM 6.1.7(3)).
 
       if Is_Class_Wide_Type (Typ) and then Is_EVF_Expression (Expr) then
          Error_Msg_N
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index e26ff704908..c8869d720e4 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -4421,7 +4421,7 @@ package body Sem_Res is
             --  A formal parameter of a specific tagged type whose related
             --  subprogram is subject to pragma Extensions_Visible with value
             --  "False" cannot act as an actual in a subprogram with value
-            --  "True".
+            --  "True" (SPARK RM 6.1.7(3)).
 
             if Is_EVF_Expression (A)
               and then Extensions_Visible_Status (Nam) =
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index db8cdd717bd..0715894b2d5 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -9481,9 +9481,12 @@ package body Sem_Util is
    --   Start of processing for Inherit_Subprogram_Contract
 
    begin
-      --  Inheritance is carried out only when both subprograms have contracts
+      --  Inheritance is carried out only when both entities are subprograms
+      --  with contracts.
 
-      if Present (Contract (Subp))
+      if Is_Subprogram_Or_Generic_Subprogram (Subp)
+        and then Is_Subprogram_Or_Generic_Subprogram (From_Subp)
+        and then Present (Contract (Subp))
         and then Present (Contract (From_Subp))
       then
          Inherit_Pragma (Pragma_Extensions_Visible);