From acd4ef9df257ce400c5eabfa9ab92a1b3196e090 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Fri, 18 Sep 2020 14:45:51 +0200 Subject: [Ada] Fix harmless assertion failure in GNATprove mode gcc/ada/ * inline.adb (Establish_Actual_Mapping_For_Inlined_Call): Add guard for a call to Set_Last_Assignment with the same condition as the assertion in that routine and explain why this guard fails in GNATprove mode. --- gcc/ada/inline.adb | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) (limited to 'gcc/ada/inline.adb') diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index b4d56b6..c24763a 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -2917,7 +2917,24 @@ package body Inline is -- formal in the inlined code. if Is_Entity_Name (A) and then Ekind (F) /= E_In_Parameter then - Set_Last_Assignment (Entity (A), Empty); + + -- In GNATprove mode a protected component acting as an actual + -- subprogram parameter will appear as inlined-for-proof. However, + -- its E_Component entity is not an assignable object, so the + -- assertion in Set_Last_Assignment will fail. We just omit the + -- call to Set_Last_Assignment, because GNATprove flags useless + -- assignments with its own flow analysis. + -- + -- In GNAT mode such a problem does not occur, because protected + -- components are inlined via object renamings whose entity kind + -- E_Variable is assignable. + + if Is_Assignable (Entity (A)) then + Set_Last_Assignment (Entity (A), Empty); + else + pragma Assert + (GNATprove_Mode and then Is_Protected_Component (Entity (A))); + end if; end if; -- If the argument may be a controlling argument in a call within -- cgit v1.1 From 3fcb8100aac71b8a109a4f0ceaabd6cfd650b668 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 16 Nov 2020 12:06:32 +0100 Subject: [Ada] Correctly mark subprogram as not always inlined in GNATprove mode gcc/ada/ * inline.adb (Cannot_Inline): Add No_Info parameter to disable info message. * inline.ads (Cannot_Inline): When No_Info is set to True, do not issue info message in GNATprove mode, but still mark the subprogram as not always inlined. * sem_res.adb (Resolve_Call): Always call Cannot_Inline inside an assertion expression. --- gcc/ada/inline.adb | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) (limited to 'gcc/ada/inline.adb') diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index c24763a..bb4d97c 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1945,10 +1945,11 @@ package body Inline is ------------------- procedure Cannot_Inline - (Msg : String; - N : Node_Id; - Subp : Entity_Id; - Is_Serious : Boolean := False) + (Msg : String; + N : Node_Id; + Subp : Entity_Id; + Is_Serious : Boolean := False; + Suppress_Info : Boolean := False) is begin -- In GNATprove mode, inlining is the technical means by which the @@ -1971,7 +1972,7 @@ package body Inline is New_Msg (1 .. Len2) := "info: no contextual analysis of"; New_Msg (Len2 + 1 .. Msg'Length + Len2 - Len1) := Msg (Msg'First + Len1 .. Msg'Last); - Cannot_Inline (New_Msg, N, Subp, Is_Serious); + Cannot_Inline (New_Msg, N, Subp, Is_Serious, Suppress_Info); return; end; end if; @@ -1992,14 +1993,14 @@ package body Inline is then null; - -- In GNATprove mode, issue a warning when -gnatd_f is set, and - -- indicate that the subprogram is not always inlined by setting - -- flag Is_Inlined_Always to False. + -- In GNATprove mode, issue an info message when -gnatd_f is set and + -- Suppress_Info is False, and indicate that the subprogram is not + -- always inlined by setting flag Is_Inlined_Always to False. elsif GNATprove_Mode then Set_Is_Inlined_Always (Subp, False); - if Debug_Flag_Underscore_F then + if Debug_Flag_Underscore_F and not Suppress_Info then Error_Msg_NE (Msg, N, Subp); end if; @@ -2022,14 +2023,14 @@ package body Inline is Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp); - -- In GNATprove mode, issue a warning when -gnatd_f is set, and - -- indicate that the subprogram is not always inlined by setting - -- flag Is_Inlined_Always to False. + -- In GNATprove mode, issue an info message when -gnatd_f is set and + -- Suppress_Info is False, and indicate that the subprogram is not + -- always inlined by setting flag Is_Inlined_Always to False. elsif GNATprove_Mode then Set_Is_Inlined_Always (Subp, False); - if Debug_Flag_Underscore_F then + if Debug_Flag_Underscore_F and not Suppress_Info then Error_Msg_NE (Msg, N, Subp); end if; -- cgit v1.1