OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Refine error messages on illegal Refined_State in SPARK 

gcc/ada/

	* sem_prag.adb (Analyze_Refined_State_In_Decl_Part): Refine the
	error message for missing Part_Of on constituent. Avoid
	cascading error.
This commit is contained in:
Yannick Moy 2020-11-16 21:50:17 +01:00 committed by Pierre-Marie de Rodat
parent 2a1a3fc67f
commit 758daef51b
1 changed files with 76 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

99
gcc/ada/sem_prag.adb
View File

@ -28493,35 +28493,69 @@ package body Sem_Prag is
Constit, Encapsulating_State (Constit_Id));
end if;
-- The only other source of legal constituents is the body
-- state space of the related package.
else
if Present (Body_States) then
State_Elmt := First_Elmt (Body_States);
while Present (State_Elmt) loop
declare
Pack_Id : Entity_Id;
Placement : State_Space_Kind;
begin
-- Find where the constituent lives with respect to the
-- state space.
-- Consume a valid constituent to signal that it has
-- been encountered.
Find_Placement_In_State_Space
(Item_Id => Constit_Id,
Placement => Placement,
Pack_Id => Pack_Id);
if Node (State_Elmt) = Constit_Id then
Remove_Elmt (Body_States, State_Elmt);
Collect_Constituent;
return;
-- The constituent is part of the visible state of a
-- private child package, but lacks a Part_Of indicator.
if Placement = Visible_State_Space
and then Is_Child_Unit (Pack_Id)
and then not Is_Generic_Unit (Pack_Id)
and then Is_Private_Descendant (Pack_Id)
then
Error_Msg_Name_1 := Chars (State_Id);
SPARK_Msg_NE
("& cannot act as constituent of state %",
Constit, Constit_Id);
Error_Msg_Sloc :=
Sloc (Enclosing_Declaration (Constit_Id));
SPARK_Msg_NE
("\missing Part_Of indicator # should specify "
& "encapsulator &",
Constit, State_Id);
-- The only other source of legal constituents is the
-- body state space of the related package.
else
if Present (Body_States) then
State_Elmt := First_Elmt (Body_States);
while Present (State_Elmt) loop
-- Consume a valid constituent to signal that it
-- has been encountered.
if Node (State_Elmt) = Constit_Id then
Remove_Elmt (Body_States, State_Elmt);
Collect_Constituent;
return;
end if;
Next_Elmt (State_Elmt);
end loop;
end if;
Next_Elmt (State_Elmt);
end loop;
end if;
-- At this point it is known that the constituent is
-- not part of the package hidden state and cannot be
-- used in a refinement (SPARK RM 7.2.2(9)).
-- At this point it is known that the constituent is not
-- part of the package hidden state and cannot be used in
-- a refinement (SPARK RM 7.2.2(9)).
Error_Msg_Name_1 := Chars (Spec_Id);
SPARK_Msg_NE
("cannot use & in refinement, constituent is not a hidden "
& "state of package %", Constit, Constit_Id);
Error_Msg_Name_1 := Chars (Spec_Id);
SPARK_Msg_NE
("cannot use & in refinement, constituent is not a "
& "hidden state of package %", Constit, Constit_Id);
end if;
end;
end if;
end Match_Constituent;
@ -28943,6 +28977,25 @@ package body Sem_Prag is
-- in the refinement clause.
Report_Unused_Constituents (Part_Of_Constits);
-- Avoid a cascading error reporting a missing refinement by adding
-- State_Id as dummy constituent of itself.
if Non_Null_Seen
and then not Has_Non_Null_Refinement (State_Id)
then
declare
Constits : Elist_Id := Refinement_Constituents (State_Id);
begin
if No (Constits) then
Constits := New_Elmt_List;
Set_Refinement_Constituents (State_Id, Constits);
end if;
Append_Elmt (State_Id, Constits);
Set_Encapsulating_State (State_Id, State_Id);
end;
end if;
end Analyze_Refinement_Clause;
-----------------------------