From 758daef51b03aeda7afd338fc1954d0c012a4a98 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 16 Nov 2020 21:50:17 +0100 Subject: [PATCH] [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. --- gcc/ada/sem_prag.adb | 99 ++++++++++++++++++++++++++++++++++---------- 1 file changed, 76 insertions(+), 23 deletions(-) diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index fe22510baf5..8c0ce796db4 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -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; -----------------------------