Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 237961)
+++ sem_prag.adb	(working copy)
@@ -26395,7 +26395,11 @@
    -- Build_Classwide_Expression --
    --------------------------------
 
-   procedure Build_Classwide_Expression (Prag : Node_Id; Subp : Entity_Id) is
+   procedure Build_Classwide_Expression
+     (Prag        : Node_Id;
+      Subp        : Entity_Id;
+      Adjust_Sloc : Boolean)
+   is
       function Replace_Entity (N : Node_Id) return Traverse_Result;
       --  Replace reference to formal of inherited operation or to primitive
       --  operation of root type, with corresponding entity for derived type,
@@ -26410,6 +26414,10 @@
          New_E : Entity_Id;
 
       begin
+         if Adjust_Sloc then
+            Adjust_Inherited_Pragma_Sloc (N);
+         end if;
+
          if Nkind (N) = N_Identifier
            and then Present (Entity (N))
            and then
@@ -26576,15 +26584,22 @@
             Next_Formal (Inher_Formal);
             Next_Formal (Subp_Formal);
          end loop;
-      end if;
 
-      --  Copy the original pragma while performing substitutions (if
-      --  applicable).
+         --  Use generic machinery to copy inherited pragma, as if it were an
+         --  instantiation, resetting source locations appropriately, so that
+         --  expressions inside the inherited pragma use chained locations.
+         --  This is used in particular in GNATprove to locate precisely
+         --  messages on a given inherited pragma.
 
-      Check_Prag := New_Copy_Tree (Source => Prag);
+         Set_Copied_Sloc_For_Inherited_Pragma
+           (Unit_Declaration_Node (Subp_Id), Inher_Id);
+         Check_Prag := New_Copy_Tree (Source => Prag);
+         Build_Classwide_Expression (Check_Prag, Subp_Id, Adjust_Sloc => True);
 
-      if Present (Inher_Id) then
-         Build_Classwide_Expression (Check_Prag, Subp_Id);
+      --  Otherwise simply copy the original pragma
+
+      else
+         Check_Prag := New_Copy_Tree (Source => Prag);
       end if;
 
       --  Mark the pragma as being internally generated and reset the Analyzed
Index: sem_prag.ads
===================================================================
--- sem_prag.ads	(revision 237962)
+++ sem_prag.ads	(working copy)
@@ -244,16 +244,21 @@
    procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
    --  Perform preanalysis of pragma Test_Case
 
-   procedure Build_Classwide_Expression (Prag : Node_Id; Subp : Entity_Id);
+   procedure Build_Classwide_Expression
+     (Prag        : Node_Id;
+      Subp        : Entity_Id;
+      Adjust_Sloc : Boolean);
    --  Build the expression for an inherited classwide condition. Prag is
    --  the pragma constructed from the corresponding aspect of the parent
-   --  subprogram, and Subp is the overridding operation.
-   --  The routine is also called to check whether an inherited operation
-   --  that is not overridden but has inherited conditions need a wrapper,
-   --  because the inherited condition includes calls to other primitives that
-   --  have been overridden. In that case the first argument is the expression
-   --  of the original classwide aspect. In SPARK_Mode, such operation which
-   --  are just inherited but have modified pre/postconditions are illegal.
+   --  subprogram, and Subp is the overridding operation. Adjust_Sloc is True
+   --  when the sloc of nodes traversed should be adjusted for the inherited
+   --  pragma. The routine is also called to check whether an inherited
+   --  operation that is not overridden but has inherited conditions need
+   --  a wrapper, because the inherited condition includes calls to other
+   --  primitives that have been overridden. In that case the first argument
+   --  is the expression of the original classwide aspect. In SPARK_Mode, such
+   --  operation which are just inherited but have modified pre/postconditions
+   --  are illegal.
 
    function Build_Pragma_Check_Equivalent
      (Prag           : Node_Id;
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb	(revision 237957)
+++ sem_ch12.adb	(working copy)
@@ -1052,6 +1052,15 @@
           SPARK_Mode_Pragma        => SPARK_Mode_Pragma));
    end Add_Pending_Instantiation;
 
+   ----------------------------------
+   -- Adjust_Inherited_Pragma_Sloc --
+   ----------------------------------
+
+   procedure Adjust_Inherited_Pragma_Sloc (N : Node_Id) is
+   begin
+      Adjust_Instantiation_Sloc (N, S_Adjustment);
+   end Adjust_Inherited_Pragma_Sloc;
+
    --------------------------
    -- Analyze_Associations --
    --------------------------
@@ -2641,7 +2650,7 @@
       end if;
 
       Formal := New_Copy (Pack_Id);
