RM 3.2.4 (23/3) stipulates that predicates are checked on out and in-out
by-reference parameters on return from a call. If the call is to a primitive
of the type the predicate call is inserted in the postcondition subprogram.
However, if the call is to an inherited operation, the check must be performed
explicitly on exit from the call.
Executing the following:
gnatmake -q -gnata -gnat12 main.adb
main
---
must yield:
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : predicate failed at main.adb:6
---
with Derived; use Derived;
procedure Main is
A : T0 := (X => 0);
B : T0 := (X => A.X);
begin
P (A);
B := A;
end Main;
---
with Parent; use Parent;
package Derived is
type T0 is new T with null record with Dynamic_Predicate => T0.X = 0;
procedure Change (x : in out T0);
end Derived;
---
package Parent is
type T is tagged record
X : Integer;
end record;
procedure P (A : in out T);
end Parent;
---
package body Parent is
procedure P (A : in out T) is
begin
A.X := 1;
end P;
end Parent;
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-04-22 Ed Schonberg <schonb...@adacore.com>
* exp_ch6.adb (Expand_Actuals): If the call is to an
inherited operation and the actual is a by-reference type with
predicates, add predicate call to post-call actions.
* sem_util.adb (Is_Inherited_Operation_For_Type): Fix coding
error: a type declaration has a defining identifier, not an Etype.
* sem_res.adb: Restore code removed because of above error.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 198126)
+++ sem_util.adb (working copy)
@@ -8462,8 +8462,11 @@
Typ : Entity_Id) return Boolean
is
begin
+ -- Check that the operation has been created by the declaration for
+ -- the type.
+
return Is_Inherited_Operation (E)
- and then Etype (Parent (E)) = Typ;
+ and then Defining_Identifier (Parent (E)) = Typ;
end Is_Inherited_Operation_For_Type;
-----------------
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 198126)
+++ sem_res.adb (working copy)
@@ -5896,20 +5896,15 @@
-- In formal mode, the primitive operations of a tagged type or type
-- extension do not include functions that return the tagged type.
- -- Commented out as the call to Is_Inherited_Operation_For_Type may
- -- cause an error because the type entity of the parent node of
- -- Entity (Name (N) may not be set. ???
- -- So why not just add a guard ???
+ if Nkind (N) = N_Function_Call
+ and then Is_Tagged_Type (Etype (N))
+ and then Is_Entity_Name (Name (N))
+ and then Is_Inherited_Operation_For_Type
+ (Entity (Name (N)), Etype (N))
+ then
+ Check_SPARK_Restriction ("function not inherited", N);
+ end if;
--- if Nkind (N) = N_Function_Call
--- and then Is_Tagged_Type (Etype (N))
--- and then Is_Entity_Name (Name (N))
--- and then Is_Inherited_Operation_For_Type
--- (Entity (Name (N)), Etype (N))
--- then
--- Check_SPARK_Restriction ("function not inherited", N);
--- end if;
-
-- Implement rule in 12.5.1 (23.3/2): In an instance, if the actual is
-- class-wide and the call dispatches on result in a context that does
-- not provide a tag, the call raises Program_Error.
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb (revision 198126)
+++ exp_ch6.adb (working copy)
@@ -942,6 +942,7 @@
Formal : Entity_Id;
N_Node : Node_Id;
Post_Call : List_Id;
+ E_Actual : Entity_Id;
E_Formal : Entity_Id;
procedure Add_Call_By_Copy_Code;
@@ -1508,6 +1509,7 @@
Actual := First_Actual (N);
while Present (Formal) loop
E_Formal := Etype (Formal);
+ E_Actual := Etype (Actual);
if Is_Scalar_Type (E_Formal)
or else Nkind (Actual) = N_Slice
@@ -1645,7 +1647,7 @@
-- conversion" errors.
elsif Is_Access_Type (E_Formal)
- and then not Same_Type (E_Formal, Etype (Actual))
+ and then not Same_Type (E_Formal, E_Actual)
and then not Is_Tagged_Type (Designated_Type (E_Formal))
then
Add_Call_By_Copy_Code;
@@ -1661,7 +1663,7 @@
elsif Is_Entity_Name (Actual)
and then Is_Volatile (Entity (Actual))
- and then not Is_By_Reference_Type (Etype (Actual))
+ and then not Is_By_Reference_Type (E_Actual)
and then not Is_Scalar_Type (Etype (Entity (Actual)))
and then not Is_Volatile (E_Formal)
then
@@ -1682,10 +1684,10 @@
elsif Is_Scalar_Type (E_Formal)
and then
- (not In_Subrange_Of (E_Formal, Etype (Actual))
+ (not In_Subrange_Of (E_Formal, E_Actual)
or else
(Ekind (Formal) = E_In_Out_Parameter
- and then not In_Subrange_Of (Etype (Actual), E_Formal)))
+ and then not In_Subrange_Of (E_Actual, E_Formal)))
then
-- Perhaps the setting back to False should be done within
-- Add_Call_By_Copy_Code, since it could get set on other
@@ -1698,6 +1700,28 @@
Add_Call_By_Copy_Code;
end if;
+ -- RM 3.2.4 (23/3) : A predicate is checked on in-out and out
+ -- by-reference parameters on exit from the call. If the actual
+ -- is a derived type and the operation is inherited, the body
+ -- of the operation will not contain a call to the predicate
+ -- function, so it must be done explicitly after the call. Ditto
+ -- if the actual is an entity of a predicated subtype.
+
+ if Is_By_Reference_Type (E_Formal)
+ and then Has_Predicates (E_Actual)
+ then
+ if Is_Derived_Type (E_Actual)
+ and then Is_Inherited_Operation_For_Type (Subp, E_Actual)
+ then
+ Append_To
+ (Post_Call, Make_Predicate_Check (E_Actual, Actual));
+
+ elsif Is_Entity_Name (Actual) then
+ Append_To
+ (Post_Call, Make_Predicate_Check (E_Actual, Actual));
+ end if;
+ end if;
+
-- Processing for IN parameters
else
