From: Viljar Indus <[email protected]>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
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 37f82ca849f7..e7a55efb4beb 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_N ("\& has assertion level %", Ghost_Ref);
Error_Msg_Name_1 := Chars (Call_Level);
- Error_Msg_NE
- ("\& is modified # by a procedure with %", Ghost_Ref, Id);
- 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.43.0
