@@ -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).