From: Viljar Indus <[email protected]>
The assignee should depend on the level of all of the ghost entiies
with the assignment.
gcc/ada/ChangeLog:
* ghost.adb (Check_Assignee_Levels): Fix the condition and improve
error message handling.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/ghost.adb | 13 +++++--------
1 file changed, 5 insertions(+), 8 deletions(-)
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index bfe6bff0751e..ef6315a7d3d5 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -561,22 +561,19 @@ package body Ghost is
-- 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)
+ if not Is_Assertion_Level_Dependent (Assignee_Level, Id_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_N ("\& has assertion level %", Ghost_Ref);
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 ("\& is modifying & with %", Ghost_Ref, Id);
+ Error_Msg_Name_1 := Chars (Id_Level);
Error_Msg_NE
("\assertion level of & should depend on %",
Ghost_Ref,
- Id);
+ Assignee);
end if;
end Check_Assignment_Levels;
--
2.43.0