[Ada] Fix failing assertions on SPARK elaboration

Checking of SPARK elaboration rules may lead to assertion failures on a
compiler built with assertions. Now fixed.

There is no impact on compilation.

2019-08-14  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_disp.adb (Check_Dispatching_Operation): Update assertion
	for the separate declarations created in GNATprove mode.
	* sem_disp.ads (Is_Overriding_Subprogram): Update comment.
	* sem_elab.adb (SPARK_Processor): Fix test for checking of
	overriding primitives.

From-SVN: r274448

1 files changed, 7 insertions, 1 deletions

diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb
index 5deba18..ee8f443 100644
--- a/gcc/ada/sem_disp.adb
+++ b/gcc/ada/sem_disp.adb
@@ -1149,6 +1149,10 @@ package body Sem_Disp is
          --     overridden primitives. The wrappers include checks on these
          --     modified conditions. (AI12-113).
 
+         --  5. Declarations built for subprograms without separate spec which
+         --     are eligible for inlining in GNATprove (inside
+         --     Sem_Ch6.Analyze_Subprogram_Body_Helper).
+
          if Present (Old_Subp)
            and then Present (Overridden_Operation (Subp))
            and then Is_Dispatching_Operation (Old_Subp)
@@ -1168,7 +1172,9 @@ package body Sem_Disp is
               or else Get_TSS_Name (Subp) = TSS_Stream_Read
               or else Get_TSS_Name (Subp) = TSS_Stream_Write
 
-              or else Present (Contract (Overridden_Operation (Subp))));
+              or else Present (Contract (Overridden_Operation (Subp)))
+
+              or else GNATprove_Mode);
 
             Check_Controlling_Formals (Tagged_Type, Subp);
             Override_Dispatching_Operation (Tagged_Type, Old_Subp, Subp);