-      Create_Instantiation_Source (N, Gen_Unit, False, S_Adjustment);
+      Create_Instantiation_Source (N, Gen_Unit, S_Adjustment);
 
       --  Make local generic without formals. The formals will be replaced with
       --  internal declarations.
@@ -3786,7 +3795,7 @@
          --  validate an actual package, the instantiation environment is that
          --  of the enclosing instance.
 
-         Create_Instantiation_Source (N, Gen_Unit, False, S_Adjustment);
+         Create_Instantiation_Source (N, Gen_Unit, S_Adjustment);
 
          --  Copy original generic tree, to produce text for instantiation
 
@@ -5138,7 +5147,7 @@
          Generic_Renamings.Set_Last (0);
          Generic_Renamings_HTable.Reset;
 
-         Create_Instantiation_Source (N, Gen_Unit, False, S_Adjustment);
+         Create_Instantiation_Source (N, Gen_Unit, S_Adjustment);
 
          --  Copy original generic tree, to produce text for instantiation
 
@@ -7646,7 +7655,6 @@
                Create_Instantiation_Source
                  (Instantiation_Node,
                   Defining_Entity (N),
-                  False,
                   S_Adjustment);
             end if;
 
@@ -10888,7 +10896,7 @@
          Gen_Body := Unit_Declaration_Node (Gen_Body_Id);
 
          Create_Instantiation_Source
-           (Inst_Node, Gen_Body_Id, False, S_Adjustment);
+           (Inst_Node, Gen_Body_Id, S_Adjustment);
 
          Act_Body :=
            Copy_Generic_Node
@@ -11229,7 +11237,6 @@
          Create_Instantiation_Source
            (Inst_Node,
             Gen_Body_Id,
-            False,
             S_Adjustment);
 
          Act_Body :=
@@ -15139,13 +15146,30 @@
       end loop;
    end Save_Global_References_In_Aspects;
 
+   ------------------------------------------
+   -- Set_Copied_Sloc_For_Inherited_Pragma --
+   ------------------------------------------
+
+   procedure Set_Copied_Sloc_For_Inherited_Pragma
+     (N : Node_Id;
+      E : Entity_Id) is
+   begin
+      Create_Instantiation_Source (N, E,
+        Inlined_Body     => False,
+        Inherited_Pragma => True,
+        A                => S_Adjustment);
+   end Set_Copied_Sloc_For_Inherited_Pragma;
+
    --------------------------------------
    -- Set_Copied_Sloc_For_Inlined_Body --
    --------------------------------------
 
    procedure Set_Copied_Sloc_For_Inlined_Body (N : Node_Id; E : Entity_Id) is
    begin
-      Create_Instantiation_Source (N, E, True, S_Adjustment);
+      Create_Instantiation_Source (N, E,
+        Inlined_Body     => True,
+        Inherited_Pragma => False,
+        A                => S_Adjustment);
    end Set_Copied_Sloc_For_Inlined_Body;
 
    ---------------------
Index: sem_ch12.ads
===================================================================
--- sem_ch12.ads	(revision 237957)
+++ sem_ch12.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, 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- --
@@ -172,6 +172,32 @@
    --  saved as part of the internal state of the Sem_Ch12 package for use
    --  in subsequent calls to copy nodes.
 
+   procedure Set_Copied_Sloc_For_Inherited_Pragma
+     (N : Node_Id;
+      E : Entity_Id);
+   --  This procedure is used when a class-wide pre- or postcondition is
+   --  inherited. This process shares the same circuitry as the creation of
+   --  an instantiated copy of a generic template. The call to this procedure
+   --  establishes a new source file entry representing the inherited pragma
+   --  as an instantiation, marked as an inherited pragma (so that errout can
+   --  distinguish cases for generating error messages, otherwise the treatment
+   --  is identical). In this call N is the subprogram declaration from
+   --  which the pragma is inherited and E is the defining identifier of
+   --  the overridding subprogram (when the subprogram is redefined) or the
+   --  defining identifier of the extension type (when the subprogram is
+   --  inherited). The resulting Sloc adjustment factor is saved as part of the
+   --  internal state of the Sem_Ch12 package for use in subsequent calls to
+   --  copy nodes.
+
+   procedure Adjust_Inherited_Pragma_Sloc (N : Node_Id);
+   --  This procedure is used when a class-wide pre- or postcondition
+   --  is inherited. It is called on each node of the pragma expression
+   --  to adjust its sloc. These call should be preceded by a call to
+   --  Set_Copied_Sloc_For_Inherited_Pragma that sets the required sloc
+   --  adjustment. This is done directly, instead of using Copy_Generic_Node
+   --  to copy nodes and adjust slocs, as Copy_Generic_Node expects a specific
+   --  structure to be in place, which is not the case for inherited pragmas.
+
    procedure Save_Env
      (Gen_Unit : Entity_Id;
       Act_Unit : Entity_Id);
Index: freeze.adb
===================================================================
--- freeze.adb	(revision 237962)
+++ freeze.adb	(working copy)
@@ -1440,13 +1440,15 @@
             A_Pre    := Find_Aspect (Par_Prim, Aspect_Pre);
 
             if Present (A_Pre) and then Class_Present (A_Pre) then
-               Build_Classwide_Expression (Expression (A_Pre), Prim);
+               Build_Classwide_Expression (Expression (A_Pre), Prim,
+                                           Adjust_Sloc => False);
             end if;
 
             A_Post := Find_Aspect (Par_Prim, Aspect_Post);
 
             if Present (A_Post) and then Class_Present (A_Post) then
-               Build_Classwide_Expression (Expression (A_Post), Prim);
+               Build_Classwide_Expression (Expression (A_Post), Prim,
+                                           Adjust_Sloc => False);
             end if;
          end if;
 
Index: sinput-l.adb
===================================================================
--- sinput-l.adb	(revision 237957)
+++ sinput-l.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, 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- --
@@ -121,10 +121,11 @@
    ---------------------------------
 
    procedure Create_Instantiation_Source
-     (Inst_Node    : Entity_Id;
-      Template_Id  : Entity_Id;
-      Inlined_Body : Boolean;
-      A            : out Sloc_Adjustment)
+     (Inst_Node        : Entity_Id;
+      Template_Id      : Entity_Id;
+      A                : out Sloc_Adjustment;
+      Inlined_Body     : Boolean := False;
+      Inherited_Pragma : Boolean := False)
    is
       Dnod : constant Node_Id := Declaration_Node (Template_Id);
       Xold : Source_File_Index;
@@ -145,16 +146,21 @@
          Inst_Spec : Node_Id;
 
       begin
-         Snew.Inlined_Body  := Inlined_Body;
-         Snew.Template      := Xold;
+         Snew.Inlined_Body     := Inlined_Body;
+         Snew.Inherited_Pragma := Inherited_Pragma;
+         Snew.Template         := Xold;
 
-         --  For a genuine generic instantiation, assign new instance id.
-         --  For inlined bodies, we retain that of the template, but we
-         --  save the call location.
+         --  For a genuine generic instantiation, assign new instance id. For
+         --  inlined bodies, we retain that of the template, but we save the
+         --  call location. For inherited pragmas, we simply retain that of
+         --  the template.
 
          if Inlined_Body then
             Snew.Inlined_Call := Sloc (Inst_Node);
 
+         elsif Inherited_Pragma then
+            null;
+
          else
             --  If the spec has been instantiated already, and we are now
             --  creating the instance source for the corresponding body now,
@@ -509,6 +515,7 @@
                   Identifier_Casing   => Unknown,
                   Inlined_Call        => No_Location,
                   Inlined_Body        => False,
+                  Inherited_Pragma    => False,
                   Keyword_Casing      => Unknown,
                   Last_Source_Line    => 1,
                   License             => Unknown,
Index: sinput-l.ads
===================================================================
--- sinput-l.ads	(revision 237957)
+++ sinput-l.ads	(working copy)
@@ -83,19 +83,22 @@
    --  calls to Adjust_Instantiation_Sloc.
 
    procedure Create_Instantiation_Source
-     (Inst_Node    : Entity_Id;
-      Template_Id  : Entity_Id;
-      Inlined_Body : Boolean;
-      A            : out Sloc_Adjustment);
+     (Inst_Node        : Entity_Id;
+      Template_Id      : Entity_Id;
+      A                : out Sloc_Adjustment;
+      Inlined_Body     : Boolean := False;
+      Inherited_Pragma : Boolean := False);
    --  This procedure creates the source table entry for an instantiation.
    --  Inst_Node is the instantiation node, and Template_Id is the defining
    --  identifier of the generic declaration or body unit as appropriate.
    --  A is set to an adjustment factor to be used in subsequent calls to
    --  Adjust_Instantiation_Sloc. The instantiation mechanism is also used
-   --  for inlined function and procedure calls. The parameter Inlined_Body
-   --  is set to True in such cases, and False for a generic instantiation.
-   --  This is used for generating error messages that distinguish these
-   --  two cases, otherwise the two cases are handled identically.
+   --  for inlined function and procedure calls. The parameter Inlined_Body is
+   --  set to True in such cases. This is used for generating error messages
+   --  that distinguish these two cases, otherwise the two cases are handled
+   --  identically. Similarly, the instantiation mechanism is also used
+   --  for inherited class-wide pre- and postconditions. The parameter
+   --  Inherited_Pragma is set to True in such cases.
 
    procedure Adjust_Instantiation_Sloc (N : Node_Id; A : Sloc_Adjustment);
    --  The instantiation tree is created by copying the tree of the generic
