[Ada] Warning on nonmatching subtypes in fully conforming subprogram specs and bodies

diff --git a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
--- a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
+++ b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
@@ -3582,6 +3582,25 @@  of the pragma in the :title:`GNAT_Reference_manual`).
   ordering.
 
 
+.. index:: -gnatw_p  (gcc)
+
+:switch:`-gnatw_p`
+  *Activate warnings for pedantic checks.*
+
+  This switch activates warnings for the failure of certain pedantic checks.
+  The only case currently supported is a check that the subtype_marks given
+  for corresponding formal parameter and function results in a subprogram
+  declaration and its body denote the same subtype declaration. The default
+  is that such warnings are not given.
+
+.. index:: -gnatw_P  (gcc)
+
+:switch:`-gnatw_P`
+  *Suppress warnings for pedantic checks.*
+
+  This switch suppresses warnings on violations of pedantic checks.
+
+
 .. index:: -gnatwq  (gcc)
 .. index:: Parentheses, warnings
 


diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -21,7 +21,7 @@ 
 
 @copying
 @quotation
-GNAT User's Guide for Native Platforms , Sep 28, 2021
+GNAT User's Guide for Native Platforms , Oct 19, 2021
 
 AdaCore
 
@@ -11800,6 +11800,34 @@  This switch suppresses warnings on cases of suspicious parameter
 ordering.
 @end table
 
+@geindex -gnatw_p (gcc)
+
+
+@table @asis
+
+@item @code{-gnatw_p}
+
+@emph{Activate warnings for pedantic checks.}
+
+This switch activates warnings for the failure of certain pedantic checks.
+The only case currently supported is a check that the subtype_marks given
+for corresponding formal parameter and function results in a subprogram
+declaration and its body denote the same subtype declaration. The default
+is that such warnings are not given.
+@end table
+
+@geindex -gnatw_P (gcc)
+
+
+@table @asis
+
+@item @code{-gnatw_P}
+
+@emph{Suppress warnings for pedantic checks.}
+
+This switch suppresses warnings on violations of pedantic checks.
+@end table
+
 @geindex -gnatwq (gcc)
 
 @geindex Parentheses


diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -90,6 +90,7 @@  with Tbuild;         use Tbuild;
 with Uintp;          use Uintp;
 with Urealp;         use Urealp;
 with Validsw;        use Validsw;
+with Warnsw;         use Warnsw;
 
 package body Sem_Ch6 is
 
@@ -5962,6 +5963,17 @@  package body Sem_Ch6 is
       --  True if the null exclusions of two formals of anonymous access type
       --  match.
 
+      function Subprogram_Subtypes_Have_Same_Declaration
+        (Subp         : Entity_Id;
+         Decl_Subtype : Entity_Id;
+         Body_Subtype : Entity_Id) return Boolean;
+      --  Checks whether corresponding subtypes named within a subprogram
+      --  declaration and body originate from the same declaration, and returns
+      --  True when they do. In the case of anonymous access-to-object types,
+      --  checks the designated types. Also returns True when GNAT_Mode is
+      --  enabled, or when the subprogram is marked Is_Internal or occurs
+      --  within a generic instantiation or internal unit (GNAT library unit).
+
       -----------------------
       -- Conformance_Error --
       -----------------------
@@ -6094,6 +6106,86 @@  package body Sem_Ch6 is
          end if;
       end Null_Exclusions_Match;
 
