===================================================================
@@ -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
===================================================================
@@ -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;
===================================================================
@@ -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;
---------------------
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- 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);
===================================================================
@@ -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;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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,
===================================================================
@@ -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
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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;
===================================================================
@@ -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;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- 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,