Commit bab15911 by Yannick Moy Committed by Pierre-Marie de Rodat

[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
parent 4a6db9fd
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.
2019-08-14 Eric Botcazou <ebotcazou@adacore.com> 2019-08-14 Eric Botcazou <ebotcazou@adacore.com>
* inline.adb (Add_Inlined_Body): Tweak comments. * inline.adb (Add_Inlined_Body): Tweak comments.
......
...@@ -1149,6 +1149,10 @@ package body Sem_Disp is ...@@ -1149,6 +1149,10 @@ package body Sem_Disp is
-- overridden primitives. The wrappers include checks on these -- overridden primitives. The wrappers include checks on these
-- modified conditions. (AI12-113). -- 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) if Present (Old_Subp)
and then Present (Overridden_Operation (Subp)) and then Present (Overridden_Operation (Subp))
and then Is_Dispatching_Operation (Old_Subp) and then Is_Dispatching_Operation (Old_Subp)
...@@ -1168,7 +1172,9 @@ package body Sem_Disp is ...@@ -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_Read
or else Get_TSS_Name (Subp) = TSS_Stream_Write 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); Check_Controlling_Formals (Tagged_Type, Subp);
Override_Dispatching_Operation (Tagged_Type, Old_Subp, Subp); Override_Dispatching_Operation (Tagged_Type, Old_Subp, Subp);
......
...@@ -151,7 +151,8 @@ package Sem_Disp is ...@@ -151,7 +151,8 @@ package Sem_Disp is
-- Returns True if E is a null procedure that is an interface primitive -- Returns True if E is a null procedure that is an interface primitive
function Is_Overriding_Subprogram (E : Entity_Id) return Boolean; 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; function Is_Tag_Indeterminate (N : Node_Id) return Boolean;
-- Returns true if the expression N is tag-indeterminate. An expression -- Returns true if the expression N is tag-indeterminate. An expression
......
...@@ -49,6 +49,7 @@ with Sem_Aux; use Sem_Aux; ...@@ -49,6 +49,7 @@ with Sem_Aux; use Sem_Aux;
with Sem_Cat; use Sem_Cat; with Sem_Cat; use Sem_Cat;
with Sem_Ch7; use Sem_Ch7; with Sem_Ch7; use Sem_Ch7;
with Sem_Ch8; use Sem_Ch8; with Sem_Ch8; use Sem_Ch8;
with Sem_Disp; use Sem_Disp;
with Sem_Prag; use Sem_Prag; with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util; with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo; with Sinfo; use Sinfo;
...@@ -15233,9 +15234,12 @@ package body Sem_Elab is ...@@ -15233,9 +15234,12 @@ package body Sem_Elab is
begin begin
-- Nothing to do for predefined primitives because they are -- Nothing to do for predefined primitives because they are
-- artifacts of tagged type expansion and cannot override source -- 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; return;
end if; end if;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment