From: Viljar Indus <indus@adacore.com>
Date: Tue, 2 Sep 2025 09:25:07 +0000 (+0300)
Subject: ada: Fix ghost condition for level dependencies for assignments
X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=89b4aa18ca581cdb11f07d60d7ac05a7e556281c;p=thirdparty%2Fgcc.git

ada: Fix ghost condition for level dependencies for assignments

gcc/ada/ChangeLog:

	* ghost.adb (Check_Assignment_Policies): The level of the assignee
	should depend on the level of the region.
---

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 40075bdf0a6..37f82ca849f 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -1913,12 +1913,14 @@ package body Ghost is
               ("\& is modified in a region with `Ignore`", N, Assignee);
          end if;
 
+         --  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 (SPARK RM 6.9(18)).
+
          if Present (Region_Level)
            and then not Is_Assertion_Level_Dependent
-                          (Region_Level, Assignee_Level)
+                          (Assignee_Level, Region_Level)
          then
-            Error_Msg_Sloc := Sloc (N);
-
             Error_Msg_N (Assertion_Level_Error_Msg, N);
             Error_Msg_Name_1 := Chars (Assignee_Level);
             Error_Msg_NE ("\& has assertion level %", N, Assignee);