This patch complete the generation of invariant checks, for the case of
return values or in-out parameters that involve access types whose designated
type has invariants.
Executing:
gnatmake -q -gnat12 -gnata main
main
must yield:
1
TEST 0
1
TEST 1
2
TEST 2
2
TEST 3
TEST 4
3
4
TEST 5
3
4
END
---
with P; use P;
with Ada.Text_IO; use Ada.Text_IO;
procedure Main is
O : T; -- value = 1
V : T_Access := new T; -- value = 2
W : aliased X;
begin
W.V1 := new T; -- value = 3
W.V2 := new T; -- value = 4
Put_Line ("TEST 0");
Test_0 (O);
Put_Line ("TEST 1");
Test_1 (V);
Put_Line ("TEST 2");
Test_2 (V);
Put_Line ("TEST 3");
Test_3 (W);
Put_Line ("TEST 4");
Test_4 (W);
Put_Line ("TEST 5");
Test_5 (W'Access);
Put_Line ("END");
end Main;
---
package P is
type T is private
with Type_Invariant => Check (T);
type T_Access is access all T;
type X is record
V1 : access T;
V2 : T_Access;
end record;
function Make (X : integer) return T;
function Make (X : integer) return access T;
procedure Test_0 (Obj : in out T);
function Check (O : T) return Boolean;
procedure Test_1 (V : access T);
procedure Test_2 (V : T_Access);
procedure Test_3 (V : X);
procedure Test_4 (V : in out X);
procedure Test_5 (V : access X);
private
Counter : Integer := 0;
function Incr return Integer;
type T is record
Value : Integer := Incr;
end record;
end P;
---
with Ada.Text_IO; use Ada.Text_IO;
package body P is
function Incr return Integer is
begin
Counter := Counter + 1;
return Counter;
end;
Root : aliased T := (others => 15);
function Check (O : T) return Boolean is
begin
Put_Line (Integer'Image (O.Value));
return True;
end Check;
function Make (X : Integer) return T is
begin
return (Value => X);
end;
function Make (X : Integer) return access T is
begin
return Root'access;
end;
procedure Test_0 (Obj : in out T) is
begin
null;
end;
procedure Test_1 (V : access T) is
begin
null;
end Test_1;
procedure Test_2 (V : T_Access) is
begin
null;
end Test_2;
procedure Test_3 (V : X) is
begin
null;
end Test_3;
procedure Test_4 (V : in out X) is
begin
null;
end Test_4;
procedure Test_5 (V : access X) is
begin
null;
end Test_5;
end P;
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-10-02 Ed Schonberg <schonb...@adacore.com>
* sem_ch6.adb (Process_PPCs): Generate invariant checks for a
return value whose type is an access type and whose designated
type has invariants. Ditto for in-out parameters and in-parameters
of an access type.
* exp_ch3.adb (Build_Component_Invariant_Call): Add invariant check
for an access component whose designated type has invariants.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 191911)
+++ sem_ch6.adb (working copy)
@@ -11078,6 +11078,12 @@
Plist : List_Id := No_List;
-- List of generated postconditions
+ procedure Check_Access_Invariants (E : Entity_Id);
+ -- If the subprogram returns an access to a type with invariants, or
+ -- has access parameters whose designated type has an invariant, then
+ -- under the same visibility conditions as for other invariant checks,
+ -- the type invariant must be applied to the returned value.
+
function Grab_CC return Node_Id;
-- Prag contains an analyzed contract case pragma. This function copies
-- relevant components of the pragma, creates the corresponding Check
@@ -11108,6 +11114,43 @@
-- that an invariant check is required (for an IN OUT parameter, or
-- the returned value of a function.
+ -----------------------------
+ -- Check_Access_Invariants --
+ -----------------------------
+
+ procedure Check_Access_Invariants (E : Entity_Id) is
+ Call : Node_Id;
+ Obj : Node_Id;
+ Typ : Entity_Id;
+
+ begin
+ if Is_Access_Type (Etype (E))
+ and then not Is_Access_Constant (Etype (E))
+ then
+ Typ := Designated_Type (Etype (E));
+
+ if Has_Invariants (Typ)
+ and then Present (Invariant_Procedure (Typ))
+ and then Is_Public_Subprogram_For (Typ)
+ then
+ Obj :=
+ Make_Explicit_Dereference (Loc,
+ Prefix => New_Occurrence_Of (E, Loc));
+ Set_Etype (Obj, Typ);
+
+ Call := Make_Invariant_Call (Obj);
+
+ Append_To (Plist,
+ Make_If_Statement (Loc,
+ Condition =>
+ Make_Op_Ne (Loc,
+ Left_Opnd => Make_Null (Loc),
+ Right_Opnd => New_Occurrence_Of (E, Loc)),
+ Then_Statements => New_List (Call)));
+ end if;
+ end if;
+ end Check_Access_Invariants;
+
-------------
-- Grab_CC --
-------------
@@ -11308,12 +11351,19 @@
Formal : Entity_Id;
begin
- -- Check function return result
+ -- Check function return result. If result is an access type there
+ -- may be invariants on the designated type.
if Ekind (Designator) /= E_Procedure
and then Has_Invariants (Etype (Designator))
then
return True;
+
+ elsif Ekind (Designator) /= E_Procedure
+ and then Is_Access_Type (Etype (Designator))
+ and then Has_Invariants (Designated_Type (Etype (Designator)))
+ then
+ return True;
end if;
-- Check parameters
@@ -11321,11 +11371,15 @@
Formal := First_Formal (Designator);
while Present (Formal) loop
if Ekind (Formal) /= E_In_Parameter
- and then
- (Has_Invariants (Etype (Formal))
- or else Present (Predicate_Function (Etype (Formal))))
+ and then (Has_Invariants (Etype (Formal))
+ or else Present (Predicate_Function (Etype (Formal))))
then
return True;
+
+ elsif Is_Access_Type (Etype (Formal))
+ and then Has_Invariants (Designated_Type (Etype (Formal)))
+ then
+ return True;
end if;
Next_Formal (Formal);
@@ -11731,6 +11785,10 @@
Append_To (Plist,
Make_Invariant_Call (New_Occurrence_Of (Rent, Loc)));
end if;
+
+ -- Same if return value is an access to type with invariants.
+
+ Check_Access_Invariants (Rent);
end;
-- Procedure rather than a function
@@ -11750,7 +11808,9 @@
begin
Formal := First_Formal (Designator);
while Present (Formal) loop
- if Ekind (Formal) /= E_In_Parameter then
+ if Ekind (Formal) /= E_In_Parameter
+ or else Is_Access_Type (Etype (Formal))
+ then
Ftype := Etype (Formal);
if Has_Invariants (Ftype)
@@ -11762,6 +11822,8 @@
(New_Occurrence_Of (Formal, Loc)));
end if;
+ Check_Access_Invariants (Formal);
+
if Present (Predicate_Function (Ftype)) then
Append_To (Plist,
Make_Predicate_Check
Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb (revision 191914)
+++ exp_ch3.adb (working copy)
@@ -3674,20 +3674,43 @@
return Node_Id
is
Sel_Comp : Node_Id;
+ Typ : Entity_Id;
+ Call : Node_Id;
begin
Invariant_Found := True;
+ Typ := Etype (Comp);
+
Sel_Comp :=
Make_Selected_Component (Loc,
Prefix => New_Occurrence_Of (Object_Entity, Loc),
Selector_Name => New_Occurrence_Of (Comp, Loc));
- return
+ if Is_Access_Type (Typ) then
+ Sel_Comp := Make_Explicit_Dereference (Loc, Sel_Comp);
+ Typ := Designated_Type (Typ);
+ end if;
+
+ Call :=
Make_Procedure_Call_Statement (Loc,
Name =>
- New_Occurrence_Of
- (Invariant_Procedure (Etype (Comp)), Loc),
+ New_Occurrence_Of (Invariant_Procedure (Typ), Loc),
Parameter_Associations => New_List (Sel_Comp));
+
+ if Is_Access_Type (Etype (Comp)) then
+ Call :=
+ Make_If_Statement (Loc,
+ Condition =>
+ Make_Op_Ne (Loc,
+ Left_Opnd => Make_Null (Loc),
+ Right_Opnd =>
+ Make_Selected_Component (Loc,
+ Prefix => New_Occurrence_Of (Object_Entity, Loc),
+ Selector_Name => New_Occurrence_Of (Comp, Loc))),
+ Then_Statements => New_List (Call));
+ end if;
+
+ return Call;
end Build_Component_Invariant_Call;
----------------------------
@@ -3706,8 +3729,17 @@
if Nkind (Decl) = N_Component_Declaration then
Id := Defining_Identifier (Decl);
- if Has_Invariants (Etype (Id)) then
+ if Has_Invariants (Etype (Id))
+ and then In_Open_Scopes (Scope (R_Type))
+ then
Append_To (Stmts, Build_Component_Invariant_Call (Id));
+
+ elsif Is_Access_Type (Etype (Id))
+ and then not Is_Access_Constant (Etype (Id))
+ and then Has_Invariants (Designated_Type (Etype (Id)))
+ and then In_Open_Scopes (Scope (Designated_Type (Etype (Id))))
+ then
+ Append_To (Stmts, Build_Component_Invariant_Call (Id));
end if;
end if;
@@ -5861,10 +5893,15 @@
Build_Array_Init_Proc (Base, N);
end if;
- if Has_Invariants (Component_Type (Base)) then
+ if Has_Invariants (Component_Type (Base))
+ and then In_Open_Scopes (Scope (Component_Type (Base)))
+ then
+ -- Generate component invariant checking procedure. This is only
+ -- relevant if the array type is within the scope of the component
+ -- type. Otherwise an array object can only be built using the public
+ -- subprograms for the component type, and calls to those will have
+ -- invariant checks.
- -- Generate component invariant checking procedure.
-
Insert_Component_Invariant_Checks
(N, Base, Build_Array_Invariant_Proc (Base, N));
end if;
