From bab15911661814606d18639ef53597ea9a843afa Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 14 Aug 2019 09:50:55 +0000 Subject: [PATCH] [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 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 --- gcc/ada/ChangeLog | 8 ++++++++ gcc/ada/sem_disp.adb | 8 +++++++- gcc/ada/sem_disp.ads | 3 ++- gcc/ada/sem_elab.adb | 8 ++++++-- 4 files changed, 23 insertions(+), 4 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ff7de27c00e..b8f85c45998 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,11 @@ +2019-08-14 Yannick Moy + + * 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. + 2019-08-14 Eric Botcazou * inline.adb (Add_Inlined_Body): Tweak comments. diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb index 5deba186e41..ee8f4431da9 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); diff --git a/gcc/ada/sem_disp.ads b/gcc/ada/sem_disp.ads index c3f4586447e..fd399a31972 100644 --- a/gcc/ada/sem_disp.ads +++ b/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 diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index 31455592d51..714a9f7221f 100644 --- a/gcc/ada/sem_elab.adb +++ b/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 begin -- 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 return; end if; -- 2.30.2