+      function Subprogram_Subtypes_Have_Same_Declaration
+        (Subp         : Entity_Id;
+         Decl_Subtype : Entity_Id;
+         Body_Subtype : Entity_Id) return Boolean
+      is
+
+         function Nonlimited_View_Of_Subtype
+           (Subt : Entity_Id) return Entity_Id;
+         --  Returns the nonlimited view of a type or subtype that is an
+         --  incomplete or class-wide type that comes from a limited view of
+         --  a package (From_Limited_With is True for the entity), or the
+         --  full view when the subtype is an incomplete type. Otherwise
+         --  returns the entity passed in.
+
+         function Nonlimited_View_Of_Subtype
+           (Subt : Entity_Id) return Entity_Id
+         is
+            Subt_Temp : Entity_Id := Subt;
+         begin
+            if Ekind (Subt) in Incomplete_Kind | E_Class_Wide_Type
+              and then From_Limited_With (Subt)
+            then
+               Subt_Temp := Non_Limited_View (Subt);
+            end if;
+
+            --  If the subtype is incomplete, return full view if present
+            --  (and accounts for the case where a type from a limited view
+            --  is itself an incomplete type).
+
+            if Ekind (Subt_Temp) in Incomplete_Kind
+              and then Present (Full_View (Subt_Temp))
+            then
+               Subt_Temp := Full_View (Subt_Temp);
+            end if;
+
+            return Subt_Temp;
+         end Nonlimited_View_Of_Subtype;
+
+      --  Start of processing for Subprogram_Subtypes_Have_Same_Declaration
+
+      begin
+         if not In_Instance
+           and then not In_Internal_Unit (Subp)
+           and then not Is_Internal (Subp)
+           and then not GNAT_Mode
+           and then
+             Ekind (Etype (Decl_Subtype)) not in Access_Subprogram_Kind
+         then
+            if Ekind (Etype (Decl_Subtype)) = E_Anonymous_Access_Type then
+               if Nonlimited_View_Of_Subtype (Designated_Type (Decl_Subtype))
+                 /= Nonlimited_View_Of_Subtype (Designated_Type (Body_Subtype))
+               then
+                  return False;
+               end if;
+
+            elsif Nonlimited_View_Of_Subtype (Decl_Subtype)
+               /= Nonlimited_View_Of_Subtype (Body_Subtype)
+            then
+               --  Avoid returning False (and a false-positive warning) for
+               --  the case of "not null" itypes, which will appear to be
+               --  different subtypes even when the subtype_marks denote
+               --  the same subtype.
+
+               if Ekind (Decl_Subtype) = E_Access_Subtype
+                 and then Ekind (Body_Subtype) = E_Access_Subtype
+                 and then Is_Itype (Body_Subtype)
+                 and then Can_Never_Be_Null (Body_Subtype)
+                 and then Etype (Decl_Subtype) = Etype (Body_Subtype)
+               then
+                  return True;
+
+               else
+                  return False;
+               end if;
+            end if;
+         end if;
+
+         return True;
+      end Subprogram_Subtypes_Have_Same_Declaration;
+
       --  Local Variables
 
       Old_Type           : constant Entity_Id := Etype (Old_Id);
@@ -6147,6 +6239,18 @@  package body Sem_Ch6 is
             end if;
 
             return;
+
+         --  If the result subtypes conform and pedantic checks are enabled,
+         --  check to see whether the subtypes originate from different
+         --  declarations, and issue a warning when they do.
+
+         elsif Ctype = Fully_Conformant
+           and then Warn_On_Pedantic_Checks
+           and then not Subprogram_Subtypes_Have_Same_Declaration
+                          (Old_Id, Old_Type, New_Type)
+         then
+            Error_Msg_N ("result subtypes conform but come from different "
+                          & "declarations??", New_Id);
          end if;
 
          --  Ada 2005 (AI-231): In case of anonymous access types check the
@@ -6343,6 +6447,18 @@  package body Sem_Ch6 is
             end if;
 
             return;
+
+         --  If the formals' subtypes conform and pedantic checks are enabled,
+         --  check to see whether the subtypes originate from different
+         --  declarations, and issue a warning when they do.
+
+         elsif Ctype = Fully_Conformant
+           and then Warn_On_Pedantic_Checks
+           and then not Subprogram_Subtypes_Have_Same_Declaration
+                          (Old_Id, Old_Formal_Base, New_Formal_Base)
+         then
+            Error_Msg_N ("formal subtypes conform but come from "
+                          & "different declarations??", New_Formal);
          end if;
 
          --  For mode conformance, mode must match


