[Ada] Ada 2012 type invariants on type completions

[Arnaud Charlet]

In Ada 2012, type invariants can appear in the private part of a package, on
a type declaration that is a completion. This patch analyzes properly the
invariant and creates the invariant procedure for the type, so that it is
applied in the same contexts as an invariant in the visible part.

Compiling wrong_inv.ads must yield:

   wrong_inv.ads:7:31: expected type "Standard.Boolean"
   wrong_inv.ads:7:31: found type universal integer
---
package Wrong_Inv is
   type T is private;
   function Is_OK (Obj : T) return Boolean;
   function Wrong (X : Integer) return T;
private
   type T is new Integer range 1 .. 10000
     with Type_Invariant => 1 + 2;
end;
---
The following must execute quietly:

   gnatmake -q -gnat12 -gnata test_invariant
   test_invariant

---
with Ada.Assertions; use Ada.Assertions;
with Typinv; use Typinv;
procedure Test_Invariant is
   Thing : T;
begin
   Thing:= Wrong (5);
   raise Program_Error;
exception
   when Assertion_Error => null;
end;
---
package Typinv is
   type T is private;
   function Is_OK (Obj : T) return Boolean;
   function Wrong (X : Integer) return T;
private
   type T is new Integer range 1 .. 10000
      with Type_Invariant => Is_OK (T);
end;
---
package body  Typinv is
   function Is_OK (Obj : T) return Boolean is
   begin
      return Obj mod 7 = 3;
   end;
   function Wrong (X : Integer) return T is
   begin
      return 9;
   end;
end;

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

2011-12-21  Ed Schonberg  <schonb...@adacore.com>

        * sem_ch7.adb, sem_ch13.adb (Analyze_Package_Specification): Build the
        invariant procedure of a type declaration that is a completion and has
        aspect specifications.
        (Build_Invariant_Procedure): If the procedure is built for a
        type declaration that is a completion, analyze body expliitly
        because all private declarations have been already analyzed.


Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 182572)
+++ sem_ch7.adb (working copy)
@@ -1378,6 +1378,16 @@
               ("full view of & does not have preelaborable initialization", E);
          end if;
 
+         --  An invariant may appear on a full view of a type
+
+         if Is_Type (E)
+           and then Has_Private_Declaration (E)
+           and then Nkind (Parent (E)) = N_Full_Type_Declaration
+           and then Has_Aspects (Parent (E))
+         then
+            Build_Invariant_Procedure (E, N);
+         end if;
+
          Next_Entity (E);
       end loop;
 
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb        (revision 182585)
+++ sem_ch13.adb        (working copy)
@@ -4738,6 +4738,14 @@
             --  (this is an error that will be caught elsewhere);
 
             Append_To (Private_Decls, PBody);
+
+            --  If the invariant appears on the full view of a type, the
+            --  analysis of the private part is complete, and we must
+            --  analyze the new body explicitly.
+
+            if In_Private_Part (Current_Scope) then
+               Analyze (PBody);
+            end if;
          end if;
       end if;
    end Build_Invariant_Procedure;