From 840899585a23ae346235035aca4842b3d1358180 Mon Sep 17 00:00:00 2001 From: Viljar Indus Date: Tue, 9 Sep 2025 15:00:56 +0300 Subject: [PATCH] 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. --- gcc/ada/ghost.adb | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) 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; -- 2.47.3