From: Viljar Indus <[email protected]>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
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 5604bfec92a..58d320006eb 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 87401c16a66..1cecaa7855f 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 0465975c2c4..53c29274281 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;
------------------------------
--
2.51.0
