===================================================================
@@ -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
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)).