From e3f9dc2795eccfae4bf878ff6b29d50ff5139011 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 20 Jun 2023 15:30:35 +0200 Subject: ada: Fix list of inherited subprograms in query for GNATprove The query Inherited_Subprograms was returning a list containing some subprograms whose overridding was also in the list, when interfaces was present. This was an issue for GNATprove. Now propose a mode for this function to filter out overridden primitives. gcc/ada/ * sem_disp.adb (Inherited_Subprograms): Add parameter to filter out results. * sem_disp.ads: Likewise. --- gcc/ada/sem_disp.adb | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) (limited to 'gcc/ada/sem_disp.adb') diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb index 6c8212c..b22407aa 100644 --- a/gcc/ada/sem_disp.adb +++ b/gcc/ada/sem_disp.adb @@ -2530,6 +2530,7 @@ package body Sem_Disp is (S : Entity_Id; No_Interfaces : Boolean := False; Interfaces_Only : Boolean := False; + Skip_Overridden : Boolean := False; One_Only : Boolean := False) return Subprogram_List is Result : Subprogram_List (1 .. 6000); @@ -2670,6 +2671,34 @@ package body Sem_Disp is end if; end if; + -- Do not keep an overridden operation if its overridding operation + -- is in the results too, and it is not S. This can happen for + -- inheritance between interfaces. + + if Skip_Overridden then + declare + Res : constant Subprogram_List (1 .. N) := Result (1 .. N); + M : Nat := 0; + begin + for J in 1 .. N loop + for K in 1 .. N loop + if Res (K) /= S + and then Res (J) = Overridden_Operation (Res (K)) + then + goto Skip; + end if; + end loop; + + M := M + 1; + Result (M) := Res (J); + + <> + end loop; + + N := M; + end; + end if; + <> return Result (1 .. N); @@ -2702,6 +2731,7 @@ package body Sem_Disp is (S : Entity_Id; No_Interfaces : Boolean := False; Interfaces_Only : Boolean := False; + Skip_Overridden : Boolean := False; One_Only : Boolean := False) return Subprogram_List renames Inheritance_Utilities_Inst.Inherited_Subprograms; -- cgit v1.1