From: Viljar Indus <indus@adacore.com>
Date: Tue, 9 Sep 2025 12:00:56 +0000 (+0300)
Subject: ada: Update the condition for ghost call arguments
X-Git-Url: http://git.ipfire.org/gitweb.cgi?a=commitdiff_plain;h=840899585a23ae346235035aca4842b3d1358180;p=thirdparty%2Fgcc.git

ada: Update the condition for ghost call arguments

The SPARK RM specifies that the levels between the argument and
the call shall have the same level.

gcc/ada/ChangeLog:

	* ghost.adb (Check_Procedure_Call_Policies): Update the check
	between the levels of the argument and the call.
---

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 37f82ca849f..e7a55efb4be 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -578,20 +578,20 @@ package body Ghost is
                      Id);
                end if;
 
-               if not Is_Assertion_Level_Dependent (Id_Level, Call_Level) then
-                  Error_Msg_Sloc := Sloc (Ghost_Ref);
+               --  An out or in out mode actual parameter and the subprogram
+               --  shall have matching assertion levels SPARK RM 6.9 (15).
 
+               if Id_Level /= Call_Level then
                   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 (Call_Level);
-                  Error_Msg_NE
-                    ("\& is modified # by a procedure with %", Ghost_Ref, Id);
+                  Error_Msg_N ("\& has assertion level %", Ghost_Ref);
                   Error_Msg_Name_1 := Chars (Call_Level);
-                  Error_Msg_NE
-                    ("\assertion level of & should depend on %",
-                     Ghost_Ref,
-                     Id);
+                  Error_Msg_Node_2 := Callee;
+                  Error_Msg_N
+                    ("\& is modified by & with %", Ghost_Ref);
+                  Error_Msg_N
+                    ("\the levels of the call and call arguments must match",
+                     Ghost_Ref);
                end if;
             end Check_Procedure_Call_Policies;