[Ada] Ada 2012 invariant checks on access values and components

[Arnaud Charlet <charlet at adacore dot com>]

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  <schonberg@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.

Attachment: difs
Description: Text document