https://gcc.gnu.org/g:b666b1c3f27c3d8751d5d902389fa05d7ea4a8d2
commit r16-5383-gb666b1c3f27c3d8751d5d902389fa05d7ea4a8d2 Author: Viljar Indus <[email protected]> Date: Wed Sep 10 12:47:19 2025 +0300 ada: Add rule check for call arguments Implement SPARK RM 6.9(18). If an assignment to a part of a ghost variable occurs in a ghost entity, then the variable should be assertion-level-dependent on this entity. [This includes both assignment statements and passing a ghost variable as an out or in out mode actual parameter.] gcc/ada/ChangeLog: * ghost.adb (Check_Procedure_Call_Levels): New function for implementing the check. * ghost.ads (Check_Procedure_Call_Levels): Likewise. * sem_ch6.adb (Analyze_Procedure_Call): Check the levels after the call has been resolved and the previous ghost region has been restored. Diff: --- gcc/ada/ghost.adb | 102 ++++++++++++++++++++++++++++++++++++++++++++++++++++ gcc/ada/ghost.ads | 5 +++ gcc/ada/sem_ch6.adb | 1 + 3 files changed, 108 insertions(+) diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 5604bfec92ae..58d320006eb1 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -2264,6 +2264,108 @@ package body Ghost is Check_Ghost_Actuals; end Mark_And_Set_Ghost_Instantiation; + ------------------------------------------ + -- Check_Procedure_Call_Argument_Levels -- + ------------------------------------------ + + procedure Check_Procedure_Call_Argument_Levels (N : Node_Id) is + procedure Check_Argument_Levels + (Actual : Entity_Id; Actual_Ref : Node_Id); + -- Check that the ghost assertion level of an actual is an assertion + -- level which depends on the ghost region where the procedure call + -- is located. + + --------------------------- + -- Check_Argument_Levels -- + --------------------------- + + procedure Check_Argument_Levels + (Actual : Entity_Id; Actual_Ref : Node_Id) + is + Actual_Level : constant Entity_Id := Ghost_Assertion_Level (Actual); + Region_Level : constant Entity_Id := + Ghost_Config.Ghost_Mode_Assertion_Level; + begin + -- If an assignment to a part of a ghost variable occurs in a ghost + -- entity, then the variable should be assertion-level-dependent on + -- this entity [This includes both assignment statements and passing + -- a ghost variable as an out or in out mode actual parameter.] + -- (SPARK RM 6.9(18)). + + if Present (Region_Level) + and then not Is_Assertion_Level_Dependent + (Actual_Level, Region_Level) + then + Error_Msg_N (Assertion_Level_Error_Msg, Actual_Ref); + Error_Msg_Name_1 := Chars (Actual_Level); + Error_Msg_N ("\& has assertion level %", Actual_Ref); + Error_Msg_Name_1 := Chars (Region_Level); + Error_Msg_N ("\& is modified within a region with %", Actual_Ref); + Error_Msg_Name_1 := Chars (Region_Level); + Error_Msg_N + ("\assertion level of & should depend on %", Actual_Ref); + end if; + end Check_Argument_Levels; + + -- Local variables + + Actual : Node_Id; + Actual_Id : Entity_Id; + Formal : Node_Id; + Id : Entity_Id; + Orig_Actual : Node_Id; + + -- Start of processing for Check_Procedure_Call_Argument_Levels + + begin + if Nkind (N) not in N_Procedure_Call_Statement then + return; + end if; + + -- Handle the access-to-subprogram case + + if Ekind (Etype (Name (N))) = E_Subprogram_Type then + Id := Etype (Name (N)); + else + Id := Get_Enclosing_Ghost_Entity (Name (N)); + end if; + + -- Check for context if we are able to derive the called subprogram and + -- we are not dealing with an expanded construct. + + if Present (Id) + and then Comes_From_Source (N) + and then Ghost_Config.Ghost_Mode /= None + then + Orig_Actual := First_Actual (N); + Formal := First_Formal (Id); + + while Present (Orig_Actual) loop + -- Similarly to Mark_And_Set_Ghost_Procedure_Call we need to + -- analyze the call argument first to get its level for this + -- analysis. + + Actual := + (if Analyzed (Orig_Actual) + then Orig_Actual + else New_Copy_Tree (Orig_Actual)); + if not Analyzed (Actual) then + Preanalyze_Without_Errors (Actual); + end if; + + if Ekind (Formal) in E_Out_Parameter | E_In_Out_Parameter then + Actual_Id := Get_Enclosing_Ghost_Entity (Actual); + if Present (Actual_Id) then + Check_Argument_Levels (Actual_Id, Orig_Actual); + end if; + end if; + + Next_Formal (Formal); + Next_Actual (Orig_Actual); + end loop; + end if; + end Check_Procedure_Call_Argument_Levels; + --------------------------------------- -- Mark_And_Set_Ghost_Procedure_Call -- --------------------------------------- diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 87401c16a66c..1cecaa7855f4 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -221,6 +221,11 @@ package Ghost is -- Install the Ghost mode of the instantiation. This routine starts a Ghost -- region and must be used with routine Restore_Ghost_Region. + procedure Check_Procedure_Call_Argument_Levels (N : Node_Id); + -- Check that the variable being modified by a call argument inside a ghost + -- region is assertion-level-dependent on the ghost region (SPARK RM + -- 6.9(18)). + procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id); -- Mark procedure call N as Ghost when: -- diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 0465975c2c4c..53c292742815 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1899,6 +1899,7 @@ package body Sem_Ch6 is <<Leave>> Restore_Ghost_Region (Saved_Ghost_Config); + Check_Procedure_Call_Argument_Levels (N); end Analyze_Procedure_Call; ------------------------------
