[Ada] Fix failing assertions on SPARK elaboration
diff mbox series

Message ID 20190814095311.GA51899@adacore.com
State New
Headers show
  • [Ada] Fix failing assertions on SPARK elaboration
Related show

Commit Message

Pierre-Marie de Rodat Aug. 14, 2019, 9:53 a.m. UTC
Checking of SPARK elaboration rules may lead to assertion failures on a
compiler built with assertions. Now fixed.

There is no impact on compilation.

Tested on x86_64-pc-linux-gnu, committed on trunk

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


	* 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.

diff mbox series

--- gcc/ada/sem_disp.adb
+++ 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);

--- gcc/ada/sem_disp.ads
+++ gcc/ada/sem_disp.ads
@@ -151,7 +151,8 @@  package Sem_Disp is
    --  Returns True if E is a null procedure that is an interface primitive
    function Is_Overriding_Subprogram (E : Entity_Id) return Boolean;
-   --  Returns True if E is an overriding subprogram
+   --  Returns True if E is an overriding subprogram and False otherwise, in
+   --  particular for an inherited subprogram.
    function Is_Tag_Indeterminate (N : Node_Id) return Boolean;
    --  Returns true if the expression N is tag-indeterminate. An expression

--- gcc/ada/sem_elab.adb
+++ gcc/ada/sem_elab.adb
@@ -49,6 +49,7 @@  with Sem_Aux;  use Sem_Aux;
 with Sem_Cat;  use Sem_Cat;
 with Sem_Ch7;  use Sem_Ch7;
 with Sem_Ch8;  use Sem_Ch8;
+with Sem_Disp; use Sem_Disp;
 with Sem_Prag; use Sem_Prag;
 with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
@@ -15233,9 +15234,12 @@  package body Sem_Elab is
             --  Nothing to do for predefined primitives because they are
             --  artifacts of tagged type expansion and cannot override source
-            --  primitives.
+            --  primitives. Nothing to do as well for inherited primitives as
+            --  the check concerns overridding ones.
-            if Is_Predefined_Dispatching_Operation (Prim) then
+            if Is_Predefined_Dispatching_Operation (Prim)
+              or else not Is_Overriding_Subprogram (Prim)
+            then
             end if;