diff --git a/gcc/ada/usage.adb b/gcc/ada/usage.adb
--- a/gcc/ada/usage.adb
+++ b/gcc/ada/usage.adb
@@ -557,6 +557,8 @@  begin
                                                   "order");
    Write_Line ("        .P*  turn off warnings for suspicious parameter " &
                                                   "order");
+   Write_Line ("        _p   turn on warnings for pedantic checks");
+   Write_Line ("        _P   turn off warnings for pedantic checks");
    Write_Line ("        q*+  turn on warnings for questionable " &
                                                   "missing parenthesis");
    Write_Line ("        Q    turn off warnings for questionable " &


diff --git a/gcc/ada/warnsw.adb b/gcc/ada/warnsw.adb
--- a/gcc/ada/warnsw.adb
+++ b/gcc/ada/warnsw.adb
@@ -76,6 +76,7 @@  package body Warnsw is
       Warn_On_Overlap                      := Setting;
       Warn_On_Overridden_Size              := Setting;
       Warn_On_Parameter_Order              := Setting;
+      Warn_On_Pedantic_Checks              := Setting;
       Warn_On_Questionable_Layout          := Setting;
       Warn_On_Questionable_Missing_Parens  := Setting;
       Warn_On_Record_Holes                 := Setting;
@@ -172,6 +173,8 @@  package body Warnsw is
         W.Warn_On_Overridden_Size;
       Warn_On_Parameter_Order              :=
         W.Warn_On_Parameter_Order;
+      Warn_On_Pedantic_Checks              :=
+        W.Warn_On_Pedantic_Checks;
       Warn_On_Questionable_Layout          :=
         W.Warn_On_Questionable_Layout;
       Warn_On_Questionable_Missing_Parens  :=
@@ -284,6 +287,8 @@  package body Warnsw is
         Warn_On_Overridden_Size;
       W.Warn_On_Parameter_Order              :=
         Warn_On_Parameter_Order;
+      W.Warn_On_Pedantic_Checks              :=
+        Warn_On_Pedantic_Checks;
       W.Warn_On_Questionable_Layout          :=
         Warn_On_Questionable_Layout;
       W.Warn_On_Questionable_Missing_Parens  :=
@@ -505,6 +510,12 @@  package body Warnsw is
          when 'C' =>
             Warn_On_Unknown_Compile_Time_Warning := False;
 
+         when 'p' =>
+            Warn_On_Pedantic_Checks := True;
+
+         when 'P' =>
+            Warn_On_Pedantic_Checks := False;
+
          when 'r' =>
             Warn_On_Component_Order := True;
 


diff --git a/gcc/ada/warnsw.ads b/gcc/ada/warnsw.ads
--- a/gcc/ada/warnsw.ads
+++ b/gcc/ada/warnsw.ads
@@ -58,6 +58,13 @@  package Warnsw is
    --  set with an explicit size clause. Off by default, modified by use of
    --  -gnatw.s/.S (but not -gnatwa).
 
+   Warn_On_Pedantic_Checks : Boolean := False;
+   --  Warn for violation of miscellaneous pedantic rules (such as when the
+   --  subtype of a formal parameter given in a subprogram body's specification
+   --  comes from a different subtype declaration that the subtype of the
+   --  formal in the subprogram declaration). Off by default, and set by
+   --  -gnatw_p (but not -gnatwa).
+
    Warn_On_Questionable_Layout : Boolean := False;
    --  Warn when default layout of a record type is questionable for run-time
    --  efficiency reasons and would be improved by reordering the components.
@@ -128,6 +135,7 @@  package Warnsw is
       Warn_On_Overlap                      : Boolean;
       Warn_On_Overridden_Size              : Boolean;
       Warn_On_Parameter_Order              : Boolean;
+      Warn_On_Pedantic_Checks              : Boolean;
       Warn_On_Questionable_Layout          : Boolean;
       Warn_On_Questionable_Missing_Parens  : Boolean;
       Warn_On_Record_Holes                 : Boolean;