diff options
Diffstat (limited to 'gcc/ada/sem_prag.adb')
| -rw-r--r-- | gcc/ada/sem_prag.adb | 359 |
1 files changed, 239 insertions, 120 deletions
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 16113e1..d342906 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -3168,71 +3168,26 @@ package body Sem_Prag is Encap_Id : out Entity_Id; Legal : out Boolean) is - Encap_Typ : Entity_Id; - Item_Decl : Node_Id; - Pack_Id : Entity_Id; - Placement : State_Space_Kind; - Parent_Unit : Entity_Id; + procedure Check_Part_Of_Abstract_State; + pragma Inline (Check_Part_Of_Abstract_State); + -- Verify the legality of indicator Part_Of when the encapsulator is an + -- abstract state. - begin - -- Assume that the indicator is illegal - - Encap_Id := Empty; - Legal := False; - - if Nkind_In (Encap, N_Expanded_Name, - N_Identifier, - N_Selected_Component) - then - Analyze (Encap); - Resolve_State (Encap); - - Encap_Id := Entity (Encap); - - -- The encapsulator is an abstract state - - if Ekind (Encap_Id) = E_Abstract_State then - null; - - -- The encapsulator is a single concurrent type (SPARK RM 9.3) - - elsif Is_Single_Concurrent_Object (Encap_Id) then - null; - - -- Otherwise the encapsulator is not a legal choice - - else - SPARK_Msg_N - ("indicator Part_Of must denote abstract state, single " - & "protected type or single task type", Encap); - return; - end if; - - -- This is a syntax error, always report - - else - Error_Msg_N - ("indicator Part_Of must denote abstract state, single protected " - & "type or single task type", Encap); - return; - end if; - - -- Catch a case where indicator Part_Of denotes the abstract view of a - -- variable which appears as an abstract state (SPARK RM 10.1.2 2). - - if From_Limited_With (Encap_Id) - and then Present (Non_Limited_View (Encap_Id)) - and then Ekind (Non_Limited_View (Encap_Id)) = E_Variable - then - SPARK_Msg_N ("indicator Part_Of must denote abstract state", Encap); - SPARK_Msg_N ("\& denotes abstract view of object", Encap); - return; - end if; + procedure Check_Part_Of_Concurrent_Type; + pragma Inline (Check_Part_Of_Concurrent_Type); + -- Verify the legality of indicator Part_Of when the encapsulator is a + -- single concurrent type. - -- The encapsulator is an abstract state + ---------------------------------- + -- Check_Part_Of_Abstract_State -- + ---------------------------------- - if Ekind (Encap_Id) = E_Abstract_State then + procedure Check_Part_Of_Abstract_State is + Pack_Id : Entity_Id; + Placement : State_Space_Kind; + Parent_Unit : Entity_Id; + begin -- Determine where the object, package instantiation or state lives -- with respect to the enclosing packages or package bodies. @@ -3250,6 +3205,7 @@ package body Sem_Prag is SPARK_Msg_N ("indicator Part_Of cannot appear in this context " & "(SPARK RM 7.2.6(5))", Indic); + Error_Msg_Name_1 := Chars (Scope (Encap_Id)); SPARK_Msg_NE ("\& is not part of the hidden state of package %", @@ -3267,14 +3223,14 @@ package body Sem_Prag is and then Is_Private_Descendant (Pack_Id) then -- A variable or state abstraction which is part of the visible - -- state of a private child unit (or one of its public - -- descendants) must have its Part_Of indicator specified. The - -- Part_Of indicator must denote a state abstraction declared - -- by either the parent unit of the private unit or by a public - -- descendant of that parent unit. + -- state of a private child unit or its public descendants must + -- have its Part_Of indicator specified. The Part_Of indicator + -- must denote a state declared by either the parent unit of + -- the private unit or by a public descendant of that parent + -- unit. - -- Find nearest private ancestor (which can be the current unit - -- itself). + -- Find the nearest private ancestor (which can be the current + -- unit itself). Parent_Unit := Pack_Id; while Present (Parent_Unit) loop @@ -3288,8 +3244,8 @@ package body Sem_Prag is if not Is_Child_Or_Sibling (Pack_Id, Scope (Encap_Id)) then SPARK_Msg_NE - ("indicator Part_Of must denote abstract state of & " - & "or of its public descendant (SPARK RM 7.2.6(3))", + ("indicator Part_Of must denote abstract state of & or of " + & "its public descendant (SPARK RM 7.2.6(3))", Indic, Parent_Unit); return; @@ -3302,8 +3258,8 @@ package body Sem_Prag is else SPARK_Msg_NE - ("indicator Part_Of must denote abstract state of & " - & "or of its public descendant (SPARK RM 7.2.6(3))", + ("indicator Part_Of must denote abstract state of & or of " + & "its public descendant (SPARK RM 7.2.6(3))", Indic, Parent_Unit); return; end if; @@ -3315,6 +3271,7 @@ package body Sem_Prag is SPARK_Msg_N ("indicator Part_Of cannot appear in this context " & "(SPARK RM 7.2.6(5))", Indic); + Error_Msg_Name_1 := Chars (Pack_Id); SPARK_Msg_NE ("\& is declared in the visible part of package %", @@ -3330,6 +3287,7 @@ package body Sem_Prag is 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 %", @@ -3354,11 +3312,77 @@ package body Sem_Prag is return; end if; - -- The encapsulator is a single concurrent type + -- At this point it is known that the Part_Of indicator is legal - else - Encap_Typ := Etype (Encap_Id); + Legal := True; + end Check_Part_Of_Abstract_State; + + ----------------------------------- + -- Check_Part_Of_Concurrent_Type -- + ----------------------------------- + procedure Check_Part_Of_Concurrent_Type is + function In_Proper_Order + (First : Node_Id; + Second : Node_Id) return Boolean; + pragma Inline (In_Proper_Order); + -- Determine whether node First precedes node Second + + procedure Placement_Error; + pragma Inline (Placement_Error); + -- Emit an error concerning the illegal placement of the item with + -- respect to the single concurrent type. + + --------------------- + -- In_Proper_Order -- + --------------------- + + function In_Proper_Order + (First : Node_Id; + Second : Node_Id) return Boolean + is + N : Node_Id; + + begin + if List_Containing (First) = List_Containing (Second) then + N := First; + while Present (N) loop + if N = Second then + return True; + end if; + + Next (N); + end loop; + end if; + + return False; + end In_Proper_Order; + + --------------------- + -- Placement_Error -- + --------------------- + + procedure Placement_Error is + begin + SPARK_Msg_N + ("indicator Part_Of must denote a previously declared single " + & "protected type or single task type", Encap); + end Placement_Error; + + -- Local variables + + Conc_Typ : constant Entity_Id := Etype (Encap_Id); + Encap_Decl : constant Node_Id := Declaration_Node (Encap_Id); + Encap_Context : constant Node_Id := Parent (Encap_Decl); + + Item_Context : Node_Id; + Item_Decl : Node_Id; + Prv_Decls : List_Id; + Vis_Decls : List_Id; + + -- Start of processing for Check_Part_Of_Concurrent_Type + + begin -- Only abstract states and variables can act as constituents of an -- encapsulating single concurrent type. @@ -3370,7 +3394,7 @@ package body Sem_Prag is elsif Ekind (Item_Id) = E_Constant then Error_Msg_Name_1 := Chars (Encap_Id); SPARK_Msg_NE - (Fix_Msg (Encap_Typ, "constant & cannot act as constituent of " + (Fix_Msg (Conc_Typ, "constant & cannot act as constituent of " & "single protected type %"), Indic, Item_Id); return; @@ -3379,7 +3403,7 @@ package body Sem_Prag is else Error_Msg_Name_1 := Chars (Encap_Id); SPARK_Msg_NE - (Fix_Msg (Encap_Typ, "package instantiation & cannot act as " + (Fix_Msg (Conc_Typ, "package instantiation & cannot act as " & "constituent of single protected type %"), Indic, Item_Id); return; end if; @@ -3398,64 +3422,159 @@ package body Sem_Prag is Item_Decl := Declaration_Node (Item_Id); end if; - -- Both the item and its encapsulating single concurrent type must - -- appear in the same declarative region (SPARK RM 9.3). Note that - -- privacy is ignored. + Item_Context := Parent (Item_Decl); + + -- The item and the single concurrent type must appear in the same + -- declarative region, with the item following the declaration of + -- the single concurrent type (SPARK RM 9(3)). + + if Item_Context = Encap_Context then + if Nkind_In (Item_Context, N_Package_Specification, + N_Protected_Definition, + N_Task_Definition) + then + Prv_Decls := Private_Declarations (Item_Context); + Vis_Decls := Visible_Declarations (Item_Context); + + -- The placement is OK when the single concurrent type appears + -- within the visible declarations and the item in the private + -- declarations. + -- + -- package Pack is + -- protected PO ... + -- private + -- Constit : ... with Part_Of => PO; + -- end Pack; + + if List_Containing (Encap_Decl) = Vis_Decls + and then List_Containing (Item_Decl) = Prv_Decls + then + null; + + -- The placement is illegal when the item appears within the + -- visible declarations and the single concurrent type is in + -- the private declarations. + -- + -- package Pack is + -- Constit : ... with Part_Of => PO; + -- private + -- protected PO ... + -- end Pack; + + elsif List_Containing (Item_Decl) = Vis_Decls + and then List_Containing (Encap_Decl) = Prv_Decls + then + Placement_Error; + return; + + -- Otherwise both the item and the single concurrent type are + -- in the same list. Ensure that the declaration of the single + -- concurrent type precedes that of the item. + + elsif not In_Proper_Order + (First => Encap_Decl, + Second => Item_Decl) + then + Placement_Error; + return; + end if; + + -- Otherwise both the item and the single concurrent type are + -- in the same list. Ensure that the declaration of the single + -- concurrent type precedes that of the item. + + elsif not In_Proper_Order + (First => Encap_Decl, + Second => Item_Decl) + then + Placement_Error; + return; + end if; + + -- Otherwise the item and the single concurrent type reside within + -- unrelated regions. - if Parent (Item_Decl) /= Parent (Declaration_Node (Encap_Id)) then + else Error_Msg_Name_1 := Chars (Encap_Id); SPARK_Msg_NE - (Fix_Msg (Encap_Typ, "constituent & must be declared " + (Fix_Msg (Conc_Typ, "constituent & must be declared " & "immediately within the same region as single protected " & "type %"), Indic, Item_Id); return; end if; - -- The declaration of the item should follow the declaration of its - -- encapsulating single concurrent type and must appear in the same - -- declarative region (SPARK RM 9.3). + -- At this point it is known that the Part_Of indicator is legal - declare - N : Node_Id; + Legal := True; + end Check_Part_Of_Concurrent_Type; - begin - N := Next (Declaration_Node (Encap_Id)); - while Present (N) loop - exit when N = Item_Decl; - Next (N); - end loop; + -- Start of processing for Analyze_Part_Of - -- The single concurrent type might be in the visible part of a - -- package, and the declaration of the item in the private part - -- of the same package. + begin + -- Assume that the indicator is illegal - if No (N) then - declare - Pack : constant Node_Id := - Parent (Declaration_Node (Encap_Id)); - begin - if Nkind (Pack) = N_Package_Specification - and then not In_Private_Part (Encap_Id) - then - N := First (Private_Declarations (Pack)); - while Present (N) loop - exit when N = Item_Decl; - Next (N); - end loop; - end if; - end; - end if; + Encap_Id := Empty; + Legal := False; - if No (N) then - SPARK_Msg_N - ("indicator Part_Of must denote a previously declared " - & "single protected type or single task type", Encap); - return; - end if; - end; + if Nkind_In (Encap, N_Expanded_Name, + N_Identifier, + N_Selected_Component) + then + Analyze (Encap); + Resolve_State (Encap); + + Encap_Id := Entity (Encap); + + -- The encapsulator is an abstract state + + if Ekind (Encap_Id) = E_Abstract_State then + null; + + -- The encapsulator is a single concurrent type (SPARK RM 9.3) + + elsif Is_Single_Concurrent_Object (Encap_Id) then + null; + + -- Otherwise the encapsulator is not a legal choice + + else + SPARK_Msg_N + ("indicator Part_Of must denote abstract state, single " + & "protected type or single task type", Encap); + return; + end if; + + -- This is a syntax error, always report + + else + Error_Msg_N + ("indicator Part_Of must denote abstract state, single protected " + & "type or single task type", Encap); + return; end if; - Legal := True; + -- Catch a case where indicator Part_Of denotes the abstract view of a + -- variable which appears as an abstract state (SPARK RM 10.1.2 2). + + if From_Limited_With (Encap_Id) + and then Present (Non_Limited_View (Encap_Id)) + and then Ekind (Non_Limited_View (Encap_Id)) = E_Variable + then + SPARK_Msg_N ("indicator Part_Of must denote abstract state", Encap); + SPARK_Msg_N ("\& denotes abstract view of object", Encap); + return; + end if; + + -- The encapsulator is an abstract state + + if Ekind (Encap_Id) = E_Abstract_State then + Check_Part_Of_Abstract_State; + + -- The encapsulator is a single concurrent type + + else + Check_Part_Of_Concurrent_Type; + end if; end Analyze_Part_Of; ---------------------------------- |