From: Viljar Indus <in...@adacore.com>
gcc/ada/ChangeLog:
* ghost.adb (Check_Assignment_Policies): The level of the assignee
should depend on the level of the region.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/ghost.adb | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 40075bdf0a6b..37f82ca849f7 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);
--
2.43.0
