===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -43,6 +43,7 @@
with Sem_Ch7; use Sem_Ch7;
with Sem_Ch8; use Sem_Ch8;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Snames; use Snames;
@@ -553,6 +554,28 @@
end;
else
+ -- If the action is the generated body of a null subprogram,
+ -- analyze the expressions in its delayed aspects, because we
+ -- may not have reached the end of the declarative list when
+ -- delayed aspects are normally analyzed. This ensures that
+ -- dispatching calls are properly rewritten when the inner
+ -- postcondition procedure is analyzed.
+
+ if Is_Subprogram (E)
+ and then Nkind (Parent (E)) = N_Procedure_Specification
+ and then Null_Present (Parent (E))
+ then
+ declare
+ Prag : Node_Id;
+ begin
+ Prag := Spec_PPC_List (Contract (E));
+ while Present (Prag) loop
+ Analyze_PPC_In_Decl_Part (Prag, E);
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end;
+ end if;
+
Analyze (Decl, Suppress => All_Checks);
end if;
===================================================================
@@ -536,6 +536,21 @@
Set_Entity (Name (N), Alias (Subp));
return;
+ -- An obscure special case: a null procedure may have a class-
+ -- wide pre/postcondition that includes a call to an abstract
+ -- subp. Calls within the expression may not have been rewritten
+ -- as dispatching calls yet, because the null body appears in
+ -- the current declarative part. The expression will be properly
+ -- rewritten/reanalyzed when the postcondition procedure is built.
+
+ elsif In_Spec_Expression
+ and then Is_Subprogram (Current_Scope)
+ and then
+ Nkind (Parent (Current_Scope)) = N_Procedure_Specification
+ and then Null_Present (Parent (Current_Scope))
+ then
+ null;
+
else
-- We need to determine whether the context of the call
-- provides a tag to make the call dispatching. This requires
This patch allows classwide postconditions on null procedures when the aspect expression includes calls to abstract functions that must be rewrittne as dispatching calls. The following must compile and execute quietly: gnatmake -gnat12 -gnata -q test_class test_class -- with objects; use Objects; with objects.child; use Objects.child; with objects.child.grand; use Objects.child.grand; procedure test_class is Thing : Objects.child.O2; Thing2 : O2; Thing3 : O3; procedure Dispatch (It : in out Object'class) is begin P1 (It); end; procedure D2 (It : in out O2'class) is begin P2 (It); end; begin Dispatch (Thing); D2 (Thing2); D2 (Thing3); P2 (Object (Thing)); end; -- package Objects is type Object is interface; procedure P1 (This : in out Object) is abstract with Post'Class => This.Get_X'Old = This.Get_X; procedure P2 (This : in out Object) is null with Post'Class => This.Get_X'Old = This.Get_X; function Get_X (This : Object) return Float is abstract; end Objects; --- package Objects.Child is type O2 is new object with private; overriding procedure P1 (This : in out O2) ; overriding function Get_X (This : O2) return Float; overriding procedure P2 (This : in out O2) -- is null with Post'class => (this.Check > 1.0); function Check (This : O2) return Float; private type O2 is new Object with record Value : Float := 3.14; end record; end Objects.Child; --- package body Objects.Child is procedure P1 (This : in out O2) is begin null; end; function Get_X (This : O2) return Float is begin return This.Value; end; procedure P2 (This : in out O2) is begin null; end; function Check (This : O2) return Float is begin return This.Value; end; end Objects.Child; --- package Objects.Child.Grand is type O3 is new O2 with private; function Check (This : O3) return Float; private type O3 is new O2 with record Counter : Integer := 123; end record; end Objects.Child.Grand; --- package body Objects.Child.Grand is function Check (This : O3) return Float is begin return This.Value + Float (This.Counter); end; end Objects.Child.Grand; Tested on x86_64-pc-linux-gnu, committed on trunk 2013-04-11 Ed Schonberg <schonberg@adacore.com> * sem_disp.adb (Check_Dispatching_Context): If the context is a contract for a null procedure defer error reporting until postcondition body is created. * exp_ch13.adb (Expand_N_Freeze_Entity): If the entity is a null procedure, complete the analysis of its contracts so that calls within classwide conditions are properly rewritten as dispatching calls.