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 37f82ca849f7f3b3a31a69acf6a08c0207fa109c..e7a55efb4beb858047543ce6bc47d4c7209ab2de 100644 (file)
--- 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;