[Ada] Improve messages on incorrect state refinement in SPARK
gcc/ada/ * sem_ch10.adb (Is_Private_Library_Unit): Move query to Sem_Util for sharing. * sem_ch7.adb (Analyze_Package_Body_Helper): Add continuation message. * sem_prag.adb (Analyze_Part_Of): Call new function Is_Private_Library_Unit. (Check_Valid_Library_Unit_Pragma): Specialize error messages on misplaced pragmas. (Analyze_Refined_State_In_Decl_Part): Recognize missing Part_Of on object in private part. * sem_util.adb (Check_State_Refinements): Add continuation message. (Find_Placement_In_State_Space): Fix detection of placement, which relied wrongly on queries In_Package_Body/In_Private_Part which do not provide the right information here for all cases. (Is_Private_Library_Unit): Move query here for sharing. * sem_util.ads (Is_Private_Library_Unit): Move query here for sharing.
This commit is contained in:
parent
7b4069fb7c
commit
aeaabe7b3c
|
@ -2952,23 +2952,6 @@ package body Sem_Ch10 is
|
|||
Par_Lib : Entity_Id;
|
||||
Par_Spec : Node_Id;
|
||||
|
||||
function Is_Private_Library_Unit (Unit : Entity_Id) return Boolean;
|
||||
-- Returns true if and only if the library unit is declared with
|
||||
-- an explicit designation of private.
|
||||
|
||||
-----------------------------
|
||||
-- Is_Private_Library_Unit --
|
||||
-----------------------------
|
||||
|
||||
function Is_Private_Library_Unit (Unit : Entity_Id) return Boolean is
|
||||
Comp_Unit : constant Node_Id := Parent (Unit_Declaration_Node (Unit));
|
||||
|
||||
begin
|
||||
return Private_Present (Comp_Unit);
|
||||
end Is_Private_Library_Unit;
|
||||
|
||||
-- Start of processing for Check_Private_Child_Unit
|
||||
|
||||
begin
|
||||
if Nkind (Lib_Unit) in N_Package_Body | N_Subprogram_Body then
|
||||
Curr_Unit := Defining_Entity (Unit (Library_Unit (N)));
|
||||
|
|
|
@ -759,6 +759,8 @@ package body Sem_Ch7 is
|
|||
("optional package body (not allowed in Ada 95)??", N);
|
||||
else
|
||||
Error_Msg_N ("spec of this package does not allow a body", N);
|
||||
Error_Msg_N ("\either remove the body or add pragma "
|
||||
& "Elaborate_Body in the spec", N);
|
||||
end if;
|
||||
end if;
|
||||
end if;
|
||||
|
|
|
@ -3453,9 +3453,7 @@ package body Sem_Prag is
|
|||
|
||||
Parent_Unit := Pack_Id;
|
||||
while Present (Parent_Unit) loop
|
||||
exit when
|
||||
Private_Present
|
||||
(Parent (Unit_Declaration_Node (Parent_Unit)));
|
||||
exit when Is_Private_Library_Unit (Parent_Unit);
|
||||
Parent_Unit := Scope (Parent_Unit);
|
||||
end loop;
|
||||
|
||||
|
@ -3503,17 +3501,80 @@ package body Sem_Prag is
|
|||
-- encapsulating state must be declared in the same package.
|
||||
|
||||
elsif Placement = Private_State_Space then
|
||||
if Scope (Encap_Id) /= Pack_Id then
|
||||
SPARK_Msg_NE
|
||||
("indicator Part_Of must denote an abstract state of "
|
||||
& "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
|
||||
|
||||
Error_Msg_Name_1 := Chars (Pack_Id);
|
||||
SPARK_Msg_NE
|
||||
("\& is declared in the private part of package %",
|
||||
Indic, Item_Id);
|
||||
return;
|
||||
end if;
|
||||
-- In the case of the abstract state of a nongeneric private
|
||||
-- child package, it may be encapsulated in the state of a
|
||||
-- public descendant of its parent package.
|
||||
|
||||
declare
|
||||
function Is_Public_Descendant
|
||||
(Child, Ancestor : Entity_Id)
|
||||
return Boolean;
|
||||
-- Return True if Child is a public descendant of Pack
|
||||
|
||||
--------------------------
|
||||
-- Is_Public_Descendant --
|
||||
--------------------------
|
||||
|
||||
function Is_Public_Descendant
|
||||
(Child, Ancestor : Entity_Id)
|
||||
return Boolean
|
||||
is
|
||||
P : Entity_Id := Child;
|
||||
begin
|
||||
while Is_Child_Unit (P)
|
||||
and then not Is_Private_Library_Unit (P)
|
||||
loop
|
||||
if Scope (P) = Ancestor then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
P := Scope (P);
|
||||
end loop;
|
||||
|
||||
return False;
|
||||
end Is_Public_Descendant;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Immediate_Pack_Id : constant Entity_Id := Scope (Item_Id);
|
||||
|
||||
Is_State_Of_Private_Child : constant Boolean :=
|
||||
Is_Child_Unit (Immediate_Pack_Id)
|
||||
and then not Is_Generic_Unit (Immediate_Pack_Id)
|
||||
and then Is_Private_Descendant (Immediate_Pack_Id);
|
||||
|
||||
Is_OK_Through_Sibling : Boolean := False;
|
||||
|
||||
begin
|
||||
if Ekind (Item_Id) = E_Abstract_State
|
||||
and then Is_State_Of_Private_Child
|
||||
and then Is_Public_Descendant (Scope (Encap_Id), Pack_Id)
|
||||
then
|
||||
Is_OK_Through_Sibling := True;
|
||||
end if;
|
||||
|
||||
if Scope (Encap_Id) /= Pack_Id
|
||||
and then not Is_OK_Through_Sibling
|
||||
then
|
||||
if Is_State_Of_Private_Child then
|
||||
SPARK_Msg_NE
|
||||
("indicator Part_Of must denote abstract state of & "
|
||||
& "or of its public descendant "
|
||||
& "(SPARK RM 7.2.6(3))", Indic, Pack_Id);
|
||||
else
|
||||
SPARK_Msg_NE
|
||||
("indicator Part_Of must denote an abstract state of "
|
||||
& "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
|
||||
end if;
|
||||
|
||||
Error_Msg_Name_1 := Chars (Pack_Id);
|
||||
SPARK_Msg_NE
|
||||
("\& is declared in the private part of package %",
|
||||
Indic, Item_Id);
|
||||
return;
|
||||
end if;
|
||||
end;
|
||||
|
||||
-- Items declared in the body state space of a package do not need
|
||||
-- Part_Of indicators as the refinement has already been seen.
|
||||
|
@ -6612,7 +6673,9 @@ package body Sem_Prag is
|
|||
|
||||
elsif Nkind (Parent_Node) = N_Compilation_Unit_Aux then
|
||||
if Plist /= Pragmas_After (Parent_Node) then
|
||||
Pragma_Misplaced;
|
||||
Error_Pragma
|
||||
("pragma% misplaced, must be inside or after the "
|
||||
& "compilation unit");
|
||||
|
||||
elsif Arg_Count = 0 then
|
||||
Error_Pragma
|
||||
|
@ -6679,26 +6742,36 @@ package body Sem_Prag is
|
|||
Unit_Node := Unit_Declaration_Node (Current_Scope);
|
||||
Unit_Kind := Nkind (Unit_Node);
|
||||
|
||||
if Nkind (Parent (Unit_Node)) /= N_Compilation_Unit then
|
||||
Pragma_Misplaced;
|
||||
if Unit_Node = Standard_Package_Node then
|
||||
Error_Pragma
|
||||
("pragma% misplaced, must be inside or after the "
|
||||
& "compilation unit");
|
||||
|
||||
elsif Nkind (Parent (Unit_Node)) /= N_Compilation_Unit then
|
||||
Error_Pragma
|
||||
("pragma% misplaced, must be on library unit");
|
||||
|
||||
elsif Unit_Kind = N_Subprogram_Body
|
||||
and then not Acts_As_Spec (Unit_Node)
|
||||
then
|
||||
Pragma_Misplaced;
|
||||
Error_Pragma
|
||||
("pragma% misplaced, must be on the subprogram spec");
|
||||
|
||||
elsif Nkind (Parent_Node) = N_Package_Body then
|
||||
Pragma_Misplaced;
|
||||
Error_Pragma
|
||||
("pragma% misplaced, must be on the package spec");
|
||||
|
||||
elsif Nkind (Parent_Node) = N_Package_Specification
|
||||
and then Plist = Private_Declarations (Parent_Node)
|
||||
then
|
||||
Pragma_Misplaced;
|
||||
Error_Pragma
|
||||
("pragma% misplaced, must be in the public part");
|
||||
|
||||
elsif Nkind (Parent_Node) in N_Generic_Declaration
|
||||
and then Plist = Generic_Formal_Declarations (Parent_Node)
|
||||
then
|
||||
Pragma_Misplaced;
|
||||
Error_Pragma
|
||||
("pragma% misplaced, must not be in formal part");
|
||||
|
||||
elsif Arg_Count > 0 then
|
||||
Analyze (Get_Pragma_Arg (Arg1));
|
||||
|
@ -28761,13 +28834,17 @@ package body Sem_Prag is
|
|||
Placement => Placement,
|
||||
Pack_Id => Pack_Id);
|
||||
|
||||
-- The constituent is part of the visible state of a
|
||||
-- private child package, but lacks a Part_Of indicator.
|
||||
-- The constituent is either part of the hidden state of
|
||||
-- the package or 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)
|
||||
if (Placement = Private_State_Space
|
||||
and then Pack_Id = Spec_Id)
|
||||
or else
|
||||
(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
|
||||
|
|
|
@ -5246,6 +5246,8 @@ package body Sem_Util is
|
|||
and then not Has_Non_Null_Refinement (State_Id)
|
||||
then
|
||||
Error_Msg_N ("state & requires refinement", State_Id);
|
||||
Error_Msg_N ("\package body should have Refined_State "
|
||||
& "for state & with constituents", State_Id);
|
||||
end if;
|
||||
|
||||
Next_Elmt (State_Elmt);
|
||||
|
@ -9586,35 +9588,88 @@ package body Sem_Util is
|
|||
Placement : out State_Space_Kind;
|
||||
Pack_Id : out Entity_Id)
|
||||
is
|
||||
function Inside_Package_Body (Id : Entity_Id) return Boolean;
|
||||
function Inside_Private_Part (Id : Entity_Id) return Boolean;
|
||||
-- Return True if Id is declared directly within the package body
|
||||
-- and the package private parts, respectively. We cannot use
|
||||
-- In_Private_Part/In_Body_Part flags, as these are only set during the
|
||||
-- analysis of the package itself, while Find_Placement_In_State_Space
|
||||
-- can be called on an entity of another package.
|
||||
|
||||
------------------------
|
||||
-- Inside_Package_Body --
|
||||
------------------------
|
||||
|
||||
function Inside_Package_Body (Id : Entity_Id) return Boolean is
|
||||
Spec_Id : constant Entity_Id := Scope (Id);
|
||||
Body_Decl : constant Opt_N_Package_Body_Id := Package_Body (Spec_Id);
|
||||
Decl : constant Node_Id := Enclosing_Declaration (Id);
|
||||
begin
|
||||
if Present (Body_Decl)
|
||||
and then Is_List_Member (Decl)
|
||||
and then List_Containing (Decl) = Declarations (Body_Decl)
|
||||
then
|
||||
return True;
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
end Inside_Package_Body;
|
||||
|
||||
-------------------------
|
||||
-- Inside_Private_Part --
|
||||
-------------------------
|
||||
|
||||
function Inside_Private_Part (Id : Entity_Id) return Boolean is
|
||||
Spec_Id : constant Entity_Id := Scope (Id);
|
||||
Private_Decls : constant List_Id :=
|
||||
Private_Declarations (Package_Specification (Spec_Id));
|
||||
Decl : constant Node_Id := Enclosing_Declaration (Id);
|
||||
begin
|
||||
if Is_List_Member (Decl)
|
||||
and then List_Containing (Decl) = Private_Decls
|
||||
then
|
||||
return True;
|
||||
|
||||
elsif Ekind (Id) = E_Package
|
||||
and then Is_Private_Library_Unit (Id)
|
||||
then
|
||||
return True;
|
||||
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
end Inside_Private_Part;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Context : Entity_Id;
|
||||
|
||||
-- Start of processing for Find_Placement_In_State_Space
|
||||
|
||||
begin
|
||||
-- Assume that the item does not appear in the state space of a package
|
||||
|
||||
Placement := Not_In_Package;
|
||||
Pack_Id := Empty;
|
||||
|
||||
-- Climb the scope stack and examine the enclosing context
|
||||
|
||||
Context := Scope (Item_Id);
|
||||
while Present (Context) and then Context /= Standard_Standard loop
|
||||
if Is_Package_Or_Generic_Package (Context) then
|
||||
Pack_Id := Context;
|
||||
Context := Item_Id;
|
||||
Pack_Id := Scope (Context);
|
||||
while Present (Pack_Id) and then Pack_Id /= Standard_Standard loop
|
||||
if Is_Package_Or_Generic_Package (Pack_Id) then
|
||||
|
||||
-- A package body is a cut off point for the traversal as the item
|
||||
-- cannot be visible to the outside from this point on. Note that
|
||||
-- this test must be done first as a body is also classified as a
|
||||
-- private part.
|
||||
-- A package body is a cut off point for the traversal as the
|
||||
-- item cannot be visible to the outside from this point on.
|
||||
|
||||
if In_Package_Body (Context) then
|
||||
if Inside_Package_Body (Context) then
|
||||
Placement := Body_State_Space;
|
||||
return;
|
||||
|
||||
-- The private part of a package is a cut off point for the
|
||||
-- traversal as the item cannot be visible to the outside from
|
||||
-- this point on.
|
||||
-- traversal as the item cannot be visible to the outside
|
||||
-- from this point on.
|
||||
|
||||
elsif In_Private_Part (Context) then
|
||||
elsif Inside_Private_Part (Context) then
|
||||
Placement := Private_State_Space;
|
||||
return;
|
||||
|
||||
|
@ -9626,9 +9681,11 @@ package body Sem_Util is
|
|||
Placement := Visible_State_Space;
|
||||
|
||||
-- The visible state space of a child unit acts as the proper
|
||||
-- placement of an item.
|
||||
-- placement of an item, unless this is a private child unit.
|
||||
|
||||
if Is_Child_Unit (Context) then
|
||||
if Is_Child_Unit (Pack_Id)
|
||||
and then not Is_Private_Library_Unit (Pack_Id)
|
||||
then
|
||||
return;
|
||||
end if;
|
||||
end if;
|
||||
|
@ -9638,10 +9695,12 @@ package body Sem_Util is
|
|||
|
||||
else
|
||||
Placement := Not_In_Package;
|
||||
Pack_Id := Empty;
|
||||
return;
|
||||
end if;
|
||||
|
||||
Context := Scope (Context);
|
||||
Pack_Id := Scope (Context);
|
||||
end loop;
|
||||
end Find_Placement_In_State_Space;
|
||||
|
||||
|
@ -20308,6 +20367,17 @@ package body Sem_Util is
|
|||
return False;
|
||||
end Is_Preelaborable_Function;
|
||||
|
||||
-----------------------------
|
||||
-- Is_Private_Library_Unit --
|
||||
-----------------------------
|
||||
|
||||
function Is_Private_Library_Unit (Unit : Entity_Id) return Boolean is
|
||||
Comp_Unit : constant Node_Id := Parent (Unit_Declaration_Node (Unit));
|
||||
begin
|
||||
return Nkind (Comp_Unit) = N_Compilation_Unit
|
||||
and then Private_Present (Comp_Unit);
|
||||
end Is_Private_Library_Unit;
|
||||
|
||||
---------------------------------
|
||||
-- Is_Protected_Self_Reference --
|
||||
---------------------------------
|
||||
|
|
|
@ -2276,6 +2276,10 @@ package Sem_Util is
|
|||
-- Is_Non_Preelaborable_Construct takes into account the syntactic
|
||||
-- and semantic properties of N for a more accurate diagnostic.
|
||||
|
||||
function Is_Private_Library_Unit (Unit : Entity_Id) return Boolean;
|
||||
-- Returns True if and only if the library unit is declared with an
|
||||
-- explicit designation of private.
|
||||
|
||||
function Is_Protected_Self_Reference (N : Node_Id) return Boolean;
|
||||
-- Return True if node N denotes a protected type name which represents
|
||||
-- the current instance of a protected object according to RM 9.4(21/2).
|
||||
|
|
Loading…
Reference in New Issue