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 --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 5604bfec92ae691c3f9de318863390e1e2ee3638..58d320006eb1af0f137549d1a6de93ca7ef64e7a 100644 (file)
--- 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 87401c16a66cfea50cf3da0391a12a2b0c10179c..1cecaa7855f4d2a911cf9d7821b379e2d1a4f5d4 100644 (file)
--- 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 0465975c2c4c51381595a23de903ae5fafc0d1e5..53c292742815084457ef7634b392b57938910f5a 100644 (file)
--- 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;
 
    ------------------------------