Index: sinput.adb
===================================================================
--- sinput.adb	(revision 237957)
+++ sinput.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, 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- --
@@ -300,6 +300,17 @@
       end case;
    end Check_For_BOM;
 
+   ---------------------------------
+   -- Comes_From_Inherited_Pragma --
+   ---------------------------------
+
+   function Comes_From_Inherited_Pragma (S : Source_Ptr) return Boolean is
+      SIE : Source_File_Record renames
+              Source_File.Table (Get_Source_File_Index (S));
+   begin
+      return SIE.Inherited_Pragma;
+   end Comes_From_Inherited_Pragma;
+
    -----------------------------
    -- Comes_From_Inlined_Body --
    -----------------------------
@@ -1190,6 +1201,11 @@
       return Source_File.Table (S).Identifier_Casing;
    end Identifier_Casing;
 
+   function Inherited_Pragma (S : SFI) return Boolean is
+   begin
+      return Source_File.Table (S).Inherited_Pragma;
+   end Inherited_Pragma;
+
    function Inlined_Body (S : SFI) return Boolean is
    begin
       return Source_File.Table (S).Inlined_Body;
Index: sinput.ads
===================================================================
--- sinput.ads	(revision 237957)
+++ sinput.ads	(working copy)
@@ -269,6 +269,11 @@
    --    an instance of an inlined body.
    --    ??? Redundant, always equal to (Inlined_Call /= No_Location)
 
+   --  Inherited_Pragma : Boolean;
+   --    This can only be set True if Instantiation has a value other than
+   --    No_Location. If true it indicates that the instantiation is actually
+   --    an inherited class-wide pre- or postcondition.
+
    --  Template : Source_File_Index; (read-only)
    --    Source file index of the source file containing the template if this
    --    is a generic instantiation. Set to No_Source_File for the normal case
@@ -298,6 +303,7 @@
    function Full_Ref_Name     (S : SFI) return File_Name_Type;
    function Identifier_Casing (S : SFI) return Casing_Type;
    function Inlined_Body      (S : SFI) return Boolean;
+   function Inherited_Pragma  (S : SFI) return Boolean;
    function Inlined_Call      (S : SFI) return Source_Ptr;
    function Instance          (S : SFI) return Instance_Id;
    function Keyword_Casing    (S : SFI) return Casing_Type;
@@ -644,6 +650,13 @@
    --  from instantiation of generics, since Instantiation_Location returns a
    --  valid location in both cases.
 
+   function Comes_From_Inherited_Pragma (S : Source_Ptr) return Boolean;
+   pragma Inline (Comes_From_Inherited_Pragma);
+   --  Given a source pointer S, returns whether it comes from an inherited
+   --  pragma. This allows distinguishing these source pointers from those
+   --  that come from instantiation of generics, since Instantiation_Location
+   --  returns a valid location in both cases.
+
    function Top_Level_Location (S : Source_Ptr) return Source_Ptr;
    --  Given a source pointer S, returns the argument unchanged if it is
    --  not in an instantiation. If S is in an instantiation, then it returns
@@ -759,6 +772,7 @@
    pragma Inline (Identifier_Casing);
    pragma Inline (Inlined_Call);
    pragma Inline (Inlined_Body);
+   pragma Inline (Inherited_Pragma);
    pragma Inline (Template);
    pragma Inline (Unit);
 
@@ -824,6 +838,7 @@
       File_Type         : Type_Of_File;
       Inlined_Call      : Source_Ptr;
       Inlined_Body      : Boolean;
+      Inherited_Pragma  : Boolean;
       License           : License_Type;
       Keyword_Casing    : Casing_Type;
       Identifier_Casing : Casing_Type;
@@ -881,7 +896,8 @@
       Time_Stamp          at 60 range 0 .. 8 * Time_Stamp_Length - 1;
       File_Type           at 74 range 0 .. 7;
       Inlined_Call        at 88 range 0 .. 31;
-      Inlined_Body        at 75 range 0 .. 7;
+      Inlined_Body        at 75 range 0 .. 0;
+      Inherited_Pragma    at 75 range 1 .. 1;
       License             at 76 range 0 .. 7;
       Keyword_Casing      at 77 range 0 .. 7;
       Identifier_Casing   at 78 range 0 .. 15;
Index: sinput-c.adb
===================================================================
--- sinput-c.adb	(revision 237957)
+++ sinput-c.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, 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- --
@@ -183,6 +183,7 @@
                Identifier_Casing   => Unknown,
                Inlined_Call        => No_Location,
                Inlined_Body        => False,
+               Inherited_Pragma    => False,
                Keyword_Casing      => Unknown,
                Last_Source_Line    => 1,
                License             => Unknown,
