This patch modifies the way analysis determine whether an assignment is
an ignored Ghost assignment. This is now achieved by preanalyzing a copy
of the left hand side in order to account for potential code generated
by the left hand side itself.
No small reproducer possible.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-11-14 Hristian Kirtchev <kirtc...@adacore.com>
gcc/ada/
* ghost.adb (Ghost_Entity): New routine.
(Mark_And_Set_Ghost_Assignment): Reimplemented.
* sem_ch5.adb (Analyze_Assignment): Assess whether the target of
the assignment is an ignored Ghost entity before analyzing the
left hand side.
* sem_ch8.adb (Find_Direct_Name): Update the subprogram
signature. Do not generate markers and references when they are
not desired.
(Nvis_Messages): Do not execute when errors are not desired.
(Undefined): Do not emit errors when they are not desired.
* sem_ch8.ads (Find_Direct_Name): Update the subprogram
signature and comment on usage.
* sem_util.adb (Ultimate_Prefix): New routine.
* sem_util.ads (Ultimate_Prefix): New routine.--- gcc/ada/ghost.adb
+++ gcc/ada/ghost.adb
@@ -34,6 +34,7 @@ with Nlists; use Nlists;
with Nmake; use Nmake;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
+with Sem_Ch8; use Sem_Ch8;
with Sem_Disp; use Sem_Disp;
with Sem_Eval; use Sem_Eval;
with Sem_Prag; use Sem_Prag;
@@ -64,9 +65,10 @@ package body Ghost is
-- Local subprograms --
-----------------------
- function Ghost_Entity (N : Node_Id) return Entity_Id;
- -- Find the entity of a reference to a Ghost entity. Return Empty if there
- -- is no such entity.
+ function Ghost_Entity (Ref : Node_Id) return Entity_Id;
+ pragma Inline (Ghost_Entity);
+ -- Obtain the entity of a Ghost entity from reference Ref. Return Empty if
+ -- no such entity exists.
procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type);
pragma Inline (Install_Ghost_Mode);
@@ -829,24 +831,18 @@ package body Ghost is
-- Ghost_Entity --
------------------
- function Ghost_Entity (N : Node_Id) return Entity_Id is
- Ref : Node_Id;
+ function Ghost_Entity (Ref : Node_Id) return Entity_Id is
+ Obj_Ref : constant Node_Id := Ultimate_Prefix (Ref);
begin
- -- When the reference denotes a subcomponent, recover the related
+ -- When the reference denotes a subcomponent, recover the related whole
-- object (SPARK RM 6.9(1)).
- Ref := N;
- while Nkind_In (Ref, N_Explicit_Dereference,
- N_Indexed_Component,
- N_Selected_Component,
- N_Slice)
- loop
- Ref := Prefix (Ref);
- end loop;
+ if Is_Entity_Name (Obj_Ref) then
+ return Entity (Obj_Ref);
+
+ -- Otherwise the reference cannot possibly denote a Ghost entity
- if Is_Entity_Name (Ref) then
- return Entity (Ref);
else
return Empty;
end if;
@@ -1181,13 +1177,50 @@ package body Ghost is
-----------------------------------
procedure Mark_And_Set_Ghost_Assignment (N : Node_Id) is
- Id : Entity_Id;
+ Orig_Lhs : constant Node_Id := Name (N);
+ Orig_Ref : constant Node_Id := Ultimate_Prefix (Orig_Lhs);
+
+ Id : Entity_Id;
+ Ref : Node_Id;
begin
+ -- A reference to a whole Ghost object (SPARK RM 6.9(1)) appears as an
+ -- identifier. If the reference has not been analyzed yet, preanalyze a
+ -- copy of the reference to discover the nature of its entity.
+
+ if Nkind (Orig_Ref) = N_Identifier and then not Analyzed (Orig_Ref) then
+ Ref := New_Copy_Tree (Orig_Ref);
+
+ -- Alter the assignment statement by setting its left-hand side to
+ -- the copy.
+
+ Set_Name (N, Ref);
+ Set_Parent (Ref, N);
+
+ -- Preanalysis is carried out by looking for a Ghost entity while
+ -- suppressing all possible side effects.
+
+ Find_Direct_Name
+ (N => Ref,
+ Errors_OK => False,
+ Marker_OK => False,
+ Reference_OK => False);
+
+ -- Restore the original state of the assignment statement
+
+ Set_Name (N, Orig_Lhs);
+
+ -- A potential reference to a Ghost entity is already properly resolved
+ -- when the left-hand side is analyzed.
+
+ else
+ Ref := Orig_Ref;
+ end if;
+
-- An assignment statement becomes Ghost when its target denotes a Ghost
-- object. Install the Ghost mode of the target.
- Id := Ghost_Entity (Name (N));
+ Id := Ghost_Entity (Ref);
if Present (Id) then
if Is_Checked_Ghost_Entity (Id) then
--- gcc/ada/sem_ch5.adb
+++ gcc/ada/sem_ch5.adb
@@ -452,16 +452,16 @@ package body Sem_Ch5 is
-- Local variables
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
+
T1 : Entity_Id;
T2 : Entity_Id;
Save_Full_Analysis : Boolean := False;
-- Force initialization to facilitate static analysis
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
- -- Save the Ghost-related attributes to restore on exit
-
-- Start of processing for Analyze_Assignment
begin
@@ -476,16 +476,12 @@ package body Sem_Ch5 is
Checks => True,
Modes => True);
- -- Analyze the target of the assignment first in case the expression
- -- contains references to Ghost entities. The checks that verify the
- -- proper use of a Ghost entity need to know the enclosing context.
-
- Analyze (Lhs);
-
-- An assignment statement is Ghost when the left hand side denotes a
-- Ghost entity. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly marked as Ghost.
+ Mark_And_Set_Ghost_Assignment (N);
+
if Has_Target_Names (N) then
Current_Assignment := N;
Expander_Mode_Save_And_Set (False);
@@ -495,7 +491,7 @@ package body Sem_Ch5 is
Current_Assignment := Empty;
end if;
- Mark_And_Set_Ghost_Assignment (N);
+ Analyze (Lhs);
Analyze (Rhs);
-- Ensure that we never do an assignment on a variable marked as
--- gcc/ada/sem_ch8.adb
+++ gcc/ada/sem_ch8.adb
@@ -4843,7 +4843,12 @@ package body Sem_Ch8 is
-- Find_Direct_Name --
----------------------
- procedure Find_Direct_Name (N : Node_Id) is
+ procedure Find_Direct_Name
+ (N : Node_Id;
+ Errors_OK : Boolean := True;
+ Marker_OK : Boolean := True;
+ Reference_OK : Boolean := True)
+ is
E : Entity_Id;
E2 : Entity_Id;
Msg : Boolean;
@@ -5096,6 +5101,10 @@ package body Sem_Ch8 is
Item : Node_Id;
begin
+ if not Errors_OK then
+ return;
+ end if;
+
-- Ada 2005 (AI-262): Generate a precise error concerning the
-- Beaujolais effect that was previously detected
@@ -5263,7 +5272,8 @@ package body Sem_Ch8 is
-- Named aggregate should also be handled similarly ???
- if Nkind (N) = N_Identifier
+ if Errors_OK
+ and then Nkind (N) = N_Identifier
and then Nkind (Parent (N)) = N_Case_Statement_Alternative
then
declare
@@ -5299,119 +5309,122 @@ package body Sem_Ch8 is
Set_Entity (N, Any_Id);
Set_Etype (N, Any_Type);
- -- We use the table Urefs to keep track of entities for which we
- -- have issued errors for undefined references. Multiple errors
- -- for a single name are normally suppressed, however we modify
- -- the error message to alert the programmer to this effect.
+ if Errors_OK then
- for J in Urefs.First .. Urefs.Last loop
- if Chars (N) = Chars (Urefs.Table (J).Node) then
- if Urefs.Table (J).Err /= No_Error_Msg
- and then Sloc (N) /= Urefs.Table (J).Loc
- then
- Error_Msg_Node_1 := Urefs.Table (J).Node;
+ -- We use the table Urefs to keep track of entities for which we
+ -- have issued errors for undefined references. Multiple errors
+ -- for a single name are normally suppressed, however we modify
+ -- the error message to alert the programmer to this effect.
- if Urefs.Table (J).Nvis then
- Change_Error_Text (Urefs.Table (J).Err,
- "& is not visible (more references follow)");
- else
- Change_Error_Text (Urefs.Table (J).Err,
- "& is undefined (more references follow)");
- end if;
+ for J in Urefs.First .. Urefs.Last loop
+ if Chars (N) = Chars (Urefs.Table (J).Node) then
+ if Urefs.Table (J).Err /= No_Error_Msg
+ and then Sloc (N) /= Urefs.Table (J).Loc
+ then
+ Error_Msg_Node_1 := Urefs.Table (J).Node;
- Urefs.Table (J).Err := No_Error_Msg;
- end if;
+ if Urefs.Table (J).Nvis then
+ Change_Error_Text (Urefs.Table (J).Err,
+ "& is not visible (more references follow)");
+ else
+ Change_Error_Text (Urefs.Table (J).Err,
+ "& is undefined (more references follow)");
+ end if;
- -- Although we will set Msg False, and thus suppress the
- -- message, we also set Error_Posted True, to avoid any
- -- cascaded messages resulting from the undefined reference.
+ Urefs.Table (J).Err := No_Error_Msg;
+ end if;
- Msg := False;
- Set_Error_Posted (N, True);
- return;
- end if;
- end loop;
+ -- Although we will set Msg False, and thus suppress the
+ -- message, we also set Error_Posted True, to avoid any
+ -- cascaded messages resulting from the undefined reference.
- -- If entry not found, this is first undefined occurrence
+ Msg := False;
+ Set_Error_Posted (N);
+ return;
+ end if;
+ end loop;
- if Nvis then
- Error_Msg_N ("& is not visible!", N);
- Emsg := Get_Msg_Id;
+ -- If entry not found, this is first undefined occurrence
- else
- Error_Msg_N ("& is undefined!", N);
- Emsg := Get_Msg_Id;
+ if Nvis then
+ Error_Msg_N ("& is not visible!", N);
+ Emsg := Get_Msg_Id;
- -- A very bizarre special check, if the undefined identifier
- -- is put or put_line, then add a special error message (since
- -- this is a very common error for beginners to make).
+ else
+ Error_Msg_N ("& is undefined!", N);
+ Emsg := Get_Msg_Id;
- if Nam_In (Chars (N), Name_Put, Name_Put_Line) then
- Error_Msg_N -- CODEFIX
- ("\\possible missing `WITH Ada.Text_'I'O; " &
- "USE Ada.Text_'I'O`!", N);
+ -- A very bizarre special check, if the undefined identifier
+ -- is Put or Put_Line, then add a special error message (since
+ -- this is a very common error for beginners to make).
- -- Another special check if N is the prefix of a selected
- -- component which is a known unit, add message complaining
- -- about missing with for this unit.
+ if Nam_In (Chars (N), Name_Put, Name_Put_Line) then
+ Error_Msg_N -- CODEFIX
+ ("\\possible missing `WITH Ada.Text_'I'O; " &
+ "USE Ada.Text_'I'O`!", N);
- elsif Nkind (Parent (N)) = N_Selected_Component
- and then N = Prefix (Parent (N))
- and then Is_Known_Unit (Parent (N))
- then
- Error_Msg_Node_2 := Selector_Name (Parent (N));
- Error_Msg_N -- CODEFIX
- ("\\missing `WITH &.&;`", Prefix (Parent (N)));
- end if;
+ -- Another special check if N is the prefix of a selected
+ -- component which is a known unit: add message complaining
+ -- about missing with for this unit.
+
+ elsif Nkind (Parent (N)) = N_Selected_Component
+ and then N = Prefix (Parent (N))
+ and then Is_Known_Unit (Parent (N))
+ then
+ Error_Msg_Node_2 := Selector_Name (Parent (N));
+ Error_Msg_N -- CODEFIX
+ ("\\missing `WITH &.&;`", Prefix (Parent (N)));
+ end if;
- -- Now check for possible misspellings
+ -- Now check for possible misspellings
- declare
- E : Entity_Id;
- Ematch : Entity_Id := Empty;
+ declare
+ E : Entity_Id;
+ Ematch : Entity_Id := Empty;
- Last_Name_Id : constant Name_Id :=
- Name_Id (Nat (First_Name_Id) +
- Name_Entries_Count - 1);
+ Last_Name_Id : constant Name_Id :=
+ Name_Id (Nat (First_Name_Id) +
+ Name_Entries_Count - 1);
- begin
- for Nam in First_Name_Id .. Last_Name_Id loop
- E := Get_Name_Entity_Id (Nam);
+ begin
+ for Nam in First_Name_Id .. Last_Name_Id loop
+ E := Get_Name_Entity_Id (Nam);
- if Present (E)
- and then (Is_Immediately_Visible (E)
- or else
- Is_Potentially_Use_Visible (E))
- then
- if Is_Bad_Spelling_Of (Chars (N), Nam) then
- Ematch := E;
- exit;
+ if Present (E)
+ and then (Is_Immediately_Visible (E)
+ or else
+ Is_Potentially_Use_Visible (E))
+ then
+ if Is_Bad_Spelling_Of (Chars (N), Nam) then
+ Ematch := E;
+ exit;
+ end if;
end if;
- end if;
- end loop;
+ end loop;
- if Present (Ematch) then
- Error_Msg_NE -- CODEFIX
- ("\possible misspelling of&", N, Ematch);
- end if;
- end;
- end if;
+ if Present (Ematch) then
+ Error_Msg_NE -- CODEFIX
+ ("\possible misspelling of&", N, Ematch);
+ end if;
+ end;
+ end if;
- -- Make entry in undefined references table unless the full errors
- -- switch is set, in which case by refraining from generating the
- -- table entry, we guarantee that we get an error message for every
- -- undefined reference. The entry is not added if we are ignoring
- -- errors.
+ -- Make entry in undefined references table unless the full errors
+ -- switch is set, in which case by refraining from generating the
+ -- table entry we guarantee that we get an error message for every
+ -- undefined reference. The entry is not added if we are ignoring
+ -- errors.
+
+ if not All_Errors_Mode and then Ignore_Errors_Enable = 0 then
+ Urefs.Append (
+ (Node => N,
+ Err => Emsg,
+ Nvis => Nvis,
+ Loc => Sloc (N)));
+ end if;
- if not All_Errors_Mode and then Ignore_Errors_Enable = 0 then
- Urefs.Append (
- (Node => N,
- Err => Emsg,
- Nvis => Nvis,
- Loc => Sloc (N)));
+ Msg := True;
end if;
-
- Msg := True;
end Undefined;
-- Local variables
@@ -5834,7 +5847,7 @@ package body Sem_Ch8 is
-- If no homonyms were visible, the entity is unambiguous
if not Is_Overloaded (N) then
- if not Is_Actual_Parameter then
+ if Reference_OK and then not Is_Actual_Parameter then
Generate_Reference (E, N);
end if;
end if;
@@ -5853,7 +5866,8 @@ package body Sem_Ch8 is
-- in SPARK mode where renamings are traversed for generating
-- local effects of subprograms.
- if Is_Object (E)
+ if Reference_OK
+ and then Is_Object (E)
and then Present (Renamed_Object (E))
and then not GNATprove_Mode
then
@@ -5883,7 +5897,7 @@ package body Sem_Ch8 is
-- Generate reference unless this is an actual parameter
-- (see comment below)
- if Is_Actual_Parameter then
+ if Reference_OK and then Is_Actual_Parameter then
Generate_Reference (E, N);
Set_Referenced (E, R);
end if;
@@ -5892,7 +5906,7 @@ package body Sem_Ch8 is
-- Normal case, not a label: generate reference
else
- if not Is_Actual_Parameter then
+ if Reference_OK and then not Is_Actual_Parameter then
-- Package or generic package is always a simple reference
@@ -5961,9 +5975,10 @@ package body Sem_Ch8 is
-- reference is a write when it appears on the left hand side of an
-- assignment.
- if Needs_Variable_Reference_Marker
- (N => N,
- Calls_OK => False)
+ if Marker_OK
+ and then Needs_Variable_Reference_Marker
+ (N => N,
+ Calls_OK => False)
then
declare
Is_Assignment_LHS : constant Boolean := Is_LHS (N) = Yes;
--- gcc/ada/sem_ch8.ads
+++ gcc/ada/sem_ch8.ads
@@ -82,7 +82,11 @@ package Sem_Ch8 is
-- Subsidiaries of End_Use_Clauses. Also called directly for use clauses
-- appearing in context clauses.
- procedure Find_Direct_Name (N : Node_Id);
+ procedure Find_Direct_Name
+ (N : Node_Id;
+ Errors_OK : Boolean := True;
+ Marker_OK : Boolean := True;
+ Reference_OK : Boolean := True);
-- Given a direct name (Identifier or Operator_Symbol), this routine scans
-- the homonym chain for the name, searching for corresponding visible
-- entities to find the referenced entity (or in the case of overloading,
@@ -99,6 +103,11 @@ package Sem_Ch8 is
-- entries in the current scope, and that will give all homonyms that are
-- declared before the point of call in the current scope. This is useful
-- for example in the processing for pragma Inline.
+ --
+ -- Flag Errors_OK should be set when error diagnostics are desired. Flag
+ -- Marker_OK should be set when a N_Variable_Reference_Marker needs to be
+ -- generated for a SPARK object in order to detect elaboration issues. Flag
+ -- Reference_OK should be set when N must generate a cross reference.
procedure Find_Selected_Component (N : Node_Id);
-- Resolve various cases of selected components, recognize expanded names
--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -25269,6 +25269,26 @@ package body Sem_Util is
end if;
end Type_Without_Stream_Operation;
+ ---------------------
+ -- Ultimate_Prefix --
+ ---------------------
+
+ function Ultimate_Prefix (N : Node_Id) return Node_Id is
+ Pref : Node_Id;
+
+ begin
+ Pref := N;
+ while Nkind_In (Pref, N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Selected_Component,
+ N_Slice)
+ loop
+ Pref := Prefix (Pref);
+ end loop;
+
+ return Pref;
+ end Ultimate_Prefix;
+
----------------------------
-- Unique_Defining_Entity --
----------------------------
--- gcc/ada/sem_util.ads
+++ gcc/ada/sem_util.ads
@@ -2810,6 +2810,10 @@ package Sem_Util is
-- prevents the construction of a composite stream operation. If Op is
-- specified we check only for the given stream operation.
+ function Ultimate_Prefix (N : Node_Id) return Node_Id;
+ -- Obtain the "outermost" prefix of arbitrary node N. Return N if no such
+ -- prefix exists.
+
function Unique_Defining_Entity (N : Node_Id) return Entity_Id;
-- Return the entity that represents declaration N, so that different
-- views of the same entity have the same unique defining entity:
