[Ada] Classwide postconditions on null procedures

Message ID 20130411132810.GA25731@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet April 11, 2013, 1:28 p.m.
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

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
      P1 (It);
   procedure D2 (It : in out O2'class) is
      P2 (It);
   Dispatch (Thing);

   D2 (Thing2);

   D2 (Thing3);

   P2 (Object (Thing));
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;
   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

   function Get_X (This : O2) return Float is begin
      return This.Value;

   procedure P2 (This : in out O2) is

   function Check (This : O2) return Float is
      return This.Value;
end Objects.Child;
package Objects.Child.Grand is

   type O3 is new O2 with private;

   function Check (This : O3) return Float;
   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
      return This.Value + Float (This.Counter);
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.


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 @@ 
+               --  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));
+            --  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;
                --  We need to determine whether the context of the call
                --  provides a tag to make the call dispatching. This requires