[Ada] Invariant checks and multiple inheritance

Submitted by Arnaud Charlet on Oct. 1, 2012, 8:39 a.m.


Message ID 20121001083953.GA4163@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Oct. 1, 2012, 8:39 a.m.
This patch fixes some problems involving the use of Type_Invariant'Class on
the ancestor of a derived type that also implements an interface.

The following command:

   gnatmake -q -gnat12 -gnata test_invariant

must yield:

        failed inherited invariant from invariants.ads:5
with Carrier.Next; use Carrier.Next;
procedure Test_Invariant is
  THing : NT;
  HeHe (Thing);
package Carrier is
  type PT is tagged private;
  function Invariant(X: PT) return Boolean;
  procedure Do_AandB(X: out PT);
  type PT is tagged record A,B: Integer; end record;
  procedure Do_A(X: out PT; V: Integer);
  procedure Do_B(X: out PT; V: Integer);
end Carrier;
Package body Carrier is
  procedure Do_AandB(X: out PT) is
      begin Do_A(X,42); Do_B(X,42); end Do_AandB;
  function Invariant(X: PT) return Boolean is
      begin return X.A=X.B; end Invariant;
  procedure Do_A(X: out PT; V: Integer) is begin X.A := V; end Do_A;
  procedure Do_B(X: out PT; V: Integer) is begin X.B := V; end do_B;
end Carrier;
with Carrier; use Carrier;
Package Invariants is
  type T is new PT with private
    with Type_Invariant'class => Invariant(PT(T));
    -- type T introduced by my ignorance about visibility rules inside
    -- of type invariants; maybe could be on Carrier.PT already, or
    -- only on I below. The conclusion applies in all cases and
    -- combinations.
  type T is new PT with null record;
end Invariants;
package Interf is
  type I is Interface
  -- if you want:
    with Type_Invariant'Class => Invariant(I);
  -- maybe with the same "carrier detour" because of visibility?
  function Invariant(X: I) return boolean is abstract;
  procedure HeHe(X: out I) is abstract;
end Interf;
with Invariants; with Interf;
package Carrier.Next is
  type NT is new Invariants.T and Interf.I with null record;
  procedure HeHe(X: out NT); -- newly added op; definitely needs 	
			      -- to check the invariant, or else....
end Carrier.Next;
package body Carrier.Next is
  procedure HeHe(X: out NT) is
end Carrier.Next;

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

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

	* aspects.ads: Type_Invariant'class is a valid aspect.
	* sem_ch6.adb (Is_Public_Subprogram_For): with the exception of
	initialization procedures, subprograms that do not come from
	source are not public for the purpose of invariant checking.
	* sem_ch13.adb (Build_Invariant_Procedure): Handle properly the
	case of a non-private type in a package without a private part,
	when the type inherits invariants from its ancestor.

Patch hide | download patch | download mbox

Index: aspects.ads
--- aspects.ads	(revision 191888)
+++ aspects.ads	(working copy)
@@ -191,11 +191,12 @@ 
    --  The following array indicates aspects that accept 'Class
    Class_Aspect_OK : constant array (Aspect_Id) of Boolean :=
-                       (Aspect_Invariant     => True,
-                        Aspect_Pre           => True,
-                        Aspect_Predicate     => True,
-                        Aspect_Post          => True,
-                        others               => False);
+                       (Aspect_Invariant      => True,
+                        Aspect_Pre            => True,
+                        Aspect_Predicate      => True,
+                        Aspect_Post           => True,
+                        Aspect_Type_Invariant => True,
+                        others                => False);
    --  The following array indicates aspects that a subtype inherits from
    --  its base type. True means that the subtype inherits the aspect from
Index: sem_ch6.adb
--- sem_ch6.adb	(revision 191888)
+++ sem_ch6.adb	(working copy)
@@ -11342,10 +11342,16 @@ 
          --  If the subprogram declaration is not a list member, it must be
          --  an Init_Proc, in which case we want to consider it to be a
          --  public subprogram, since we do get initializations to deal with.
+         --  Other internally generated subprograms are not public.
-         if not Is_List_Member (DD) then
+         if not Is_List_Member (DD)
+           and then Is_Init_Proc (DD)
+         then
             return True;
+         elsif not Comes_From_Source (DD) then
+            return False;
          --  Otherwise we test whether the subprogram is declared in the
          --  visible declarations of the package containing the type.
Index: sem_ch13.adb
--- sem_ch13.adb	(revision 191900)
+++ sem_ch13.adb	(working copy)
@@ -5188,9 +5188,6 @@ 
                  Statements => Stmts));
          --  Insert procedure declaration and spec at the appropriate points.
-         --  Skip this if there are no private declarations (that's an error
-         --  that will be diagnosed elsewhere, and there is no point in having
-         --  an invariant procedure set if the full declaration is missing).
          if Present (Private_Decls) then
@@ -5214,6 +5211,19 @@ 
             if In_Private_Part (Current_Scope) then
                Analyze (PBody);
             end if;
+         --  If there are no private declarations this may be an error that
+         --  will be diagnosed elsewhere. However, if this is a non-private
+         --  type that inherits invariants, it needs no completion and there
+         --  may be no private part. In this case insert invariant procedure
+         --  at end of current declarative list, and analyze at once, given
+         --  that the type is about to be frozen.
+         elsif not Is_Private_Type (Typ) then
+            Append_To (Visible_Decls, PDecl);
+            Append_To (Visible_Decls, PBody);
+            Analyze (PDecl);
+            Analyze (PBody);
          end if;
       end if;
    end Build_Invariant_Procedure;