[Ada] Reimplementation of type invariants

This patch prevents the insertion of the invariant procedure declaration and
body when the context is a generic unit. This ensures that generated code does
not permiate the template.

------------
-- Source --
------------

--  tester.ads

package Tester is
   type Type_Id is
     (Ext_1_Id,
      Ext_1_FV_Id,
      Ext_2_Id,
      Ext_3_Id,
      Ext_4_Id,
      Ext_4_FV_Id,
      Ext_5_Id,
      Ext_6_Id,
      Ext_6_FV_Id,
      Ext_7_Id,
      Ext_8_Id,
      Iface_1_Id,
      Iface_2_Id,
      Iface_3_Id,
      Iface_4_Id,
      Par_1_Id,
      Par_2_FV_Id,
      Par_3_Id,
      Par_4_Id,
      Par_4_FV_Id,
      Prot_1_FV_Id,
      Prot_2_Id,
      Prot_3_Id,
      Prot_3_FV_Id,
      Synch_1_Id,
      Synch_2_Id,
      Tag_1_Id,
      Tag_2_Id,
      Tag_3_Id,
      Tag_4_Id,
      Tag_4_FV_Id,
      Tag_5_Id,
      Tag_6_Id,
      Tag_7_Id,
      Tag_8_Id,
      Tag_9_Id,
      Tag_10_Id,
      Tag_11_Id,
      Tag_12_Id,
      Tag_13_Id,
      Tag_14_Id,
      Tag_15_Id,
      Tag_15_FV_Id,
      Tag_16_Id,
      Tag_17_Id,
      Tag_18_Id,
      Tag_19_Id,
      Tag_20_Id,
      Tag_20_FV_Id,
      Tag_21_Id,
      Tag_22_Id,
      Tag_23_Id,
      Tag_24_Id,
      Tag_24_FV_Id,
      Tag_25_Id,
      Tag_26_Id,
      Tag_27_Id,
      Tag_28_Id,
      Task_1_Id,
      Task_2_Id,
      Task_2_FV_Id,
      Untag_1_Id,
      Untag_2_Id,
      Untag_3_Id,
      Untag_4_Id,
      Untag_5_Id,
      Untag_6_Id,
      Untag_7_Id,
      Untag_8_Id,
      Untag_9_Id);

   type Results is array (Type_Id) of Boolean;

   function Mark (Typ : Type_Id) return Boolean;
   --  Mark the result for a particular type as verified. The function always
   --  returns True.

   procedure Reset_Results;
   --  Reset the internally kept result state

   procedure Test_Results (Test_Id : String; Exp : Results);
   --  Ensure that the internally kept result state agrees with expected
   --  results Exp. Emit an error if this is not the case.
end Tester;

--  tester.adb

with Ada.Text_IO; use Ada.Text_IO;

package body Tester is
   State : Results;

   ----------
   -- Mark --
   ----------

   function Mark (Typ : Type_Id) return Boolean is
   begin
      State (Typ) := True;
      return True;
   end Mark;

   -------------------
   -- Reset_Results --
   -------------------

   procedure Reset_Results is
   begin
      State := (others => False);
   end Reset_Results;

   ------------------
   -- Test_Results --
   ------------------

   procedure Test_Results (Test_Id : String; Exp : Results) is
      Exp_Val   : Boolean;
      Posted    : Boolean := False;
      State_Val : Boolean;

   begin
      for Index in Results'Range loop
         Exp_Val   := Exp (Index);
         State_Val := State (Index);

         if State_Val /= Exp_Val then
            if not Posted then
               Posted := True;
               Put_Line (Test_Id & ": ERROR");
            end if;

            Put_Line ("  Expected: " & Exp_Val'Img & " for " & Index'Img);
            Put_Line ("  Got:      " & State_Val'Img);
         end if;
      end loop;

      if not Posted then
         Put_Line (Test_Id & ": OK");
      end if;
   end Test_Results;
end Tester;

--  gen_invariants.ads

with Tester; use Tester;

generic
package Gen_Invariants is
   type Untag_1 is private
     with Type_Invariant => Mark (Untag_1_Id);

private
   type Untag_1 is null record;

   Obj_1 : Untag_1;
end Gen_Invariants;

-----------------
-- Compilation --
-----------------

$ gcc -c -gnata -gnatDG gen_invariants.ads
$ grep "Invariant" gen_invariants.ads.dg

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

2016-06-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch7.adb (Build_Invariant_Procedure_Body):
	Always install the scope of the invariant procedure
	in order to produce better error messages. Do not
	insert the body when the context is a generic unit.
	(Build_Invariant_Procedure_Declaration): Perform minimal
	decoration of the invariant procedure and its formal parameter
	in case they are not analyzed.	Do not insert the declaration
	when the context is a generic unit.

[Ada] Reimplementation of type invariants

Commit Message

Patch