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 <[email protected]>
* 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.
Index: exp_ch13.adb
===================================================================
--- exp_ch13.adb (revision 197743)
+++ exp_ch13.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2012, Free Software Foundation, Inc. --
+-- 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;
Index: sem_disp.adb
===================================================================
--- sem_disp.adb (revision 197786)
+++ sem_disp.adb (working copy)
@@ -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
