]> git.ipfire.org Git - thirdparty/gcc.git/commitdiff
ada: Fix the condition of ghost level dependencies inside assignments
authorViljar Indus <indus@adacore.com>
Mon, 1 Sep 2025 08:00:38 +0000 (11:00 +0300)
committerMarc Poulhiès <dkm@gcc.gnu.org>
Mon, 15 Sep 2025 12:59:30 +0000 (14:59 +0200)
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.

gcc/ada/ghost.adb

index bfe6bff0751eecd97a2c22707158238fcb9c6cb9..ef6315a7d3d5ce4c0ce58b3f52c172dde6c43440 100644 (file)
@@ -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;