[Ada] Additional invariant checks on composite types

[Arnaud Charlet <charlet at adacore dot com>]

If a composite type has a declared invariant, and some of its compoents are of
types that have their own invariants, the invariant checks on those compoents
must be added to the invariant checks for the enclosing type.

The command;

   gnatmake -q -gnat12 -gnata test_bars
   test_bars

must yield:

   chart invariant violation detected
   value invariant violation detected

with Ada.Assertions; use Ada.Assertions;
with Bars; use Bars;
with Text_IO; use Text_IO;
procedure Test_Bars is
   B : Bar_chart := Bare_Bar (5);
   D : Data (1 .. 5) := (20, 20, 20, 20, 19);
begin
   begin
      Assemble (D, B);
   exception
      when Assertion_Error => Put_Line ("chart invariant violation detected");
   end;

   declare
      D : Data (1 .. 5) := (30, 30, 30, 30, -20);
   begin
      Assemble (D, B);
   exception
      when Assertion_Error => Put_Line ("value invariant violation detected");
   end;
end;
---
package Bars is
   type Value is private
     with Invariant => Legal (Value);

   type Bar_Chart (<>) is private
     with Invariant => Complete (Bar_Chart);

   type Data is array (positive range <>) of Integer;

   function Legal (It : Value) return Boolean;
   function Complete (It : Bar_Chart) return Boolean;
   function Bare_Bar (N : Positive) return Bar_Chart;
   procedure Assemble (From : Data; Result : out Bar_Chart);
private
   type Value is new Integer;
   type Bar_Chart is array (positive range <>) of Value;
end;
--- 
package body  Bars is
   --  type Value is private
   --    with Invariant => Legal (Value);

   --  type Bar_Chart is private
   --    with Invariant => Complete (Bar_Chart);

   function Legal (It : Value) return Boolean is
   begin
      return It >= 0 and It <= 100;
   end;

   function Complete (It : Bar_Chart) return Boolean is
      Total : Value := 0;
   begin
      for B of It loop Total := Total + B; end loop;
      return Total = 100;
   end;
      
   function Bare_Bar (N : Positive) return Bar_Chart is
      Result : Bar_Chart (1 .. N) := (100, others => 0);
   begin
      return Result;
   end;
      
   
   procedure Assemble (From : Data; Result : out Bar_Chart) is
   begin
      for J in From'range loop
         Result (J) := Value (From (J));
      end loop;
   end;
end;

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

2012-10-01  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch3.ads (Build_Array_Invariant_Proc): moved to body.
	* exp_ch3.adb (Build_Array_Invariant_Proc,
	Build_Record_Invariant_Proc): transform into functions.
	(Insert_Component_Invariant_Checks): for composite types that have
	components with specified invariants, build a checking procedure,
	and make into the invariant procedure of the composite type,
	or incorporate it into the user- defined invariant procedure if
	one has been created.
	* sem_ch3.adb (Array_Type_Declaration): Checking for invariants
	on the component type is defered to the expander.

Attachment: difs
Description: Text document