[Ada] Class-wide pre/postconditions

[Ada] Class-wide pre/postconditions

[Arnaud Charlet]

[-- Attachment #1: Type: text/plain, Size: 2434 bytes --]

Class-wide pre- and postconditions of a primitive operation of some type T
apply to the overriding operation of any descendant of T. Therefore, any
mention of of a formal of type T in the expression for the condition must be
interpreted as a being of type  T'class. A similar rule applies to access
paremeters. This patch adds the required type conversion to such references.
The following must execute quietly:

    gnatmake -q -gnatws -gnat12 -gnata r
    r
--
with System.Assertions; use System.Assertions;
with P1.Q1;
procedure R is
   Thing1 : P1.T1;
   Thing2 : P1.Q1.T2;
   Thing3 : aliased P1.Q1.T2;

begin
 P1.P (Thing1);

   begin
     P1.Q1.P (Thing2);
     raise Program_Error;   --  should not reach here
   exception
     when Assert_Failure  => null;
   end;

   --  Test access parameters.

   begin
     P1.Q1.P2 (Thing3'access);
     raise Program_Error;   --  should not reach here
   exception
     when Assert_Failure  => null;
   end;
end R;
---
package P1 is
  type T1 is tagged record
     Value : Integer := 16;
  end record;

  procedure P(X : in out T1) with
    Pre'Class => Precond(X'Old),
    Post'Class => Postcond(X);

  procedure P2 (X : access T1)
  with
    Post'Class => X.all.Value > 0;
  
  function Precond(X : T1) return Boolean;
  function Postcond(X : T1) return Boolean;
end P1;
---
package body P1 is

  procedure P(X : in out T1)  is begin null; end;

  procedure P2 (X : access T1) is
  begin
    X.Value := X.Value + 3;
 end P2;

  function Precond(X : T1) return Boolean is begin return True; end;
  function Postcond(X : T1) return Boolean is begin return X.Value < 20; end;
end P1;
---
package P1.Q1 is
  type T2 is new T1 with null record;

  overriding
    procedure P(X : in out T2);

  overriding
    procedure P2 (X : access T2);
end P1.Q1;
---
package body P1.Q1 is

 --  Overriding procedures that violate inherited postcondition.

 procedure P (X : in out T2) is begin X.Value := 25; end;

 procedure P2 (X : access T2) is
  begin
    X.Value := -X.Value + 3;
 end P2;
end P1.Q1;

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-09-02  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb (Analyze_PPC_In_Decl_Part): for a class-wide
	condition, a reference to a controlling formal must be interpreted
	as having the class-wide type (or an access to such) so that the
	inherited condition can be properly applied to any overriding
	operation (see ARM12 6.6.1 (7)).


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 4570 bytes --]

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 178381)
+++ sem_prag.adb	(working copy)
@@ -39,6 +39,7 @@
 with Errout;   use Errout;
 with Exp_Dist; use Exp_Dist;
 with Exp_Util; use Exp_Util;
+with Freeze;   use Freeze;
 with Lib;      use Lib;
 with Lib.Writ; use Lib.Writ;
 with Lib.Xref; use Lib.Xref;
@@ -261,6 +262,99 @@
       Preanalyze_Spec_Expression
         (Get_Pragma_Arg (Arg1), Standard_Boolean);
 
+      if Class_Present (N) then
+         declare
+            T   : constant Entity_Id := Find_Dispatching_Type (S);
+
+            ACW : Entity_Id := Empty;
+            --  Access to T'class, created if there is a controlling formal
+            --  that is an access parameter.
+
+            function Get_ACW return Entity_Id;
+            --  If the expression has a reference to an controlling access
+            --  parameter, create an access to T'class for the necessary
+            --  conversions if one does not exist.
+
+            function Process (N : Node_Id) return Traverse_Result;
+            --  ARM 6.1.1: Within the expression for a Pre'Class or Post'Class
+            --  aspect for a primitive subprogram of a tagged type T, a name
+            --  that denotes a formal parameter of type T is interpreted as
+            --  having type T'Class. Similarly, a name that denotes a formal
+            --  accessparameter of type access-to-T is interpreted as having
+            --  type access-to-T'Class. This ensures the expression is well-
+            --  defined for a primitive subprogram of a type descended from T.
+
+            -------------
+            -- Get_ACW --
+            -------------
+
+            function Get_ACW return Entity_Id is
+               Loc  : constant Source_Ptr := Sloc (N);
+               Decl : Node_Id;
+
+            begin
+               if No (ACW) then
+                  Decl := Make_Full_Type_Declaration (Loc,
+                    Defining_Identifier => Make_Temporary (Loc, 'T'),
+                    Type_Definition =>
+                       Make_Access_To_Object_Definition (Loc,
+                       Subtype_Indication =>
+                         New_Occurrence_Of (Class_Wide_Type (T), Loc),
+                       All_Present => True));
+
+                  Insert_Before (Unit_Declaration_Node (S), Decl);
+                  Analyze (Decl);
+                  ACW := Defining_Identifier (Decl);
+                  Freeze_Before (Unit_Declaration_Node (S), ACW);
+               end if;
+
+               return ACW;
+            end Get_ACW;
+
+            -------------
+            -- Process --
+            -------------
+
+            function Process (N : Node_Id) return Traverse_Result is
+               Loc : constant Source_Ptr := Sloc (N);
+               Typ : Entity_Id;
+
+            begin
+               if Is_Entity_Name (N)
+                 and then Is_Formal (Entity (N))
+                 and then Nkind (Parent (N)) /= N_Type_Conversion
+               then
+                  if Etype (Entity (N)) = T then
+                     Typ := Class_Wide_Type (T);
+
+                  elsif Is_Access_Type (Etype (Entity (N)))
+                    and then Designated_Type (Etype (Entity (N))) = T
+                  then
+                     Typ := Get_ACW;
+                  else
+                     Typ := Empty;
+                  end if;
+
+                  if Present (Typ) then
+                     Rewrite (N,
+                       Make_Type_Conversion (Loc,
+                         Subtype_Mark =>
+                           New_Occurrence_Of (Typ, Loc),
+                         Expression  => New_Occurrence_Of (Entity (N), Loc)));
+                     Set_Etype (N, Typ);
+                  end if;
+               end if;
+
+               return OK;
+            end Process;
+
+            procedure Replace_Type is new Traverse_Proc (Process);
+
+         begin
+            Replace_Type (Get_Pragma_Arg (Arg1));
+         end;
+      end if;
+
       --  Remove the subprogram from the scope stack now that the pre-analysis
       --  of the precondition/postcondition is done.
 
@@ -1838,6 +1932,12 @@
                   Chain_PPC (PO);
                   return;
 
+               elsif Nkind (PO) = N_Subprogram_Declaration
+                 and then In_Instance
+               then
+                  Chain_PPC (PO);
+                  return;
+
                --  For all other cases of non source code, do nothing
 
                else