From acd4ef9df257ce400c5eabfa9ab92a1b3196e090 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Fri, 18 Sep 2020 14:45:51 +0200 Subject: [PATCH] [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(-) diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index b4d56b620a6..c24763abedc 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 -- 2.30.2