diff mbox series

[COMMITTED,20/31] ada: Check ghost level dependencies inside assignments

Message ID 20250911091904.1505690-20-poulhies@adacore.com
State Committed
Commit 28b38b266d312e85ceae7f1b605eaa5b6583561d
Headers
Series [COMMITTED,01/31] ada: Disable new warning for composite equality ops that can raise Program_Error |

Commit Message

Marc Poulhiès Sept. 11, 2025, 9:18 a.m. UTC 
  From: Viljar Indus <indus@adacore.com>

Check that entities on the RHS are ghost level dependent on the
entities on the LHS of the assignemnt.

gcc/ada/ChangeLog:

	* ghost.adb (Is_OK_Statement): Check the levels of the
	assignee with the levels of the entity are ghost level dependent.
	(Check_Assignement_Levels): New function for checking the level
	dependencies.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/ghost.adb | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
diff mbox series

Patch

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index bc646b22fbe5..0fbcf20da7c1 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -515,6 +515,10 @@  package body Ghost is
          function Is_OK_Statement
            (Stmt : Node_Id; Id : Entity_Id; Call_Arg : Node_Id) return Boolean
          is
+            procedure Check_Assignment_Levels (Assignee : Entity_Id);
+            --  Check that a ghost entity on the RHS of the assignment is
+            --  assertion level dependent on the LHS.
+
             procedure Check_Procedure_Call_Policies (Callee : Entity_Id);
             --  Check that
             --  * the a checked call argument is not modified by an ignored
@@ -528,6 +532,39 @@  package body Ghost is
             --  Check that Call_Arg was used in the call and that the formal
             --  for that argument was either out or in-out.
 
+            -----------------------------
+            -- Check_Assignment_Levels --
+            -----------------------------
+
+            procedure Check_Assignment_Levels (Assignee : Entity_Id) is
+               Assignee_Level : constant Entity_Id :=
+                 Ghost_Assertion_Level (Assignee);
+               Id_Level       : constant Entity_Id :=
+                 Ghost_Assertion_Level (Id);
+            begin
+               --  SPARK RM 6.9 (13) A ghost entity E shall only be referenced
+               --  within an assignment statement whose target is a ghost
+               --  variable that is assertion-level-dependent on E.
+
+               if not Is_Assertion_Level_Dependent (Id_Level, Assignee_Level)
+               then
+                  Error_Msg_Sloc := Sloc (Ghost_Ref);
+
+                  Error_Msg_N (Assertion_Level_Error_Msg, Ghost_Ref);
+                  Error_Msg_Name_1 := Chars (Id_Level);
+                  Error_Msg_NE ("\& has assertion level %", Ghost_Ref, Id);
+                  Error_Msg_Name_1 := Chars (Assignee_Level);
+                  Error_Msg_Node_2 := Assignee;
+                  Error_Msg_NE
+                    ("\& is modifying & with %", Ghost_Ref, Id);
+                  Error_Msg_Name_1 := Chars (Assignee_Level);
+                  Error_Msg_NE
+                    ("\assertion level of & should depend on %",
+                     Ghost_Ref,
+                     Id);
+               end if;
+            end Check_Assignment_Levels;
+
             -----------------------------------
             -- Check_Procedure_Call_Policies --
             -----------------------------------
@@ -619,6 +656,8 @@  package body Ghost is
 
             if Nkind (Stmt) = N_Assignment_Statement then
                if Is_Ghost_Assignment (Stmt) then
+                  Check_Assignment_Levels
+                    (Get_Enclosing_Ghost_Entity (Name (Stmt)));
                   return True;
                end if;